Idris 2: Type Driven Development of Idris

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

• Edwin Brady, St Andrews University
• Tuesday 27 November 2018, 11:00-12:00
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.