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 = If (AnInt 8) (ABool True) (AnInt 4)thisTypeChecks
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 (
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
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 >>> TieRrllr
It type-checks, great! Let’s see what happens when we try to tie our shoes before we put them on.
don't :: Method = TieR >>> TieL >>> PutOnR >>> PutOnLdon'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 user-friendly 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 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!
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
OffLRto define a
Method. We will need it if we want to pattern match on them though, which we’ll do later when writing the
Unambiguous and most general. A simple example is with our
Exprtype from earlier:
ABool b) = bfoo (
foo :: Expr a -> aand
foo :: Expr a -> Boolare valid types to give
foohere, neither being more general than the other.↩︎