Skip to content

Instantly share code, notes, and snippets.

@MorrowM
Last active Aug 3, 2021
Embed
What would you like to do?
Tying shoes with GADTs - Complete Code
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
module Shoe where
data ShoeState = Off | Untied | On
data Shoes l r where
PutOnL :: Shoes Off r -> Shoes Untied r
PutOnR :: Shoes l Off -> Shoes l Untied
TieL :: Shoes Untied r -> Shoes On r
TieR :: Shoes l Untied -> Shoes l On
OffLR :: Shoes Off Off
type Method = Shoes Off Off -> Shoes On On
(>>>) = flip (.)
rllr :: Method
rllr = PutOnR >>> PutOnL >>> TieL >>> TieR
-- Doesn't type check:
-- don't :: Method
-- don't = TieR >>> TieL >>> PutOnR >>> PutOnL
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."
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment