University of Cambridge > > Microsoft Research Cambridge, public talks > Idris 2: Type Driven Development of Idris

Idris 2: Type Driven Development of Idris

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

 Please note, this event may be recorded. Microsoft will own the copyright of any recording and reserves the right to distribute it as required.

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.

This talk is part of the Microsoft Research Cambridge, public talks series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity