Flying Spaghetti Monster - Type Systems and Microservices
summary
Argues that expressive Idris dependent types can verify distributed protocols, preventing illegal state transitions and some classes of deadlock by encoding protocols as finite state machines and enforcing them at compile time. Shows index monads/dominoes for sequencing, models failure and nondeterminism in types, and demonstrates type providers that import a vending-machine spec into types (proof‑of‑concept on GitHub). Explains session types for projecting global protocols to local roles so complementary actions compose safely.
AI-written summary · about
chapters (22)
- 0:00Introduction
- 2:38David Kristensen
- 3:49Microservices
- 6:02Common Lisp
- 7:00Microservice Architecture
- 7:42Narrative is not enough
- 8:52Finite State Machines
- 10:45Indexmonads
- 13:02Network Boundary
- 14:42The White Space
- 16:12Availability
- 18:49Domino
- 19:52Type Providers
- 22:31Reciprocity
- 22:47Session Types
- 23:12Projection
- 23:43AcceptSelect
- 24:32Dual
- 26:31Complimentary State
- 27:03Conclusion
- 29:24Code Mesh
- 30:24References
related talks
43mTowards Language Support for Distributed Systems
38mMonolith vs. Microservices
44mBuilding event-driven microservices with Scala and Functional Domain Models
49mPractical Eff monad for microservices
59mImplementing Event-Driven Microservices architecture in Functional language
58mImmutable Patterns of System Design; From Monolith to Agentic AI
46mSimplifying Microservices: The art of effortless development
36mFreestyle: A framework for pure functional apps, libs and microservices