Dependent Type Driven Program Synthesis in Idris

Idris is a functional programming language with first-class types, where types may be parameterised by other values. This allows us to give increasingly precise specifications for functions, and be more confident in their correctness. But, perhaps more importantly, it gives the language implementation more information up front about what a function should do. Therefore, we can use Idris as an interactive assistant, and treat programming as a conversation with the machine.

In particular, the Idris system supports program synthesis, generating (fragments of) programs from types. In this talk, I will show the current state of program synthesis in Idris, outline how it works, and discuss some possible future research directions.