# Typed finite state machine!

**URL:** <https://discourse.haskell.org/t/typed-finite-state-machine/9324>\
**Category:** Announcements\
**Created:** [April 14, 2024, 4:04am UTC](https://discourse.haskell.org/t/typed-finite-state-machine/9324 "2024-04-14T04:04:16Z")\
**Posts on this page:** 8\
**Page:** 1

<div class="post-metadata">

**Author:** ![sdzx-1](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/sdzx-1/32/4258_2.png) [@sdzx-1](https://discourse.haskell.org/u/sdzx-1)\
**Post date:** [April 14, 2024, 4:04am UTC](https://discourse.haskell.org/t/typed-finite-state-machine/9324/1 "2024-04-14T04:04:16Z")

</div>

Hi everyone, I have developed a new library [typed-fsm](https://github.com/sdzx-1/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

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](https://github.com/sdzx-1/typed-fsm/blob/main/more-en.md).  
Do you have any suggestions?

---

<div class="post-metadata">

**Author:** ![polux](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/polux/32/5496_2.png) [@polux](https://discourse.haskell.org/u/polux)\
**Post date:** [April 14, 2024, 5:44am UTC](https://discourse.haskell.org/t/typed-finite-state-machine/9324/2 "2024-04-14T05:44:28Z")

</div>

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](https://hackage.haskell.org/package/motor)?

---

<div class="post-metadata">

**Author:** ![sdzx-1](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/sdzx-1/32/4258_2.png) [@sdzx-1](https://discourse.haskell.org/u/sdzx-1)\
**Post date:** [April 14, 2024, 1:31pm UTC](https://discourse.haskell.org/t/typed-finite-state-machine/9324/3 "2024-04-14T13:31:09Z")

</div>

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](https://github.com/sdzx-1/typed-fsm/blob/main/more-en.md)

[Indexed Monad](https://stackoverflow.com/questions/28690448/what-is-indexed-monad)

---

<div class="post-metadata">

**Author:** ![sdzx-1](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/sdzx-1/32/4258_2.png) [@sdzx-1](https://discourse.haskell.org/u/sdzx-1)\
**Post date:** [April 16, 2024, 3:27am UTC](https://discourse.haskell.org/t/typed-finite-state-machine/9324/4 "2024-04-16T03:27:47Z")

</div>

[Complete ATM example](https://github.com/sdzx-1/typed-fsm/tree/main/examples/ATM).  
Tracks the number of checkPin attempts on the type, statically guaranteeing no more than three attempts.|

 ![atm](https://us1.discourse-cdn.com/flex002/uploads/haskell/original/2X/0/051deb04430bd3bb61d7923ed64e79ac66d65bb4.png)  
[confidence-in-types](https://github.com/CodingCellist/talks/blob/main/2024-03-06-spls-st-andrews/confidence-in-types.pdf)

```shell
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

```

---

<div class="post-metadata">

**Author:** ![sdzx-1](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/sdzx-1/32/4258_2.png) [@sdzx-1](https://discourse.haskell.org/u/sdzx-1)\
**Post date:** [July 18, 2024, 1:06pm UTC](https://discourse.haskell.org/t/typed-finite-state-machine/9324/5 "2024-07-18T13:06:16Z")

</div>

> **[typed-fsm](https://hackage.haskell.org/package/typed-fsm)**
>
> A framework for strongly typed FSM

---

<div class="post-metadata">

**Author:** ![sdzx-1](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/sdzx-1/32/4258_2.png) [@sdzx-1](https://discourse.haskell.org/u/sdzx-1)\
**Post date:** [July 18, 2024, 1:09pm UTC](https://discourse.haskell.org/t/typed-finite-state-machine/9324/6 "2024-07-18T13:09:15Z")

</div>

> [@Advantages of type-fsm](http://discourse.haskell.org/t/advantages-of-type-fsm/9679):
>
> Advantages of [type-fsm](https://github.com/sdzx-1/typed-fsm/tree/main)[example code](https://github.com/sdzx-1/typed-fsm/blob/main/examples/motion/Handler.hs)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…

---

<div class="post-metadata">

**Author:** ![ocramz](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/ocramz/32/3713_2.png) [@ocramz](https://discourse.haskell.org/u/ocramz)\
**Post date:** [July 19, 2024, 2:31am UTC](https://discourse.haskell.org/t/typed-finite-state-machine/9324/7 "2024-07-19T02:31:32Z")

</div>

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](https://stackoverflow.com/questions/28690448/what-is-indexed-monad) , re. modeling an unpredictable (externally-driven) transition. Do you have some insight on this?

---

<div class="post-metadata">

**Author:** ![sdzx-1](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/sdzx-1/32/4258_2.png) [@sdzx-1](https://discourse.haskell.org/u/sdzx-1)\
**Post date:** [July 19, 2024, 5:26am UTC](https://discourse.haskell.org/t/typed-finite-state-machine/9324/8 "2024-07-19T05:26:55Z")

</div>

> [@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

```haskell
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

```haskell
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](https://github.com/sdzx-1/typed-fsm/tree/main/examples/turnstile).

```haskell
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:

 ![detail](https://us1.discourse-cdn.com/flex002/uploads/haskell/original/2X/6/69bf8a83f53417bc54d27aa8b3000b12bdc8336b.png)