Idris 2: Type-driven development of Idris
summary
A new implementation rewrites the language in itself: Idris 2 implemented in Idris, with an interactive editor workflow (Atom protocol) that drives development by filling editor-driven holes and synthesizing code. It adds linear types via quantitative type theory (0/1/many annotations) to track resource usage and enable safer APIs and state machines. Demos show dependent examples (printf-like format checking, vectors: append/zip/transpose), a door state DSL, and a Scheme backend that surprisingly outperforms Idris 1 and some GHC micro-benchmarks.
AI-written summary · about
chapters (11)
- 0:00Start
- 0:29Type Driven Development
- 3:49Quantitative Type Theory
- 4:16Live Demo
- 4:54Lessons in the Fundamentals of Go
- 5:26Fundamentals of of First Class Types
- 5:48Editor Interaction Protocols
- 7:40Function Type Signatures
- 11:50Vectors
- 25:10Resource Usage
- 26:49Matrix Transposition
related talks
39mDependent Type Driven Program Synthesis in Idris
01h 06mKeynote – Edwin Brady
24mImperative Syntax for Dependent Types
58mPanel discussion: Types for All: From weak to strong, from static to dynamic
12mIdris2-Table: Evaluating dependently-typed tables with... (Extended Abstract)
41mPrograms and Proofs — Dependent Typing as a Way to Structure Your Code
31mYaffle: A New Core for Idris 2
20mFirst-class Algebraic Presentations with Elaborator Reflection (Extended Abstract)