About a month ago, I started working on a complete reimplementation of Idris, because there are a number of things about the current implementation that have been bothering me for a while. It’s now got to a point where it’s beginning to work (in particular, the standard well-typed interpreter is up and running). You can start playing with it now, and follow progress at the github repository.
I’m usually very reluctant to start something again – especially so with Idris since I’ve been working on it for a few years now. But there’s quite a few problems with the current design. In fact, “design” is too strong a word – I didn’t really know when I started what I wanted the language to do and which features I’d need. Moreover, it’s evolved out of a theorem proving system Ivor that was originally meant to do something else, and it’s getting harder and harder to add the new features I want (e.g. mod cons like
where clauses, destructuring
case, and essential gadgets for developing large systems like separate compilation and a decent module system) without having to jump through hoops.
Pleasingly, the new version is not far off catching up with where the old version was. Basic syntax, type checking with implicit syntax and evaluation are all working (mostly better than before…) There is no
with rule yet, but it won’t be long. There’ll be a compiler not long after I’ve decided how to handle IO (I want to keep the IO primitives as primitive as I can so that it will be possible to experiment with different high level representations).
The main, significant, distinction between the previous implementation and this is the type checker. In the new version, the type checker is kept extremely simple – no implicit syntax, no unification, no generating proof obligations or coercions. Instead, we have a core type theory with metavariables, and an EDSL (that is, an embedded domain specific language) called
Elab which constructs programs using Coq-style tactics, directed by the high level source text, and filling in metavriables by unification where it can. This idea will be unsurprising to anyone who is following the progress of Epigram.
Elab an EDSL has several advantages. Adding a new language construct (e.g. pattern matching, now, or maybe coercions, or type classes, some day…) is simply a matter of writing a sequence of tactics to build that construct in the core type theory. To check a pattern match clause, for example, we elaborate the left hand side inferring types for the pattern variables as we go, and use this information to elaborate the right hand side. Another advantage is that it will be easy to expose the EDSL to an Idris programmer for building domain specific decision procedures (e.g. a Ring Solver would be nice). Finally, making the elaborator do all of the work and keeping the type checker simple means that we can be far more confident that only well-typed programs are accepted.
I’ll go back into my hacking shed now, and I’m staying there until all the programs that worked with the previous version compile. Hopefully this won’t take long :). In the meantime, if you have a go, please let me know what you come up with. In particular, if anything behaves badly, please shout – I want this version to work well!