Type-driven Development of Communicating Systems in Idris
summary
Idris uses dependent types and totality checking to make concrete claims: total functions terminate or produce finite prefixes of infinite results, and IO is described as terminating actions under a delayed/productive wrapper. The demo builds a mailbox/channel concurrency DSL (an adder server example) that enforces request→response types and per-loop productivity, uses a fuel parameter to run infinite behaviors, and the interpreter and type machinery fit in 90 lines of code and typecheck and run as shown.
AI-written summary · about
chapters (7)
- 0:00Start
- 2:55What Is Time Development
- 4:21Type Driven Development
- 13:14Non Terminating Statement
- 19:58Interactive Programs
- 28:04Idris Runtime System
- 28:46Dynamic Type Checking
