A Tutorial Implementation of a Dependently Typed Lambda Calculus Andres Löh, Conor McBride and Wouter Swierstra We present the type rules for a dependently-typed core calculus together with a straightforward implementation in Haskell. We explicitly highlight the changes necessary to shift from a simply-typed lambda calculus to the dependently-typed lambda calculus. We also describe how to extend our core language with data types and write several small example programs. The paper is accompanied by an executable interpreter and example code that allows immediate experimentation with the system we describe. Download Draft Paper (submitted to FI) Haskell source code (executable Haskell file containing all the code from the paper plus the interpreter; automatically generated from the paper sources) prelude.lp (prelude for the LambdaPi interpreter, containing several example programs) Instructions (how to get started with the LambdaPi interpreter)
The Haskell project was begun in order to unify "more than a dozen non-strict, purely functional programming languages". (mirror) We are rapidly approaching that many viable choices for programming with dependent types. 1. Epigram 2. ATS (successor to Dependent ML) 3. Agda (successor to Cayenne) 4. Ωmega 5. NuPrl 6. Twelf 7. Isabelle 8. Coq etc caveats * Some of the items on this list are theorem provers first and dependently-typed programming languages second. Adam Chlipala argues that this is not such a problem for Coq. * Some of these choices may not be real options for programing with dependent types. Twelf is designed for programming about programming languages, and, if I remember correctly, doesn't have parametric polymorphism because of something having to do with higher-order abstract syntax. Is it time yet to do anything about the cornucopia of options? see comments