Finite state machines
summary
Claim: encoding FSMs into the type system catches real bugs and lets the compiler enforce transitions. Implementations use Haskell and PureScript implementations with ADT and MTL-style classes, an indexed-monad runner that forbids double-use, and PureScript row kinds to compose named machines. A checkout and a flight-reservation demo run with IO side effects interleaved (prints charging and logs). An Idris version uses Idris-dependent types to track item counts and prove correctness. Libraries and examples exist for reuse: index monads and row kinds.
AI-written summary · about
chapters (20)
- 0:00Introduction
- 1:28State
- 2:33Finite state machines
- 4:33algebraic data types
- 10:02MTL style
- 12:13Checkout type
- 18:37ConcreteStay type
- 19:56CheckoutT
- 21:50Timeouts
- 24:42Summary
- 27:18Index monads
- 30:38Row kinds
- 31:55Indexmonads
- 33:41Type signatures
- 34:48Dependent types
- 36:23Read stuff
- 37:06Protocol
- 40:28Select More
- 40:53Check Out
- 43:09Conclusion
