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 (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 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 >>> 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 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!