How do you put on your shoes?
Do you put them both on and then tie them both? In what order? Do you put on one shoe, tie it and then do the other one? That might be a bit odd, but it’s acceptable. Anyone who ties either of their shoes before putting them on is a nogo, though. And since my Haskell file is my world, and GHC is my enforcer, let’s make this state of affairs unrepresentable.
A brief introduction to GADTs
Maybe
is an algebraic data type (ADT for short) that we all know and love. It’s defined as:
data Maybe a = Nothing  Just a
We can ask GHCi the types of the data constructors:
> :t Nothing
λNothing :: Maybe a
> :t Just
λJust :: a > Maybe a
Cool! This even defines what Maybe
is. It would also be pretty cool if we could define Maybe
that way.^{1}
data Maybe a where
Nothing :: Maybe a
Just :: a > Maybe a
Of course, the return types of these constructors have to be the same. But what if things didn’t have to be that way?
Consider the following data type:
data Expr a where
ABool :: Bool > Expr Bool
AnInt :: Int > Expr Int
If :: Expr Bool > Expr a > Expr a > Expr a
If we could make such a data type, then an expression like If (ABool True) (AnInt 5) (AnInt 7)
would be fine, while an expression If (AnInt 5) (AnInt 5) (AnInt 7)
wouldn’t typecheck, since If
expects an Expr Bool
as its first argument. Similarly, the following expression would also not typecheck: If (ABool False) (AnInt 6) (ABool 5)
. If
expects its second and third arguments to have the same type, which is not true in this case.
This sort of data type can indeed be defined if you enable the GHC GADTs
language extension, a GADT being a generalized ADT. If we didn’t index our expressions by their types like this, we wouldn’t have been able to prevent the programmer from constructing these invalid expressions.
data Expr = ABool Bool  AnInt Int  If Expr Expr Expr
= If (AnInt 8) (ABool True) (AnInt 4) thisTypeChecks
We can use a similar principle to construct valid shoetying methods.
Using GADTs to make illegal states unrepresentable
First, we need to define what states a shoe can be in.
data ShoeState = Off  Untied  On
So a shoe is either completely off, on but untied, or on.
Let’s define what operations we can perform on our pair of shoes, by using a GADT.
data Shoes l r where
 Both shoes can be off:
OffLR :: Shoes Off Off
 If a shoe is off, we can put it on:
PutOnL :: Shoes Off r > Shoes Untied r
PutOnR :: Shoes l Off > Shoes l Untied
 If a shoe is on, but untied, we can tie it:
TieL :: Shoes Untied r > Shoes On r
TieR :: Shoes l Untied > Shoes l On
This is pretty cool. We’re defining a set of valid state transitions, and enforcing it in the type system.
One other thing to note here is that we’re using the DataKinds
extension to allow us to use these runtime values (Off
, Untied
, and On
) in our types. We could have defined empty dummy types with no constructors (e.g data Off
), but using DataKinds
will give us tighter control over the types and give better error messages when we mess up.
We can also define a valid shoe tying method to be a function from Off
shoes to On
shoes.
type Method = Shoes Off Off > Shoes On On
It almost reads like English, nice.^{2} One last thing is we’ll define a flipped composition operator so that we can compose our constructors from left to right, as opposed to (.)
which composes right to left.
>>>) = flip (.) (
Let’s define our first method.
rllr :: Method
= PutOnR >>> PutOnL >>> TieL >>> TieR rllr
It typechecks, great! Let’s see what happens when we try to tie our shoes before we put them on.
don't :: Method
= TieR >>> TieL >>> PutOnR >>> PutOnL don't
We get a bunch of type errors, which is exactly what we wanted.
Shoe.hs: error:
• Couldn't match type ‘'Off’ with ‘'On’
Expected type: Shoes 'On 'On > Shoes 'On 'Untied
Actual type: Shoes 'On 'Off > Shoes 'On 'Untied

 don't = TieR >>> TieL >>> PutOnR >>> PutOnL
 ^^^^^^
One last thing we can do is since these are runtime values, we could print them as userfriendly instructions.
describe :: Method > IO ()
= go (method OffLR) *> putStrLn "Done!"
describe method where
go :: Shoes l r > IO ()
OffLR = putStrLn "Alright."
go PutOnL x) = go x *> putStrLn "Put on the left shoe."
go (PutOnR x) = go x *> putStrLn "Put on the right shoe."
go (TieL x) = go x *> putStrLn "Tie the left shoe."
go (TieR x) = go x *> putStrLn "Tie the right shoe." go (
Note that the type signature on go
is required, the typechecker can’t infer it. This is part of the price we pay with GADTs, expressions don’t always have a principal^{3} type.
We can run it, and finally, get some instructions on how to put on and tie our shoes.
λ> describe rllr
Alright.
Put on the right shoe.
Put on the left shoe.
Tie the left shoe.
Tie the right shoe.
Done!
We can, in fact, do this with the GHC language extension
GADTSyntax
, which will be on by default starting in GHC 9.2. Of course, we’re getting ahead of ourselves.↩︎In fact, we won’t even need
OffLR
to define aMethod
. We will need it if we want to pattern match on them though, which we’ll do later when writing thedescribe
function.↩︎Unambiguous and most general. A simple example is with our
Expr
type from earlier:ABool b) = b foo (
Both
foo :: Expr a > a
andfoo :: Expr a > Bool
are valid types to givefoo
here, neither being more general than the other.↩︎