Last Friday, I attended Well Typed’s training course on the various extensions available in Haskell - specifically, those available in GHC. I had a terrific time, and as I feel Well Typed’s courses go somewhat un-noticed, it deserves a write up. Despite having a fairly wide knowledge of type level magic, I always felt my knowledge was a little… ad hoc. I can confidently say that I no longer feel that is the case.
First though, what was this course about? As you no doubt know, Haskell is well known for being a very type safe language. However, if we limit ourselves to “vanilla” Haskell, we can quickly run into problems. Andres began with a motivating example: a basic quiz application, where we have a list of
Questions and a corresponding list of
Answers. We can model these in Haskell as
[Answer] - but there’s very little that the type system is doing to aid us build programs manipulating this data. For example, scoring the questions and answers should be a case of zipping the two lists together - but if the two lists aren’t the same length, then we certainly won’t calculate the right score!
Andres is fantastic at breaking complicated topics apart into small pieces. If you haven’t seen his talk explaining free monads from last year’s Haskell eXchange, I highly recommend it. The Well Typed course progressed in a very similar way. From the original problem statement, we first tried to write length-indexed lists using
newtypes with phantom types, but noticed that this isn’t a particularly useful abstraction. We quickly moved to GADTs and rephrased our data as
Vec n Question and
Vec n Answer, which already let’s us write a much sounder form of
zipWith for scoring. This material alone is well worth learning, as GADTs are a good solution for a wide range of problems (Andres nicely explained that GADTs are a good way to model relations between types).
However, we can go further with this data type. One problem we noticed was that this type wasn’t restrictive enough - GHC will quite happily accept types like of
Vec Bool Char, which is completely meaningless! Even though we can’t construct any terms of this type, it would be good if we were prevented from making such mistakes as soon as possible. Using the recent data type promotion functionality, we addressed this problem, and considered
Vec :: Nat -> * -> * a good solution for our application so far.
We then extended the application to support multiple types of questions and answers (true/false vs. quantity questions), and reached the limit of
Vec. We generalised a step further to a type of heterogeneous list called
We moved machinery from
Env to extend our application, still maintaining a huge amount of type safety. However, the more general type introduced problems, and we diverged out to understand how type class derivation works, and observed the need for higher-rank polymorphism to write
zipWith for this data type.
After a short break, we explored operations on
Env in further detail, comparing against the following “weakly typed Haskell” code1:
This code is clearly very dangerous -
!! can fail at runtime if the we have the wrong index, how do we move this over to
Env? We’d like to keep the shape of the program the same, so how would we write a type safe
!! function? Here we began to understand how functions that return
Bool are throwing information away, and that we need to somehow preserve information when we work with richer types. Rather than pointing into a list with
Int, we built a
Ptr object that gives us a type safe way to point into
Env, and then we compared this against the standard implementation of Peano numbers to build more intuition.
All of this is great, but it’s not very practical - we often have data that lives outside our lovely type-safe sandbox. For example, we’d probably want to store the questions in a database, and receive answers from website form submissions. Here we learnt how we can move from a weakly typed setting to stronger types through decision procedures, and how our “check” functions actually witness more type information in the process. We saw a need for existential types and how these can give us one way of encoding type information that we don’t know statically.
With a movement towards proofs, we saw how we can use
:~: and the new
Data.Type.Equality module to introduce new information into the type system - specifically constructing proofs on natural numbers to implement a type safe
reverse :: Vec n a -> Vec n a function. This is a technique I was somewhat aware of and had briefly seen in Agda, but had certainly never seen done in Haskell. I must say, I’m quite impressed with how natural it is with the new
Finally, we wrapped the day up with a look at type families to perform type level addition of natural numbers, and saw how associated types can be used with type classes.
There’s a lot of material I’ve left out, such as singleton types and various caveats on the extensions we were using; it’s remarkable just how much was squeezed into a day’s studying. As I said before, Andres has a very systematic and reasoned approach to teaching, which lets the student see the small incremental steps while also being able to check progress against a bigger picture.
Well Typed offer a wide range of courses - not just courses on the plethora of extensions to GHC. If you’re studying Haskell and want to truly solidify your knowledge, I can definitely recommend Well Typed’s work. Thanks again, Andres!
Of course, we’d normally write this with
zipWith, so it’s not particularly idiomatic Haskell. However, code like this does crop up, and this was an easy example for educational purposes.↩︎
You can contact me via email at firstname.lastname@example.org or tweet to me @acid2. I share almost all of my work at GitHub. This post is licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.
I accept Bitcoin donations:
14SsYeM3dmcUxj3cLz7JBQnhNdhg7dUiJn. Alternatively, please consider leaving a tip on