Dependent Type Driven Program Synthesis in Idris
summary
Idris uses the type to synthesize program fragments by incremental case-splitting and expression search over holes and unification, generating batches (default 16) and ranking candidates by most-local-variables-used. It builds real code (repeat, HList lookup, continuation monad including call/cc, run-length encoder) and fixes parts of the Idris 2 compiler like modular name choices. Results are type-correct, often useful but sometimes syntactically ugly; the engine is simple, editor-driven, and practical for real code.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:06Type Driven Program Synthesis
- 4:03Questions
- 4:41Examples
- 11:04Basic Plumbing
- 13:08Dependently typed programs
- 19:19Optimized data structure
- 23:09Continuation Monad
- 25:47Call with Current Continuation
- 26:57How it Works
- 29:07Expression Search
- 31:15Program Search
related talks
43mIdris 2: Type-driven development of Idris
24mImperative Syntax for Dependent Types
41mPrograms and Proofs — Dependent Typing as a Way to Structure Your Code
32mHole Refinements for Polymorphic Type-and-Example Driven Synthesis
12mIdris2-Table: Evaluating dependently-typed tables with... (Extended Abstract)
01h 06mKeynote – Edwin Brady
31mDependent tagless final
30mConstrained generation of well-typed programs