Quantitative Types in Idris 2
summary
A new Idris 2 core implements Quantitative Type Theory (Conor McBride, Bob Atkey) with concrete multiplicities 0 1 ω, enabling dependent+linear types. The implementation boots from Chez Scheme (build shown at 4m41s) and runs examples that work: type-driven synthesis finds the intended rep implementation first among 16 candidates; a run‑length uncompress uses zero multiplicity to keep compressed data erased at runtime; a linear secure‑store protocol and a linear socket API encode state transitions in types so resource protocols are enforced at compile time.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 1:54What is Idris
- 4:15Quantitative Types
- 6:24Interactive Editing
- 18:51Code
- 28:41Network Socket API
- 30:46IO primitives
- 38:15Summary
related talks
41mPrograms and Proofs — Dependent Typing as a Way to Structure Your Code
41mType-driven Development of Communicating Systems in Idris
25mLinear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl)
47mType-Driven Development in Idris
53mIntroduction to Intuitionistic Type Theory
41mFun With Categories
28mQuotient Polymorphism
25mIs Sized Typing for Coq Practical?