#dependent types

It’s the first time since I first checked out Rust that I’ve been this excited about a programming language. Idris doesn’t strike me as super practical at this point, but the pieces seem to hang together very well, and there’s lots of good work for other languages to build on.

If you feel pretty comfortable with Haskell and are looking for something like it but that fixes its main mistakes (e.g. strict by default) and with a type system with a bunch of fun new stuff on top, Idris is for you!

One of the most annoying things about creating a new programming language is generating code for it. Optimizations take a long time to develop, so it takes a long time before a compiler which does code generation from scratch to catch up to a highly optimizing compiler like GHC's.

When your language is sufficiently similar to that of an existing one, you can often compile into their intermediate representation, and let their optimization passes take care of things from there. A number of language do this with GHC Core, compiling their code into Core and then letting the optimizer take care of things from there.

However, how do you go about implementing this transformation when your language has a more expressive type system than System F with coercions? The trouble arises when you have types which you know are equal, but cannot express the evidence of equality in the coercion language.

Traditional extraction to Haskell/ML from dependently typed languages often makes use of unsafeCoerce/Object.magic to manage these cases, but too much use of these impedes optimization. Another possibility is to generate additional axioms to represent coercions that would otherwise not be safe.