"No Foul Play" Describing State with Dependently Typed FSMs
summary
Claim: types encode the full snooker state and prevent illegal plays at compile time. Implementation uses Idris and encodes counts (e.g. 15 reds) as type-level naturals so transitions must match exactly. The finite state machine models phases and fouls by making next-state a function of the shot result; illegal sequences fail to typecheck. Examples include a type-level N‑Queens solution and a working snooker break model that compiles and enforces the rules.
AI-written summary · about
chapters (15)
- 0:00Intro
- 1:30Type Systems
- 2:40Type-Level Programming
- 3:25Generic Types as Type Functions
- 5:50Peano numbers
- 9:38printf
- 12:20n-Queens
- 14:55Snooker Types
- 16:51Break Sequence
- 17:40Finite State machines
- 22:22Counting the Reds
- 24:35The Two Phases
- 29:13Foul Handling
- 37:44Analogy mapping
- 39:06What's next?
related talks
46mFinite-state machines? Your compiler wants in!
20mTaming UI complexity with Typed State Machines
35mFlying Spaguetti Monster: Verifying protocols with types and finite state machines
33mHow Not to Shoot Yourself in the Foot with a Finite State Machine
44mManaging Complex Application State with Finite-State Machines
28mState machines for frontend state management
25mMastering UIs with Finite State Machines
01h 13mModernizing Finite State Machines in C++ - Empower Simplicity & Boost Performance With std::variant