The Dependent Types Project

I should just say at this point that the dependent types project goes much further than me. So I've been using a lot of my time over the past many years to sort of push this along. In terms of these design challenges, I think they sort of keep us honest. There's other dependently typed languages out there. They tend to require a lot more type annotations than Haskell does. The desire to keep old programs working means that we have to sort of think hard about type inference in a way that other dependently typing languages haven't had to think. And so that is, I think, quite an interesting constraint and one that pushes the science of programming language design forward.