Typed finite state machine!

[sdzx-1]

Hi everyone, I have developed a new library typed-fsm.
It allows writing typed finite state machines.
It has many advantages:

1. Focus on the right message

2. Top-to-bottom design for easy refactoring

3. 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.

4. 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.

Detailed explanation here.
Do you have any suggestions?

[polux]

Nice library! In case you’d had a look at it already , would you mind explaining how it compares to motor: Type-safe effectful state machines in Haskell?

[sdzx-1]

I don’t fully understand motor.

But I feel that the motor uses the Bob Atkey Indexed Monad.

typed-fsm uses Conor McBride Indexed Monad.

I feel that for fsm, McBride Indexed Monad is the more correct choice.

More detailed instructions here

Indexed Monad

[sdzx-1]

Complete ATM example.
Tracks the number of checkPin attempts on the type, statically guaranteeing no more than three attempts.|

confidence-in-types

start ATM
-> current ATMSt: Ready
ins card
-> current ATMSt: CardInserted Z
checkPin 1
-> current ATMSt: CardInserted (S Z)
checkPin 2
-> current ATMSt: CardInserted (S (S Z))
checkPin 3
-> test 3 times, eject card!
-> current ATMSt: Ready
ins card
-> current ATMSt: CardInserted Z
checkPin 1234
-> current ATMSt: Session
getAmount
-> User Amount: 1000
-> current ATMSt: Session
dispense 100
-> Use dispense 100
-> Now User Amount: 900
-> current ATMSt: Session
dispense 100
-> Use dispense 100
-> Now User Amount: 800
-> current ATMSt: Session
eject
-> current ATMSt: Ready

[sdzx-1]

typed-fsm

[sdzx-1]

Advantages of type-fsm

Advantages of type-fsm example code Focus on the right message The FSM receives messages and changes state. When in a different state, it will only receive messages that are appropriate for that state. Any messages that do not belong to that state will be detected by the compiler and a warning will be issued. The compiler will also issue a warning if a certain type of message is not processed. [image] Top-to-bottom design for easy refactoring In typed-fsm, messages that drive state change…

[ocramz]

Thanks for the pointers!

I don’t quite follow McBride’s rationale (as often is the case) in haskell - What is indexed monad? - Stack Overflow , re. modeling an unpredictable (externally-driven) transition. Do you have some insight on this?

[sdzx-1]

@ocramz

modeling an unpredictable (externally-driven) transition

Mcbride Indexed Monad can solve this problem!

The core difference between Atkey Indexed Monad and Mcbride Indexed Monad

Bob Atkey Indexed Monad

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 Indexed Monad

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)

(a -> m j k b) and (a ~> m b), both mean constructing a new m based on the result of the previous step.

The difference is:

(a -> m j k b), a does not pass any type information to (m j k b)

(a ~> m b), a passes the specific type state to (m b) through pattern matching

---

Here is an example Turnstile.

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"

Its type is passed as follows: