Idris 2: Type-Driven Development with Edwin Brady

Code Sync · Talk · YouTube title: Edwin Brady - Idris 2: Type-driven development of Idris | Code Mesh LDN 18

Why it's here

HN points to it as a good introduction to Idris 2 and a striking demonstration of what dependent types enable.

What it covers

Edwin Brady presents Idris 2, a rewrite of the Idris dependently typed language, and shows type-driven development in practice. The demos show the compiler filling in whole functions from their types.