[goless]

I once wrote a library typed-fsm https://github.com/sdzx-1/typed-fsm

It has a completely type-safe finite state machine, and it does not require additional programming conventions.

It relies on a special monad: Mcbride Indexed Monad, which can model uncertainty in terms of type.

Are you using this monad here?

Here is a concrete ATM demo https://github.com/sdzx-1/typed-fsm/tree/main/examples/ATM

[goless]

In fact, relying on this monad, we can achieve full type safety for multi-role communication.

https://github.com/sdzx-1/typed-session