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
I’ve been working on file handling and concurrency recently, using the type system to manage state to prevent unauthorised access to resources and to ensure locks are managed correctly, even looking at how types can help prevent deadlock. I’ve been doing this in Ivor, but I think now is the time to give it a go in a real language. To this end… …I’ve spent the last few weeks hacking on a fledgling dependently typed language called Idris. It has full dependent types, pattern matching, and some basic IO with Haskell style do notation. I’ve tried a few simple examples, including the traditional well-typed interpreter. Types need to be given for pattern matching functions, but can often be omitted for constants - full type inference is of course impossible with full dependent types.