Abstract

Idris is a general purpose pure functional programming language with dependent types. Dependent types allow types to be predicated on values, meaning that some aspects of a program’s behaviour can be specified precisely in the type. It is compiled, with eager evaluation. Its features are influenced by Haskell and ML, and include:

• Full dependent types with dependent pattern matching
• Simple foreign function interface (to C)
• Compiler-supported interactive editing: the compiler helps you write code using the types where clauses, with rule, simple case expressions, pattern matching let and lambda bindings
• Dependent records with projection and update
• Interfaces (similar to type classes in Haskell)
• Type-driven overloading resolution do notation and idiom brackets
• Indentation significant syntax
• Extensible syntax
• Cumulative universes
• Totality checking
• Hugs style interactive environment

Idris is a general purpose functional programming language with full dependent types, building on state-of-the-art techniques in programming language research. It encourages “Type Driven Development”, in which we begin by stating a function’s type, and arrive at a working program by a series of refinements.

We’ve been having lots of fun over the last couple of years investigating the possibilities and limitations of type-driven development in Idris. As we write larger programs, though, we’re finding the implementation of Idris is showing the strain – and recently I decided the time was right to start again, and implement Idris 2 in Idris. In this talk, I’ll give an introduction to type-driven development (in Idris 2) and report on progress so far, showing off the most interesting features which the new design enables. In particular, I will show examples of how Idris 2 combines linear types and dependent types.