Having visited Utrecht a few weeks ago, I felt that it was my turn to stand up and save James’s bacon. I mentioned two new PhD theses that are worth looking into.
Bastiaan Heeren recently defended his thesis Top Quality Type Error Messages. There are some fairly compelling examples of strange type errors that GHC can give to relatively innocent programs. Rather than fixing the order of unification, Bastiaan argues that the type checker should first collect all the necessary constraints and subsequently try to solve them. Type errors become more precise and can be scripted by users. A lot of the ideas have been implemented in the Helium compiler, which is definitely worth checking out.
Atze Dijkstra will be defending his thesis in a few weeks. He wrote a large incrementally developed type system for a rather large subset of Haskell. During the process of coding, he implemented several interesting tools. The Ruler tool is essentially a domain specific language for describing type systems. It allows different views of typing rules and incremental specification of complex type systems. The ruler tool itself generates both an attribute grammar implementation and specification of the type rules. Although there are no soundness checks, the tool itself works nicely enough and has actually been used to describe rather large type systems.
As an encore, I outlined Ulf Norell’s winning submission to the succ-zero-th Obfuscated Haskell contest.