Tying Shoes with GADTs

August 2, 2021

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 no-go, 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 type-check, since If expects an Expr Bool as its first argument. Similarly, the following expression would also not type-check: 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
thisTypeChecks = If (AnInt 8) (ABool True) (AnInt 4)

We can use a similar principle to construct valid shoe-tying 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
rllr = PutOnR >>> PutOnL >>> TieL >>> TieR

It type-checks, great! Let’s see what happens when we try to tie our shoes before we put them on.

don't :: Method
don't = TieR >>> TieL >>> PutOnR >>> PutOnL

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 user-friendly instructions.

describe :: Method -> IO ()
describe method = go (method OffLR) *> putStrLn "Done!"
  where
    go :: Shoes l r -> IO ()
    go 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."

Note that the type signature on go is required, the type-checker can’t infer it. This is part of the price we pay with GADTs, expressions don’t always have a principal3 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!

Link to the complete code