In our second episode, we speak with Edwin Brady from the University of St. Andrews. Since 2008, Edwin has been working on Idris, a functional programming language with dependent types. This episode is very much about programming: we discuss the language Idris, its history, its implementation strategies, and plans for the future.
Reading:
- Inductive Families Need Not Store Their Indices by Edwin Brady, Conor McBride and James McKinna, TYPES 2003
- Practical Implementation of a Dependently Typed Functional Programming Language by Edwin Brady. PhD thesis, 2005
- Ivor, a Proof Engine by Edwin Brady
- Simply Easy! An Implementation of a Dependently Typed Lambda Calculus by Andres Löh, Conor McBride and (ahem) Wouter Swierstra
- Simpler! Easier! by Lennart Augustsson
- Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation by Edwin Brady. Journal of Functional Programming volume 23 issue 5, September 2013, pp. 552-593
Resources:
- The Idris homepage, with links to mailing lists, Git repository, tutorial, etc
- The idris-hackers organization on Github, with tools and libraries
- Download:
- AAC43 MB
- MP357 MB
- FLAC216 MB