Types and Tailcalls

Getting Started With Dependent Types

published on July 31, 2013

Dependent types, that is type systems where types may depend on values, are the hot new thing. Dependent types seem like a logical succession to Haskell, which people much smarter than me argue is becoming a dependently typed language itself. I am interested in learning more about dependent types and want to list some resources here that I have used or am planing on using.

Why dependent types?

Why bother learning languages with dependent types? Given that I’ve argued that it is beneficial to encode a program’s invariants in the type system, it is only natural to want a type system that allows you to do more of this. Dependent types give you this possibilitye, however there is a trade off: writing programs in dependently typed languages is more complex (you may have to write some proofs!) and we don’t have that much experience with it.

I can’t really answer the question if the more powerful type system is worth the additional difficulties, but it seems like things are in motion and that now is an interesting time to find out:

It is of course quite possible that these indications mean nothing or that it simply looks like a trend to me since I have only recently started to look at this topic. However, if Haskell has taught me one thing then it is that great ideas, however different, may eventually become successful when pursued with the necessary tenacity and that things that look like huge inconveniences (purity!) may actually turn out to be great advantages once we get accustomed to them. Non-total functions have always felt like a wart in Haskell, and that is why I am willing to bet on dependently typed languages now. I think there will be a lot of exploring and a lot of learning before these languages will be anything near mainstream (like where Haskell is now), but now seems like an exciting time to be part of this development.

Resources

Programming languages

There are now a number of interesting languages with dependent types. This list makes no attempt to be exhaustive and is slanted towards the things that interest me.

Books and Papers

There are also a few books that have come out recently-ish that make dependently typed languages (primarily Coq) much more accessible. This is of course of huge importance to an autodidact like me.

Videos

There are also a few videos and screencasts which revolve around dependent types or some programming language that features dependent types. First of all there is a four day course on Idris with videos and excercises held by the creator of Idris Edwin Brady. I have found the video and the excercises to be a good way to get started with Idris. There is also an introduction to Agda with nine lectures by Conner McBride.

My plan

While I do appreciate some theoretical background, I am not sure that I have the stamina to work through a huge amount of theory without also seeing some applications. I have thus decided to try an approach that combines theory with practice. First of all, I would like to work through Sofware Foundations. While this is theoretically a book, there are so many exercises that it nicely combines theory and practice. Once I am done with that I would like to work my way through Certified Programming with Dependent Types. At the same time I am going to try to port some nice Haskell program to Idris and attempt to prove the totality of as many functions as possible. Since Wouter Swierstra has already ported Xmonad to Coq, this seems like an interesting candidate. Besides, I am running xmonad and like it a lot, so what could be a better opportunity to learn more about it?


  1. The only other language that I am aware of that appeared during the last 10 years and does not require garbage collection is Rust.

  2. I’ve lifted the last two sentences from the books website for obvious reasons. See here and here.


comments powered by Disqus