diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,5 @@
+# Revision history for typed-fsm
+
+## 0.1.0.0 -- YYYY-mm-dd
+
+* First version. Released on an unsuspecting world.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2024 Yang Miao
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
diff --git a/examples/ATM/EventToMsg.hs b/examples/ATM/EventToMsg.hs
new file mode 100644
--- /dev/null
+++ b/examples/ATM/EventToMsg.hs
@@ -0,0 +1,57 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE ViewPatterns #-}
+
+module EventToMsg where
+
+import Data.Data (Proxy (..))
+import qualified Data.Dependent.Map as D
+import Data.Dependent.Sum
+import Data.Singletons (SingI)
+import Lens.Micro
+import Type
+import TypedFsm.Driver
+import Utils
+
+scEventHandler
+  :: (SingI n, Less3 n)
+  => Proxy n
+  -> GenMsg ATMSt InternalState MyEvent (CardInserted n)
+scEventHandler _ =
+  GenMsg
+    ( \ist event -> case event of
+        MyMouseLeftButtonClick (fmap fromIntegral -> p) ->
+          if
+            | (ist ^. ejectLabel . rect) `contains` p -> Just (SomeMsg CIEject)
+            | (ist ^. checkPinLabel . rect) `contains` p -> Just (SomeMsg (CheckPIN 1234))
+            | (ist ^. checkPinErrorLabel . rect) `contains` p -> Just (SomeMsg (CheckPIN 1))
+            | otherwise -> Nothing
+    )
+
+atmDepMap :: State2GenMsg ATMSt InternalState MyEvent
+atmDepMap =
+  D.fromList
+    [ SReady
+        :=> GenMsg
+          ( \ist event -> case event of
+              MyMouseLeftButtonClick (fmap fromIntegral -> p) ->
+                ( if
+                    | (ist ^. insCardLabel . rect) `contains` p -> Just (SomeMsg InsertCard)
+                    | (ist ^. exitLabel . rect) `contains` p -> Just (SomeMsg ExitATM)
+                    | otherwise -> Nothing
+                )
+          )
+    , SCardInserted SZ :=> scEventHandler Proxy
+    , SCardInserted (SS SZ) :=> scEventHandler Proxy
+    , SCardInserted (SS (SS SZ)) :=> scEventHandler Proxy
+    , SSession
+        :=> GenMsg
+          ( \ist event -> case event of
+              MyMouseLeftButtonClick (fmap fromIntegral -> p) ->
+                if
+                  | (ist ^. ejectLabel . rect) `contains` p -> Just (SomeMsg SEject)
+                  | (ist ^. getAmountLabel . rect) `contains` p -> Just (SomeMsg GetAmount)
+                  | (ist ^. dispenseLabel . rect) `contains` p -> Just (SomeMsg (Dispense 100))
+                  | otherwise -> Nothing
+          )
+    ]
diff --git a/examples/ATM/Handler.hs b/examples/ATM/Handler.hs
new file mode 100644
--- /dev/null
+++ b/examples/ATM/Handler.hs
@@ -0,0 +1,92 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE QualifiedDo #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Handler where
+
+import Control.Monad.State
+import Data.IFunctor (At (..), IMonad (..), returnAt)
+import qualified Data.IFunctor as I
+import Data.Singletons (SingI (sing))
+import Lens.Micro.Mtl (use, (-=), (.=))
+import Type
+import TypedFsm.Core
+import TypedFsm.Driver
+
+checkResult
+  :: forall n
+   . (SingI n, Less3 n)
+  => Int
+  -> Operate (StateT InternalState IO) CheckPINResult (CheckPin n)
+checkResult i = I.do
+  At userPin <- liftm $ use pin
+  if i == userPin
+    then LiftM $ pure (ireturn Correct)
+    else LiftM $ pure (ireturn (Incorrect @n))
+
+checkPinFun
+  :: forall (n :: N)
+   . (SingI n)
+  => Int
+  -> Operate (StateT InternalState IO) CheckPINResult (CheckPin (n :: N))
+checkPinFun i = I.do
+  case sing @n of
+    SS SZ -> checkResult i
+    SS (SS SZ) -> checkResult i
+    sn@(SS (SS (SS SZ))) -> I.do
+      At userPin <- liftm $ use pin
+      if i == userPin
+        then LiftM $ pure (ireturn Correct)
+        else LiftM $ do
+          liftIO $ putStrLn "-> test 3 times, eject card!"
+          pure (ireturn (EjectCard sn))
+    _ -> error "np"
+
+readyHandler :: Op ATMSt InternalState IO () Exit Ready
+readyHandler = I.do
+  msg <- getInput
+  case msg of
+    InsertCard -> cardInsertedHandler
+    ExitATM -> returnAt ()
+
+cardInsertedHandler
+  :: (SingI n)
+  => Op ATMSt InternalState IO () Exit (CardInserted n)
+cardInsertedHandler = I.do
+  msg <- getInput
+  case msg of
+    CIEject -> I.do
+      readyHandler
+    CheckPIN i -> I.do
+      res <- checkPinFun i
+      case res of
+        EjectCard _ -> readyHandler
+        Incorrect -> cardInsertedHandler
+        Correct -> I.do
+          liftm $ amountLabel . label .= ("Amount: -- ")
+          sessionHandler
+
+sessionHandler :: Op ATMSt InternalState IO () Exit Session
+sessionHandler = I.do
+  msg <- getInput
+  case msg of
+    GetAmount -> I.do
+      liftm $ do
+        am <- use amount
+        amountLabel . label .= ("Amount: " <> show am)
+        liftIO $ putStrLn ("-> User Amount: " <> show am)
+      sessionHandler
+    Dispense i -> I.do
+      liftm $ do
+        amount -= i -- need to check amount is enough?
+        liftIO $ putStrLn ("-> Use dispense " ++ show i)
+        am <- use amount
+        amountLabel . label .= ("Now Amount: " <> show am)
+        liftIO $ putStrLn ("-> Now User Amount: " <> show am)
+      sessionHandler
+    SEject -> readyHandler
diff --git a/examples/ATM/Main.hs b/examples/ATM/Main.hs
new file mode 100644
--- /dev/null
+++ b/examples/ATM/Main.hs
@@ -0,0 +1,79 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE QualifiedDo #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
+{-# OPTIONS_GHC -Wno-unused-do-bind #-}
+
+module Main where
+
+import Control.Concurrent (threadDelay)
+import Control.Monad.IO.Class (liftIO)
+import Control.Monad.State (StateT (runStateT))
+import qualified Control.Monad.State as M
+import EventToMsg
+import Handler
+import Lens.Micro ((^.))
+import SDL
+import qualified SDL.Font as Font
+import Type
+import TypedFsm.Driver
+import Utils
+
+main :: IO ()
+main = do
+  initialize [InitVideo]
+  Font.initialize
+  font <- Font.load "data/fonts/SourceCodePro-Regular.otf" 20
+  window <- createWindow "test" defaultWindow
+  renderer <- createRenderer window (-1) defaultRenderer
+  ccref <- initCharCache
+
+  runStateT
+    (appLoop (DrawEnv renderer font ccref) (SomeOperate readyHandler))
+    initInternState
+  destroyWindow window
+
+appLoop :: DrawEnv -> SomeOp ATMSt InternalState IO () -> StateT InternalState IO ()
+appLoop de@(DrawEnv renderer _font _ccref) (SomeOperate fun) = do
+  events <- pollEvents
+  -- liftIO $ print events
+  v <- runOp atmDepMap (makeMyEvent events) fun
+  case v of
+    Finish _ -> pure ()
+    NotMatchGenMsg si -> liftIO $ putStrLn $ "error: not match GenMsg " ++ show si
+    Cont fun1 -> do
+      let atmSt = getSomeOperateSt fun1
+      rendererDrawColor renderer $= V4 0 0 0 255
+      clear renderer
+
+      rendererDrawColor renderer $= V4 255 0 155 255
+      liftIO $ drawStrings de [show atmSt] (10, 30)
+
+      ist <- M.get
+      case atmSt of
+        Ready -> do
+          liftIO $ drawLabel de (ist ^. insCardLabel)
+          liftIO $ drawLabel de (ist ^. exitLabel)
+        CardInserted _n -> do
+          liftIO $ drawLabel de (ist ^. checkPinLabel)
+          liftIO $ drawLabel de (ist ^. checkPinErrorLabel)
+          liftIO $ drawLabel de (ist ^. ejectLabel)
+        Session -> do
+          liftIO $ drawLabel de (ist ^. amountLabel)
+          liftIO $ drawLabel de (ist ^. getAmountLabel)
+          liftIO $ drawLabel de (ist ^. dispenseLabel)
+          liftIO $ drawLabel de (ist ^. ejectLabel)
+        CheckPin _n -> pure ()
+        Exit -> pure ()
+
+      present renderer
+      liftIO $ threadDelay (1000000 `div` 30)
+      appLoop de fun1
diff --git a/examples/ATM/Type.hs b/examples/ATM/Type.hs
new file mode 100644
--- /dev/null
+++ b/examples/ATM/Type.hs
@@ -0,0 +1,144 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE QualifiedDo #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -Wall #-}
+
+module Type where
+
+import Data.GADT.Compare (GCompare (..), GEq (..))
+import Data.Int (Int32)
+import Data.Kind (Constraint, Type)
+import Data.Singletons.Base.TH
+import Data.Type.Equality (TestEquality (testEquality))
+import GHC.TypeError (TypeError)
+import GHC.TypeLits (ErrorMessage (..))
+import Lens.Micro.TH (makeLenses)
+import SDL
+import TypedFsm.Core (StateTransMsg (..))
+import TypedFsm.Driver (sOrdToGCompare)
+
+$( singletons
+    [d|
+      data N = Z | S N
+        deriving (Show, Eq, Ord)
+
+      data ATMSt
+        = Ready
+        | CardInserted N
+        | CheckPin N
+        | Session
+        | Exit
+        deriving (Show, Eq, Ord)
+      |]
+ )
+
+satmToatm :: SATMSt s -> ATMSt
+satmToatm = fromSing
+
+instance GEq SN where
+  geq = testEquality
+
+instance GEq SATMSt where
+  geq = testEquality
+
+instance GCompare SN where
+  gcompare = sOrdToGCompare
+
+instance GCompare SATMSt where
+  gcompare = sOrdToGCompare
+
+type family Less3 (n :: N) :: Constraint where
+  Less3 Z = ()
+  Less3 (S Z) = ()
+  Less3 (S (S Z)) = ()
+  Less3 _ = TypeError (Text "test must less 3")
+
+data CheckPINResult :: ATMSt -> Type where
+  EjectCard :: (n ~ S (S (S Z))) => SN n -> CheckPINResult Ready
+  Incorrect :: (SingI n, Less3 n) => CheckPINResult (CardInserted n)
+  Correct :: CheckPINResult Session
+
+instance StateTransMsg ATMSt where
+  data Msg ATMSt from to where
+    ExitATM :: Msg ATMSt Ready Exit
+    InsertCard :: Msg ATMSt Ready (CardInserted Z)
+    CIEject :: Msg ATMSt (CardInserted n) Ready
+    ---------------
+    CheckPIN :: Int -> Msg ATMSt (CardInserted n) (CheckPin (S n))
+    ---------------
+    GetAmount :: Msg ATMSt Session Session
+    Dispense :: Int -> Msg ATMSt Session Session
+    SEject :: Msg ATMSt Session Ready
+
+----------------------------------
+type Point' = Point V2 Int
+
+pattern Point :: a -> a -> Point V2 a
+pattern Point x y = P (V2 x y)
+{-# COMPLETE Point #-}
+
+newtype MyEvent = MyMouseLeftButtonClick (Point V2 Int32)
+  deriving (Show, Eq, Ord)
+
+data Rect = Rect
+  { _rx :: Int
+  , _ry :: Int
+  , _width :: Int
+  , _height :: Int
+  }
+  deriving (Show)
+
+data Label = Label
+  { _rect :: Rect
+  , _label :: String
+  }
+  deriving (Show)
+
+----------------------------------
+
+data InternalState = InternalState
+  { _pin :: Int
+  , _amount :: Int
+  , _amountLabel :: Label
+  , _insCardLabel :: Label
+  , _exitLabel :: Label
+  , _checkPinLabel :: Label
+  , _checkPinErrorLabel :: Label
+  , _getAmountLabel :: Label
+  , _dispenseLabel :: Label
+  , _ejectLabel :: Label
+  }
+  deriving (Show)
+
+initInternState :: InternalState
+initInternState =
+  InternalState
+    { _pin = 1234
+    , _amount = 1000
+    , _amountLabel = Label (Rect 10 130 100 30) "null"
+    , _insCardLabel = (Label (Rect 10 230 100 30) "Insert Card")
+    , _exitLabel = (Label (Rect 10 270 100 30) "EXIT")
+    , _checkPinLabel = (Label (Rect 10 230 100 30) "checkPin 1234")
+    , _checkPinErrorLabel = (Label (Rect 10 274 100 30) "checkPin 1 error")
+    , _getAmountLabel = (Label (Rect 10 230 100 30) "GetAmount")
+    , _dispenseLabel = (Label (Rect 130 230 100 30) "Dispense 100")
+    , _ejectLabel = (Label (Rect 10 330 100 30) "Eject")
+    }
+
+Lens.Micro.TH.makeLenses ''Rect
+Lens.Micro.TH.makeLenses ''Label
+Lens.Micro.TH.makeLenses ''InternalState
diff --git a/examples/ATM/Utils.hs b/examples/ATM/Utils.hs
new file mode 100644
--- /dev/null
+++ b/examples/ATM/Utils.hs
@@ -0,0 +1,91 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE QualifiedDo #-}
+
+module Utils where
+
+import Control.Monad
+import Data.HashMap.Strict (HashMap)
+import qualified Data.HashMap.Strict as H
+import Data.IORef
+import Linear
+import SDL
+import SDL.Font (Font)
+import qualified SDL.Font as Font
+import Type
+
+type CharCache = HashMap Char Texture
+type CharCacheRef = IORef CharCache
+
+data DrawEnv = DrawEnv
+  { _renderer :: Renderer
+  , _font :: Font
+  , _charCacheRef :: CharCacheRef
+  }
+
+eventToKP :: Event -> Maybe MyEvent
+eventToKP e = case eventPayload e of
+  MouseButtonEvent (MouseButtonEventData _ Pressed _ _ _ pos) ->
+    Just $ MyMouseLeftButtonClick pos
+  _ -> Nothing
+
+makeMyEvent :: [Event] -> [MyEvent]
+makeMyEvent events =
+  let fun b a =
+        case eventToKP a of
+          Nothing -> b
+          Just a' -> a' : b
+   in reverse (foldl' fun [] events)
+
+pattern KBE
+  :: InputMotion
+  -> Keycode
+  -> Bool
+  -> Maybe Window
+  -> Scancode
+  -> KeyModifier
+  -> EventPayload
+pattern KBE press keycode repeat a d f =
+  KeyboardEvent
+    (KeyboardEventData a press repeat (Keysym d keycode f))
+
+initCharCache :: IO CharCacheRef
+initCharCache = newIORef H.empty
+
+getCharTexure :: Renderer -> Font -> CharCacheRef -> Char -> IO Texture
+getCharTexure r font cref c = do
+  cc <- readIORef cref
+  case H.lookup c cc of
+    Nothing -> do
+      surf <- Font.blendedGlyph font (V4 0 255 0 255) c
+      text <- createTextureFromSurface r surf
+      freeSurface surf
+      modifyIORef' cref (H.insert c text)
+      pure text
+    Just t -> pure t
+
+drawString :: DrawEnv -> String -> (Int, Int) -> IO ()
+drawString (DrawEnv r font cref) st (x', y') = do
+  let go _ _ [] = pure ()
+      go x y (t : ts) = do
+        TextureInfo _ _ w h <- queryTexture t
+        copy r t Nothing (Just (Rectangle (P (V2 x y)) (V2 w h)))
+        go (x + w) y ts
+  txts <- mapM (getCharTexure r font cref) st
+  go (fromIntegral x') (fromIntegral y') txts
+
+drawStrings :: DrawEnv -> [String] -> (Int, Int) -> IO ()
+drawStrings de sts (x, y) = do
+  forM_ (zip [0 ..] sts) $ \(i, st) -> do
+    drawString de st (x, y + i * 20)
+
+drawLabel :: DrawEnv -> Label -> IO ()
+drawLabel de@(DrawEnv{_renderer}) (Label (Rect x y w h) st) = do
+  drawRect _renderer (Just (Rectangle (P (V2 (fromIntegral x) (fromIntegral y))) (V2 (fromIntegral w) (fromIntegral h))))
+  drawString de st (x, y)
+
+contains :: Rect -> Point' -> Bool
+contains (Rect rx1 ry1 w h) (Point x y) =
+  (rx1 <= x && x <= rx1 + w) && (ry1 <= y && y <= ry1 + h)
diff --git a/examples/motion/EventToMsg.hs b/examples/motion/EventToMsg.hs
new file mode 100644
--- /dev/null
+++ b/examples/motion/EventToMsg.hs
@@ -0,0 +1,48 @@
+{-# LANGUAGE ViewPatterns #-}
+
+module EventToMsg where
+
+import qualified Data.Dependent.Map as D
+import Data.Dependent.Sum
+import Type
+import TypedFsm.Driver
+import Utils
+
+mouseDepMap :: State2GenMsg Motion MotionState MyEvent
+mouseDepMap =
+  D.fromList
+    [ SIdle
+        :=> GenMsg
+          ( \(MotionState rect' _ _ _) event -> case event of
+              MyQuit -> Just (SomeMsg ExitMotion)
+              MyMouseMotion (fmap fromIntegral -> p) tms ->
+                if rect' `contains` p
+                  then Just $ SomeMsg (MoveIn p tms)
+                  else Nothing
+              _ -> Nothing
+          )
+    , SOver
+        :=> GenMsg
+          ( \(MotionState rect' _ _ _) event -> case event of
+              MyQuit -> Just (SomeMsg ExitMotion)
+              MyMouseMotion (fmap fromIntegral -> p) tms ->
+                if rect' `contains` p
+                  then Just $ SomeMsg (InMove p tms)
+                  else Just $ SomeMsg MoveOut
+              MyTimeout -> Just $ SomeMsg TimeoutH
+          )
+    , SHover
+        :=> GenMsg
+          ( \(MotionState rect' _ (Point mx my) _) event -> case event of
+              MyQuit -> Just (SomeMsg ExitMotion)
+              MyMouseMotion (fmap fromIntegral -> p@(Point x y)) tms ->
+                if rect' `contains` p
+                  then
+                    if abs (mx - x) < 30 && abs (my - y) < 30
+                      then Nothing
+                      else
+                        Just $ SomeMsg (HInMove p tms)
+                  else Just $ SomeMsg HMoveOut
+              _ -> Nothing
+          )
+    ]
diff --git a/examples/motion/Handler.hs b/examples/motion/Handler.hs
new file mode 100644
--- /dev/null
+++ b/examples/motion/Handler.hs
@@ -0,0 +1,82 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE NumericUnderscores #-}
+{-# LANGUAGE QualifiedDo #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# OPTIONS_GHC -Wall #-}
+
+module Handler where
+
+import Control.Concurrent.STM (atomically)
+import Control.Concurrent.STM.TChan
+import Control.Monad.State
+import Data.IFunctor (At (..), returnAt)
+import qualified Data.IFunctor as I
+import GHC.Event
+import Lens.Micro.Mtl
+import SDL
+import Type
+import TypedFsm.Core
+import TypedFsm.Driver
+
+timeoutSize :: Int
+timeoutSize = 400_000
+
+myRegisterTimeout :: StateT MotionState IO (TimerManager, TimeoutKey)
+myRegisterTimeout = do
+  chan <- use channel
+  liftIO $ do
+    tm <- getSystemTimerManager
+    tk <- registerTimeout tm timeoutSize (atomically $ writeTChan chan ())
+    pure (tm, tk)
+
+idelHandler :: Op Motion MotionState IO () Exit Idle
+idelHandler = I.do
+  msg <- getInput
+  case msg of
+    ExitMotion -> returnAt ()
+    MoveIn pos tms -> I.do
+      At tp <- liftm $ do
+        mousePos .= pos
+        (tm, tk) <- myRegisterTimeout
+        pure (tm, tk, tms)
+      overHandler tp
+
+overHandler :: (TimerManager, TimeoutKey, Timestamp) -> Op Motion MotionState IO () Exit Over
+overHandler (tm, tk, oldtms) = I.do
+  msg <- getInput
+  case msg of
+    ExitMotion -> returnAt ()
+    MoveOut -> I.do
+      liftm $ liftIO $ unregisterTimeout tm tk
+      idelHandler
+    InMove pos tms -> I.do
+      liftm $ do
+        mousePos .= pos
+      if tms - oldtms > 40
+        then I.do
+          liftm $ liftIO $ updateTimeout tm tk timeoutSize
+          overHandler (tm, tk, tms)
+        else overHandler (tm, tk, oldtms)
+    TimeoutH -> I.do
+      liftm $ do
+        liftIO $ unregisterTimeout tm tk
+        pos <- use mousePos
+        onHover .= Just (pos, [show oldtms, show pos])
+      hoverHandler
+
+hoverHandler :: Op Motion MotionState IO () Exit Hover
+hoverHandler = I.do
+  msg <- getInput
+  case msg of
+    ExitMotion -> returnAt ()
+    HInMove pos tms -> I.do
+      At tp <- liftm $ do
+        mousePos .= pos
+        onHover .= Nothing
+        (tm, tk) <- myRegisterTimeout
+        pure (tm, tk, tms)
+      overHandler tp
+    HMoveOut -> I.do
+      liftm $ onHover .= Nothing
+      idelHandler
diff --git a/examples/motion/Main.hs b/examples/motion/Main.hs
new file mode 100644
--- /dev/null
+++ b/examples/motion/Main.hs
@@ -0,0 +1,85 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE QualifiedDo #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# OPTIONS_GHC -Wno-unused-do-bind #-}
+
+module Main where
+
+import Control.Concurrent (threadDelay)
+import Control.Concurrent.STM (atomically)
+import Control.Concurrent.STM.TChan
+import Control.Monad.IO.Class (liftIO)
+import Control.Monad.State (StateT (runStateT))
+import qualified Control.Monad.State as M
+import EventToMsg
+import Handler
+import SDL
+import qualified SDL.Font as Font
+import Type
+import TypedFsm.Driver
+import Utils
+
+main :: IO ()
+main = do
+  initialize [InitVideo]
+  Font.initialize
+  font <- Font.load "data/fonts/SourceCodePro-Regular.otf" 20
+  window <- createWindow "test" defaultWindow
+  renderer <- createRenderer window (-1) defaultRenderer
+  ccref <- initCharCache
+  chan <- newTChanIO @()
+
+  runStateT
+    (appLoop (DrawEnv renderer font ccref) chan mouseDepMap (SomeOperate idelHandler))
+    (MotionState (Rect 100 100 400 400) chan (Point 0 0) Nothing)
+
+  destroyWindow window
+
+creatRect :: (Integral p1, Integral p2, Integral p3, Integral p4, Num a) => p1 -> p2 -> p3 -> p4 -> Rectangle a
+creatRect x y w h =
+  Rectangle
+    (P (V2 (fromIntegral x) (fromIntegral y)))
+    (V2 (fromIntegral w) (fromIntegral h))
+
+appLoop
+  :: DrawEnv
+  -> TChan ()
+  -> State2GenMsg Motion MotionState MyEvent
+  -> SomeOp Motion MotionState IO ()
+  -> StateT MotionState IO ()
+appLoop de@(DrawEnv renderer _font _ccref) chan depMap (SomeOperate fun) = do
+  events <- pollEvents
+  ma <- liftIO (atomically $ tryReadTChan chan)
+  v <- runOp depMap (makeMyEvent ma events) fun
+  case v of
+    Finish _ -> pure ()
+    NotMatchGenMsg si -> liftIO $ putStrLn $ "error: not match GenMsg " ++ show si
+    Cont fun1 -> do
+      rendererDrawColor renderer $= V4 0 0 0 255
+      clear renderer
+
+      let motionState = getSomeOperateSt fun1
+      liftIO $ drawStrings de [show motionState] (10, 30)
+
+      MotionState (Rect x y w h) _ _ mOnhove <- M.get
+      rendererDrawColor renderer $= V4 255 0 155 255
+      drawRect renderer $ Just (creatRect x y w h)
+
+      liftIO $
+        case mOnhove of
+          Nothing -> pure ()
+          Just (Point x' y', st) -> do
+            rendererDrawColor renderer $= V4 100 155 144 255
+            fillRect renderer $ Just (creatRect x' y' (300 :: Int) (-100 :: Int))
+            drawStrings de st (fromIntegral x', fromIntegral y' - 60)
+
+      present renderer
+      liftIO $ threadDelay (1000000 `div` 30)
+
+      appLoop de chan depMap fun1
diff --git a/examples/motion/Type.hs b/examples/motion/Type.hs
new file mode 100644
--- /dev/null
+++ b/examples/motion/Type.hs
@@ -0,0 +1,94 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE NumericUnderscores #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE QualifiedDo #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ViewPatterns #-}
+
+module Type where
+
+import Control.Concurrent.STM.TChan
+import Data.GADT.Compare (GCompare (..), GEq (..))
+import Data.Int (Int32)
+import Data.Singletons.Base.TH
+import Data.Type.Equality (TestEquality (testEquality))
+import Lens.Micro.TH
+import SDL
+import TypedFsm.Core
+import TypedFsm.Driver
+
+$( singletons
+    [d|
+      data Motion
+        = Idle
+        | Over
+        | Hover
+        | Exit
+        deriving (Show, Eq, Ord)
+      |]
+ )
+
+instance GEq SMotion where
+  geq = testEquality
+
+instance GCompare SMotion where
+  gcompare = sOrdToGCompare
+
+smTom :: SMotion m -> Motion
+smTom = fromSing
+
+----------------------------------
+type Point' = Point V2 Int
+
+pattern Point :: a -> a -> Point V2 a
+pattern Point x y = P (V2 x y)
+{-# COMPLETE Point #-}
+
+instance StateTransMsg Motion where
+  data Msg Motion from to where
+    ExitMotion :: Msg Motion s Exit
+    -----------------
+    MoveIn :: Point' -> Timestamp -> Msg Motion Idle Over
+    -----------------
+    MoveOut :: Msg Motion Over Idle
+    InMove :: Point' -> Timestamp -> Msg Motion Over Over
+    TimeoutH :: Msg Motion Over Hover
+    -----------------
+    HInMove :: Point' -> Timestamp -> Msg Motion Hover Over
+    HMoveOut :: Msg Motion Hover Idle
+
+data Rect = Rect
+  { _rx :: Int
+  , _ry :: Int
+  , _width :: Int
+  , _height :: Int
+  }
+  deriving (Show)
+
+data MotionState = MotionState
+  { _rect :: Rect
+  , _channel :: TChan ()
+  , _mousePos :: Point'
+  , _onHover :: Maybe (Point', [String])
+  }
+
+data MyEvent
+  = MyMouseMotion (Point V2 Int32) Timestamp
+  | MyTimeout
+  | MyQuit
+  deriving (Show, Eq, Ord)
+
+----------------------------------
+
+makeLenses ''MotionState
diff --git a/examples/motion/Utils.hs b/examples/motion/Utils.hs
new file mode 100644
--- /dev/null
+++ b/examples/motion/Utils.hs
@@ -0,0 +1,91 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE QualifiedDo #-}
+
+module Utils where
+
+import Control.Monad
+import Data.HashMap.Strict (HashMap)
+import qualified Data.HashMap.Strict as H
+import Data.IORef
+import Linear
+import SDL
+import SDL.Font (Font)
+import qualified SDL.Font as Font
+import Type
+
+type CharCache = HashMap Char Texture
+type CharCacheRef = IORef CharCache
+
+data DrawEnv = DrawEnv
+  { _renderer :: Renderer
+  , _font :: Font
+  , _charCacheRef :: CharCacheRef
+  }
+
+eventToKP :: Event -> Maybe MyEvent
+eventToKP e = case eventPayload e of
+  QuitEvent -> Just MyQuit
+  KBE Pressed KeycodeQ _ _ _ _ -> Just MyQuit
+  KBE Pressed KeycodeEscape _ _ _ _ -> Just MyQuit
+  MouseMotionEvent (MouseMotionEventData _ _ _ pos _) ->
+    Just $ MyMouseMotion pos (eventTimestamp e)
+  _ -> Nothing
+
+makeMyEvent :: Maybe () -> [Event] -> [MyEvent]
+makeMyEvent ma events =
+  let fun b a =
+        case eventToKP a of
+          Nothing -> b
+          Just a' -> a' : b
+      res = reverse (foldl' fun [] events)
+   in case ma of
+        Nothing -> res
+        Just _ -> MyTimeout : res
+
+pattern KBE
+  :: InputMotion
+  -> Keycode
+  -> Bool
+  -> Maybe Window
+  -> Scancode
+  -> KeyModifier
+  -> EventPayload
+pattern KBE press keycode repeat a d f =
+  KeyboardEvent
+    (KeyboardEventData a press repeat (Keysym d keycode f))
+
+initCharCache :: IO CharCacheRef
+initCharCache = newIORef H.empty
+
+getCharTexure :: Renderer -> Font -> CharCacheRef -> Char -> IO Texture
+getCharTexure r font cref c = do
+  cc <- readIORef cref
+  case H.lookup c cc of
+    Nothing -> do
+      surf <- Font.blendedGlyph font (V4 0 255 0 255) c
+      text <- createTextureFromSurface r surf
+      freeSurface surf
+      modifyIORef' cref (H.insert c text)
+      pure text
+    Just t -> pure t
+
+drawString :: DrawEnv -> String -> (Int, Int) -> IO ()
+drawString (DrawEnv r font cref) st (x', y') = do
+  let go _ _ [] = pure ()
+      go x y (t : ts) = do
+        TextureInfo _ _ w h <- queryTexture t
+        copy r t Nothing (Just (Rectangle (P (V2 x y)) (V2 w h)))
+        go (x + w) y ts
+  txts <- mapM (getCharTexure r font cref) st
+  go (fromIntegral x') (fromIntegral y') txts
+
+drawStrings :: DrawEnv -> [String] -> (Int, Int) -> IO ()
+drawStrings de sts (x, y) = do
+  forM_ (zip [0 ..] sts) $ \(i, st) -> do
+    drawString de st (x, y + i * 20)
+
+contains :: Rect -> Point' -> Bool
+contains (Rect rx ry w h) (Point x y) =
+  (rx <= x && x <= rx + w) && (ry <= y && y <= ry + h)
diff --git a/examples/turnstile/Main.hs b/examples/turnstile/Main.hs
new file mode 100644
--- /dev/null
+++ b/examples/turnstile/Main.hs
@@ -0,0 +1,104 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE QualifiedDo #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -Wall #-}
+{-# OPTIONS_GHC -Wno-unused-do-bind #-}
+
+module Main where
+
+import Control.Monad (void)
+import Control.Monad.State
+import qualified Data.Dependent.Map as D
+import Data.Dependent.Sum
+import Data.GADT.Compare (GCompare (..), GEq (..))
+import Data.IFunctor as I
+import Data.Singletons.Base.TH
+import Data.Type.Equality (TestEquality (testEquality))
+import TypedFsm
+
+$(singletons [d|data TurnSt = Locked | Unlocked | Exit deriving (Show, Eq, Ord)|])
+
+instance StateTransMsg TurnSt where
+  data Msg TurnSt from to where
+    Coin :: Msg TurnSt Locked Unlocked
+    Push :: Msg TurnSt Unlocked Locked
+    ExitTurnSt :: Msg TurnSt Locked Exit
+
+instance GEq STurnSt where
+  geq = testEquality
+
+instance GCompare STurnSt where
+  gcompare = sOrdToGCompare
+
+lockedHandler :: Op TurnSt Int IO () Exit Locked
+lockedHandler = I.do
+  msg <- getInput
+  case msg of
+    Coin -> I.do
+      liftm $ do
+        liftIO $ putStrLn "Coin, internal int add one"
+        modify' (+ 1)
+        v <- get
+        liftIO $ putStrLn $ "Now coin: " ++ show v
+      unlockedHandler
+    ExitTurnSt -> I.do
+      liftm $ liftIO $ putStrLn "Exit turnSt"
+
+unlockedHandler :: Op TurnSt Int IO () Exit Unlocked
+unlockedHandler = I.do
+  msg <- getInput
+  case msg of
+    Push -> I.do
+      liftm $ do
+        liftIO $ putStrLn "Push"
+      lockedHandler
+
+eventDepMap :: State2GenMsg TurnSt Int String
+eventDepMap =
+  D.fromList
+    [ SLocked
+        :=> GenMsg
+          ( \_ ev -> case ev of
+              "coin" -> Just $ SomeMsg Coin
+              "exit" -> Just $ SomeMsg ExitTurnSt
+              _ -> Nothing
+          )
+    , SUnlocked
+        :=> GenMsg
+          ( \_ ev -> case ev of
+              "push" -> Just $ SomeMsg Push
+              _ -> Nothing
+          )
+    ]
+
+loop
+  :: Result TurnSt (StateT Int IO) ()
+  -> StateT Int IO ()
+loop res = do
+  case res of
+    Finish _ -> liftIO $ putStrLn "Finish"
+    NotMatchGenMsg singst -> liftIO $ putStrLn $ "NotMatch GenMSg: " ++ show singst
+    Cont sop@(SomeOperate op) -> do
+      st <- liftIO $ do
+        putStrLn $ "current state: " ++ show (getSomeOperateSt sop)
+        putStrLn "input command:"
+        getLine
+      nres <- runOp eventDepMap [st] op
+      loop nres
+
+main :: IO ()
+main = do
+  putStrLn "start loop"
+  void $ runStateT (loop (Cont $ SomeOperate lockedHandler)) 0
diff --git a/src/Data/IFunctor.hs b/src/Data/IFunctor.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/IFunctor.hs
@@ -0,0 +1,99 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+{- | Introducing McBride Indexed Monads
+
+Here's Edward Kmett's [introduction to Indexed Monads](https://stackoverflow.com/questions/28690448/what-is-indexed-monad).
+
+As he said, there are at least three indexed monads:
+
+
+* Bob Atkey
+
+@
+class IMonad m where
+  ireturn  ::  a -> m i i a
+  ibind    ::  m i j a -> (a -> m j k b) -> m i k b
+@
+
+* Conor McBride
+
+@
+type a ~> b = forall i. a i -> b i
+
+class IMonad m where
+  ireturn :: a ~> m a
+  ibind :: (a ~> m b) -> (m a ~> m b)
+@
+
+* Dominic Orchard
+
+No detailed description, just a link to this [lecture](https://github.com/dorchard/effect-monad/blob/master/docs/ixmonad-fita14.pdf)。
+
+I use  the McBride Indexed Monad, the earliest paper [here](https://personal.cis.strath.ac.uk/conor.mcbride/Kleisli.pdf).
+
+The following is my understanding of (\~>): through GADT, let the value contain type information,
+and then use ((\~>), pattern match) to pass the type to subsequent functions
+
+@
+data V = A | B
+
+data SV :: V -> Type where  -- GADT, let the value contain type information
+   SA :: SV A
+   SB :: SV B
+
+data SV1 :: V -> Type where
+   SA1 :: SV1 A
+   SB1 :: SV1 B
+
+fun :: SV ~> SV1     -- type f ~> g = forall x. f x -> g x
+fun sv = case sv of  -- x is arbitrary but f, g must have the same x
+     SA -> SA1       -- Pass concrete type state to subsequent functions via pattern matching
+     SB -> SB1
+
+
+class (IFunctor m) => IMonad m where
+  ireturn :: a ~> m a
+  ibind :: (a ~> m b)  -- The type information contained in a will be passed to (m b),
+                       -- which is exactly what we need: external input has an impact on the type!
+        -> m a ~> m b
+@
+-}
+module Data.IFunctor where
+
+import Data.Data
+import Data.Kind
+
+infixr 0 ~>
+
+type f ~> g = forall x. f x -> g x
+
+class IFunctor f where
+  imap :: (a ~> b) -> f a ~> f b
+
+class (IFunctor m) => IMonad m where
+  ireturn :: a ~> m a
+  ibind :: (a ~> m b) -> m a ~> m b
+
+class (IMonad m) => IMonadFail m where
+  fail :: String -> m a ix
+
+data At :: Type -> k -> k -> Type where
+  At :: a -> At a k k
+  deriving (Typeable)
+
+(>>=) :: (IMonad (m :: (x -> Type) -> x -> Type)) => m a ix -> (a ~> m b) -> m b ix
+m >>= f = ibind f m
+
+{- | (>>)
+
+Note: (>>) can only be used if the type of left `m` is `m (At a j) i`.
+-}
+(>>) :: (IMonad (m :: (x -> Type) -> x -> Type)) => m (At a j) i -> m b j -> m b i
+m >> f = ibind (\(At _) -> f) m
+
+returnAt :: (IMonad m) => a -> m (At a k) k
+returnAt = ireturn . At
diff --git a/src/TypedFsm.hs b/src/TypedFsm.hs
new file mode 100644
--- /dev/null
+++ b/src/TypedFsm.hs
@@ -0,0 +1,50 @@
+{- | This package defines the typed-fsm framework. This module re-exports
+the public API.
+
+FSM stands for [Finite State Machine](https://en.wikipedia.org/wiki/Finite-state_machine).
+
+The typed-fsm is used to define and execute FSM.
+
+Advantages of type-fsm:
+
+* Focus on the right message.
+* Top-to-bottom design for easy refactoring.
+* Conducive to building complex state machine systems:
+** Type guarantees will not produce incorrect function calls when written.
+** With the help of the type system, we can define many state processing functions and then call each other recursively with confidence.
+* There is a sanity check. If you miss some items for pattern matching, the compiler will issue a warning, and there will also be a warning for invalid items.
+
+
+In order to use do syntax, the `QualifiedDo` extension is required.
+
+The QualifiedDo extension allows us to overload only the two operators (>>=) and (>>).
+
+Prior to ghc 9.10.1, this extension had [serious issues](https://gitlab.haskell.org/ghc/ghc/-/issues/21206),
+But this [MR](https://gitlab.haskell.org/ghc/ghc/-/merge_requests/10140) fixes these problems! !
+
+The latest ghc 9.10.1 contains this MR. So this library requires you to update the ghc version to 9.10.1.
+
+Using typed-fsm will go through the following five steps:
+
+1. Define status
+2. Define state transfer messages
+3. Build status processing function
+4. Construct functions from events to messages in different states
+5. Running status processing function
+
+Here are some examples:
+
+1. [turnstile](https://github.com/sdzx-1/typed-fsm/tree/main/examples/turnstile)
+2. [mouse motion](https://github.com/sdzx-1/typed-fsm/tree/main/examples/motion)
+3. [atm](https://github.com/sdzx-1/typed-fsm/tree/main/examples/ATM)
+-}
+module TypedFsm (
+  -- * Defining and implementing FSM
+  module TypedFsm.Core,
+
+  -- * Running FSM
+  module TypedFsm.Driver,
+) where
+
+import TypedFsm.Core
+import TypedFsm.Driver
diff --git a/src/TypedFsm/Core.hs b/src/TypedFsm/Core.hs
new file mode 100644
--- /dev/null
+++ b/src/TypedFsm/Core.hs
@@ -0,0 +1,62 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module TypedFsm.Core where
+
+import Data.IFunctor (
+  At (..),
+  IFunctor (..),
+  IMonad (..),
+  returnAt,
+  type (~>),
+ )
+
+import Data.Kind (Type)
+import Data.Singletons (SingI)
+
+-- | The state-transition type class
+class StateTransMsg ps where
+  data Msg ps (st :: ps) (st' :: ps)
+
+{- | Core AST
+
+Essentially all we do is build this AST and then interpret it.
+
+`Operate m ia st` is an instance of `IMonad`, and it contains an `m` internally
+
+
+Typed-fsm only contains two core functions: `getInput`, `liftm`.
+We use these two functions to build Operate.
+
+The overall behavior is as follows: constantly reading messages from the outside and converting them into internal monads action.
+-}
+data Operate :: (Type -> Type) -> (ps -> Type) -> ps -> Type where
+  IReturn :: ia (mode :: ps) -> Operate m ia mode
+  LiftM
+    :: (SingI mode, SingI mode')
+    => m (Operate m ia mode')
+    -> Operate m ia mode
+  In
+    :: forall ps m (from :: ps) ia
+     . (Msg ps from ~> Operate m ia)
+    -> Operate m ia from
+
+instance (Functor m) => IFunctor (Operate m) where
+  imap f = \case
+    IReturn ia -> IReturn (f ia)
+    LiftM f' -> LiftM (fmap (imap f) f')
+    In cont -> In (imap f . cont)
+instance (Functor m) => IMonad (Operate m) where
+  ireturn = IReturn
+  ibind f = \case
+    IReturn ia -> (f ia)
+    LiftM m -> LiftM (fmap (ibind f) m)
+    In cont -> In (ibind f . cont)
+
+-- | get messages from outside
+getInput :: forall ps m (from :: ps). (Functor m) => Operate m (Msg ps from) from
+getInput = In ireturn
+
+-- | lifts the internal `m a` to `Operate m (At a i) i'
+liftm :: forall ps m (mode :: ps) a. (Functor m, SingI mode) => m a -> Operate m (At a mode) mode
+liftm m = LiftM (returnAt <$> m)
diff --git a/src/TypedFsm/Driver.hs b/src/TypedFsm/Driver.hs
new file mode 100644
--- /dev/null
+++ b/src/TypedFsm/Driver.hs
@@ -0,0 +1,102 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+
+{- | Running FSM
+
+The core function is `runOp`, and the other functions are to make it work properly.
+-}
+module TypedFsm.Driver where
+
+import Control.Monad.State as S (MonadState (get), StateT)
+import Data.Dependent.Map (DMap)
+import Data.Dependent.Map qualified as D
+import Data.GADT.Compare (GCompare, GOrdering (..))
+import Data.IFunctor (At (..))
+import Data.Ord.Singletons (SOrd (sCompare), SOrdering (..))
+import Data.Singletons (Sing, SingI (..), SingKind (..))
+import TypedFsm.Core (Operate (..), StateTransMsg (Msg))
+import Unsafe.Coerce (unsafeCoerce)
+
+data SomeOperate ts m a
+  = forall (i :: ts) (o :: ts).
+    (SingI i) =>
+    SomeOperate (Operate m (At a o) i)
+
+getSomeOperateSt :: (SingKind ts) => SomeOperate ts m a -> Demote ts
+getSomeOperateSt (SomeOperate (_ :: Operate m (At a o) i)) = fromSing $ sing @i
+
+{- | Reuslt of runOp
+
+* Finish, return val a
+* A wrapper for SomeOperate that returns the remaining computation when there is not enough input
+* There is no corresponding GenMsg function defined for some FSM states
+-}
+data Result ps m a
+  = Finish a
+  | Cont (SomeOperate ps m a)
+  | forall t. NotMatchGenMsg (Sing (t :: ps))
+
+{- | `Op` adds new assumptions based on `Operate`: assume that the internal monad contains at least a state monad.
+
+@
+type Op ps state m a o i = Operate (StateT state m) (At a (o :: ps)) (i :: ps)
+@
+
+`Op` contains two states, `ps` and `state`.
+
+`ps` represents the state of the state machine
+`state` represents the internal state.
+
+The external event needs to be converted to Msg.
+
+It is essentially a function `event -> Msg`, but this function is affected by both `ps` and `state`.
+-}
+type Op ps state m a o i = Operate (StateT state m) (At a (o :: ps)) (i :: ps)
+
+newtype GenMsg ps state event from
+  = GenMsg (state -> event -> Maybe (SomeMsg ps from))
+
+type State2GenMsg ps state event = DMap (Sing @ps) (GenMsg ps state event)
+
+data SomeMsg ps from
+  = forall (to :: ps).
+    (SingI to) =>
+    SomeMsg (Msg ps from to)
+
+type SomeOp ps state m a = SomeOperate ps (StateT state m) a
+
+sOrdToGCompare
+  :: forall n (a :: n) (b :: n)
+   . (SOrd n)
+  => Sing a -> Sing b -> GOrdering a b
+sOrdToGCompare a b = case sCompare a b of
+  SEQ -> unsafeCoerce GEQ
+  SLT -> GLT
+  SGT -> GGT
+
+runOp
+  :: forall ps event state m a (input :: ps) (output :: ps)
+   . ( SingI input
+     , GCompare (Sing @ps)
+     )
+  => (Monad m)
+  => State2GenMsg ps state event
+  -> [event]
+  -> Operate (StateT state m) (At a output) input
+  -> (StateT state m) (Result ps (StateT state m) a)
+runOp dmp evns = \case
+  IReturn (At a) -> pure (Finish a)
+  LiftM m -> m Prelude.>>= runOp dmp evns
+  In f -> do
+    let singInput = sing @input
+    case D.lookup singInput dmp of
+      Nothing -> pure (NotMatchGenMsg singInput)
+      Just (GenMsg genMsg) -> loop evns
+       where
+        loop [] = pure $ Cont $ SomeOperate (In f)
+        loop (et : evns') = do
+          state' <- get
+          case genMsg state' et of
+            Nothing -> loop evns'
+            Just (SomeMsg msg) -> runOp dmp evns' (f msg)
diff --git a/typed-fsm.cabal b/typed-fsm.cabal
new file mode 100644
--- /dev/null
+++ b/typed-fsm.cabal
@@ -0,0 +1,171 @@
+cabal-version:      3.0
+-- The cabal-version field refers to the version of the .cabal specification,
+-- and can be different from the cabal-install (the tool) version and the
+
+-- version used must be equal or greater than the version stated in this field.
+-- Starting from the specification version 2.2, the cabal-version field must be
+-- the first thing in the cabal file.
+
+-- Initial package description 'typed-fsm' generated by
+-- 'cabal init'. For further documentation, see:
+--   http://haskell.org/cabal/users-guide/
+
+-- The name of the package.
+name:               typed-fsm
+
+-- The package version.
+
+-- guiding when and how versions should be incremented.
+-- https://pvp.haskell.org
+-- PVP summary:     +-+------- breaking API changes
+--                  | | +----- non-breaking API additions
+--                  | | | +--- code changes with no API change
+version:            0.1.0.0
+
+-- A short (one-line) description of the package.
+synopsis: A framework for strongly typed FSM
+
+-- A longer description of the package.
+description:
+  FSM stands for [Finite State Machine](https://en.wikipedia.org/wiki/Finite-state_machine).
+  The typed-fsm is used to define and execute FSM.
+
+  Advantages of type-fsm:
+
+  * Focus on the right message.
+  * Top-to-bottom design for easy refactoring.
+  * Conducive to building complex state machine systems:
+  ** Type guarantees will not produce incorrect function calls when written.
+  ** With the help of the type system, we can define many state processing functions and then call each other recursively with confidence.
+  * There is a sanity check. If you miss some items for pattern matching, the compiler will issue a warning, and there will also be a warning for invalid items.
+-- The license under which the package is released.
+license:            MIT
+
+-- The file containing the license text.
+license-file:       LICENSE
+
+-- The package author(s).
+author:             sdzx-1
+
+-- An email address to which users can send suggestions, bug reports, and patches.
+maintainer:         shangdizhixia1993@163.com
+-- A copyright notice.
+-- copyright:
+category:           Control
+build-type:         Simple
+
+-- Extra doc files to be distributed with the package, such as a CHANGELOG or a README.
+extra-doc-files:    CHANGELOG.md
+
+-- Extra source files to be distributed with the package, such as examples, or a tutorial module.
+-- extra-source-files:
+
+flag BuildExample
+  description: Build examples
+  default: False
+
+common warnings
+    ghc-options: -Wall
+
+library
+    -- Import common warning flags.
+    import:           warnings
+
+    -- Modules exported by the library.
+    exposed-modules: TypedFsm
+                   , TypedFsm.Core
+                   , TypedFsm.Driver
+                   , Data.IFunctor
+
+    -- Modules included in this library but not exported.
+    -- other-modules:
+
+    -- LANGUAGE extensions used by modules in this package.
+    -- other-extensions:
+
+    -- Other library packages from which modules are imported.
+    build-depends: base >=4.20.0.0 && < 5
+                 , dependent-map ^>= 0.4.0.0
+                 , dependent-sum ^>= 0.7.2.0
+                 , mtl ^>= 2.3.1
+                 , singletons-base ^>= 3.4
+
+    -- Directories containing source files.
+    hs-source-dirs:   src
+
+    -- Base language which the package is written in.
+    default-language: GHC2021
+
+executable motion
+  if !flag(BuildExample)
+    buildable: False
+  build-depends: base >=4.20.0.0
+               , typed-fsm
+               , sdl2 ^>= 2.5.5.0
+               , sdl2-ttf ^>= 2.1.3
+               , mtl >= 2.3.1
+               , stm ^>= 2.5.3.1
+               , linear ^>= 1.22
+               , unordered-containers ^>= 0.2.20
+               , dependent-map >= 0.4.0.0
+               , dependent-sum >= 0.7.2.0
+               , containers ^>= 0.7 
+               , microlens ^>= 0.4.0.0
+               , microlens-mtl ^>= 0.2.0.3
+               , microlens-th ^>= 0.4.3.15
+               , singletons-base >= 3.4
+  main-is: Main.hs
+  default-language: Haskell2010
+  hs-source-dirs: examples/motion
+  other-modules: Utils
+               , Handler
+               , Type
+               , EventToMsg
+  ghc-options: -threaded -Wall
+
+executable atm
+  if !flag(BuildExample)
+    buildable: False
+  build-depends: base >=4.20.0.0
+               , typed-fsm
+               , unordered-containers ^>= 0.2.20
+               , dependent-map >= 0.4.0.0
+               , dependent-sum >= 0.7.2.0
+               , containers ^>= 0.7
+               , microlens ^>= 0.4.0.0
+               , microlens-mtl ^>= 0.2.0.3
+               , microlens-th ^>= 0.4.3.15
+               , mtl >= 2.3.1
+               , sdl2 ^>= 2.5.5.0
+               , sdl2-ttf ^>= 2.1.3
+               , mtl >= 2.3.1
+               , stm ^>= 2.5.3.1
+               , linear ^>= 1.22
+               , unordered-containers
+               , singletons-base >= 3.4
+  main-is: Main.hs
+  default-language: Haskell2010
+  hs-source-dirs: examples/ATM
+  other-modules: Type
+               , Handler
+               , EventToMsg
+               , Utils
+  ghc-options: -Wall
+
+executable turnstile
+  if !flag(BuildExample)
+    buildable: False
+  build-depends: base >=4.20.0.0
+               , typed-fsm
+               , dependent-map >= 0.4.0.0
+               , dependent-sum >= 0.7.2.0
+               , mtl >= 2.3.1
+               , singletons-base >= 3.4
+  main-is: Main.hs
+  default-language: Haskell2010
+  hs-source-dirs: examples/turnstile
+  ghc-options: -Wall
+
+source-repository head
+  type:     git
+  location: https://github.com/sdzx-1/typed-fsm