Dependent Types, and a "Wow" moment

While scanning LtU for articles I had missed, I found Why Dependent Types Matter. I've come across Epigram before, and I was charmed by the idea of programming by choosing a problem-solving technique and then filling in the blanks. However, at that time they hadn't implemented general recursion yet, so my interest level dropped substantially and I decided to ignore the language until it had matured a bit more.

This newest Epigram paper, however, is very interesting. When I got to section 4.1, I had a "Wow!" moment as I finally understood what they meant by "the point of writing a proof in a strongly normalizing calculus is that you don't need to normalize it". This means that they can express statements about expressions and prove that they hold in all cases -- and then the compiler can just rely on the existence proof, without actually having to do any work at runtime.

For example, they prove the trivial rewrite rule "m+(1+n) = 1+(m+n)", via induction on the natural numbers. The proof is simple, but the really amazing part is that because they've expressed the proof in a way that the typechecker can understand, they can use it to rewrite expressions without having to pay any runtime cost. The truly elegant part of this is that the proof is done with almost exactly the same language as is used for regular computation. This really makes the Curry-Howard isomorphism start to feel concrete, to me.

For the weak of heart, they point out that these kinds of proofs are optional -- if you don't want to go through the work, you can just use less precise types, and then programming in Epigram shouldn't be much more difficult than programming in any other strongly-typed functional language.

In section 5, the paper suggests that dependent types can help nail down the specification of a program to the point where the type system will prevent you from replacing subexpressions of the same type (e.g. swapping the true- and false-branch of an if statement). This seems to me to be a static version of tools like Jester, which measures test coverage by searching for code mutations that don't trigger test suite failures. The drawback to tools like Jester is that you may have to run the entire test suite for every mutation -- and with an average of 1 mutation for every 15 lines of code, that can take a very long time. A static version of this seems quite interesting to me, even if it does require thinking hard about how to prove various properties. It's unfortunate, however, that such proofs requiring mucking with the original definition, and changing its type.

If only I wasn't also trying to get through Types and Programming Languages, while also trying to become more familiar with MzScheme and FrTime, while also working full time, I'd love to download Epigram and play around with it a bit. Maybe someday :) I suppose my next step will be to read more about GADTs.

Followups to Dependent Types, and a "Wow" moment:

• It's all connected
• It's all connected

Posted on September 28, 2005 04:29 PM
More languages articles