Last active
August 3, 2021 04:41
-
-
Save MorrowM/6cd60264dd2efdd5633522c1a7242dde to your computer and use it in GitHub Desktop.
Tying shoes with GADTs - Complete Code
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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