Merge pull request #227 from ska80/typedd-book/chapter13-14

Port code examples for chapters 13 and 14 from TypeDD book

docs/app/index.rst

@@ -32,7 +32,7 @@ applications, taking into account both exceptions and linearity. The aims of
 
 * make it possible to express what interactions a function does, in its type,
   without too much notational overhead.
-* have little or no performance overhead compared to writing in \texttt{IO}.
+* have little or no performance overhead compared to writing in *IO*.
 * be compatible with other libraries and techniques for describing effects,
   such as algebraic effects or monad transformers.
 * be sufficiently easy to use and performant that it can be the basis of
@@ -47,4 +47,3 @@ programs, then show how to extend it with exceptions, state, and other
 interfaces.
 
 [To be continued...]
-

docs/typedd/typedd.rst

@@ -248,7 +248,7 @@ know about looking inside pairs.
 
 In ``DataStore.idr``: Well this is embarrassing - I've no idea how Idris 1 lets
 this through! I think perhaps it's too "helpful" when solving unification
-problems. To fix it, add an extra parameter ``scheme`` to ``StoreView``, and change
+problems. To fix it, add an extra parameter ``schema`` to ``StoreView``, and change
 the type of ``SNil`` to be explicit that the ``empty`` is the function defined in
 ``DataStore``. Also add ``entry`` and ``store`` as explicit arguments to ``SAdd``:
 
@@ -282,8 +282,6 @@ In ``TestStore.idr``:
 Chapter 11
 ----------
 
-Remove ``%default total`` throughout - it's not yet implemented.
-
 In ``Streams.idr`` add ``import Data.Stream`` for ``iterate``.
 
 In ``Arith.idr`` and ``ArithTotal.idr``, the ``Divides`` view now has explicit
@@ -306,8 +304,6 @@ export ``(>>=)`` from the namespaces ``CommandDo`` and ``ConsoleDo``.
 Chapter 12
 ----------
 
-Remove ``%default total`` throughout, at least until it's implemented.
-
 For reasons described above: In ``ArithState.idr``, add ``import Data.Strings``.
 Also the ``(>>=)`` operators need to be set as ``export`` since they are in their
 own namespaces, and in ``getRandom``, ``DivBy`` needs to take additional
@@ -316,15 +312,140 @@ arguments ``div`` and ``rem``.
 Chapter 13
 ----------
 
-TODO
+In ``StackIO.idr``:
+
++ ``tryAdd`` pattern matches on ``height``, so it needs to be written in its
+  type:
+
+.. code-block:: idris
+
+    tryAdd : {height : _} -> StackIO height
+
++ ``height`` is also an implicit argument to ``stackCalc``, but is used by the
+  definition, so add it to its type:
+
+.. code-block:: idris
+
+    stackCalc : {height : _} -> StackIO height
+
++ In ``StackDo`` namespace, export ``(>>=)``:
+
+.. code-block:: idris
+
+    namespace StackDo
+      export
+      (>>=) : StackCmd a height1 height2 ->
+              (a -> Inf (StackIO height2)) -> StackIO height1
+              (>>=) = Do
+
+In ``Vending.idr``:
+
++ Add ``import Data.Strings`` and change ``cast`` to ``stringToNatOrZ`` in ``strToInput``
++ In ``MachineCmd`` type, add an implicit argument to ``(>>=)`` data constructor:
+
+.. code-block:: idris
+
+    (>>=) : {state2 : _} ->
+            MachineCmd a state1 state2 ->
+            (a -> MachineCmd b state2 state3) ->
+            MachineCmd b state1 state3
+
++ In ``MachineIO`` type, add an implicit argument to ``Do`` data constructor:
+
+.. code-block:: idris
+
+    data MachineIO : VendState -> Type where
+      Do : {state1 : _} ->
+           MachineCmd a state1 state2 ->
+           (a -> Inf (MachineIO state2)) -> MachineIO state1
+
++ ``runMachine`` pattern matches on ``inState``, so it needs to be written in its
+  type:
+
+.. code-block:: idris
+
+    runMachine : {inState : _} -> MachineCmd ty inState outState -> IO ty
+
++ In ``MachineDo`` namespace, add an implicit argument to ``(>>=)`` and export it:
+
+.. code-block:: idris
+
+    namespace MachineDo
+      export
+      (>>=) : {state1 : _} ->
+              MachineCmd a state1 state2 ->
+              (a -> Inf (MachineIO state2)) -> MachineIO state1
+      (>>=) = Do
+
++ ``vend`` and ``refill`` pattern match on ``pounds`` and ``chocs``, so they need to be written in
+  their type:
+
+.. code-block:: idris
+
+    vend : {pounds : _} -> {chocs : _} -> MachineIO (pounds, chocs)
+    refill: {pounds : _} -> {chocs : _} -> (num : Nat) -> MachineIO (pounds, chocs)
+
++ ``pounds`` and ``chocs`` are implicit arguments to ``machineLoop``, but are used by the
+  definition, so add them to its type:
+
+.. code-block:: idris
+
+    machineLoop : {pounds : _} -> {chocs : _} -> MachineIO (pounds, chocs)
 
 Chapter 14
 ----------
 
-TODO
+In ``ATM.idr``:
+
++ Add ``import Data.Strings`` and change ``cast`` to ``stringToNatOrZ`` in ``runATM``
+
+In ``ATM.idr``, add:
+
+.. code-block:: idris
+
+    import Data.Strings -- for `toUpper`
+    import Data.List -- for `nub`
+
++ In ``Loop`` namespace, export ``GameLoop`` type and its data constructors:
+
+.. code-block:: idris
+
+    namespace Loop
+      public export
+      data GameLoop : (ty : Type) -> GameState -> (ty -> GameState) -> Type where
+        (>>=) : GameCmd a state1 state2_fn ->
+                ((res : a) -> Inf (GameLoop b (state2_fn res) state3_fn)) ->
+                GameLoop b state1 state3_fn
+        Exit : GameLoop () NotRunning (const NotRunning)
+
++ ``letters`` and ``guesses`` are used by ``gameLoop``, so they need to be written in its type:
+
+.. code-block:: idris
+
+    gameLoop : {letters : _} -> {guesses : _} ->
+               GameLoop () (Running (S guesses) (S letters)) (const NotRunning)
+
++ In ``Game`` type, add an implicit argument ``letters`` to ``InProgress`` data constructor:
+
+.. code-block:: idris
+
+    data Game : GameState -> Type where
+      GameStart : Game NotRunning
+      GameWon : (word : String) -> Game NotRunning
+      GameLost : (word : String) -> Game NotRunning
+      InProgress : {letters : _} -> (word : String) -> (guesses : Nat) ->
+                   (missing : Vect letters Char) -> Game (Running guesses letters)
+
++ ``removeElem`` pattern matches on ``n``, so it needs to be written in its type:
+
+.. code-block:: idris
+
+    removeElem : {n : _} ->
+                 (value : a) -> (xs : Vect (S n) a) ->
+                 {auto prf : Elem value xs} ->
+                 Vect n a
 
 Chapter 15
 ----------
 
 TODO
-

tests/Main.idr

@@ -84,7 +84,7 @@ typeddTests : List String
 typeddTests
    = ["chapter01", "chapter02", "chapter03", "chapter04", "chapter05",
       "chapter06", "chapter07", "chapter08", "chapter09", "chapter10",
-      "chapter11", "chapter12"]
+      "chapter11", "chapter12", "chapter13", "chapter14"]
 
 chezTests : List String
 chezTests

tests/typedd-book/chapter11/ArithCmd.idr

@@ -2,7 +2,7 @@ import Data.Primitives.Views
 import Data.Strings
 import System
 
--- %default total
+%default total
 
 data Command : Type -> Type where
      PutStr : String -> Command ()

tests/typedd-book/chapter11/ArithCmdDo.idr

@@ -2,7 +2,7 @@ import Data.Primitives.Views
 import Data.Strings
 import System
 
--- %default total
+%default total
 
 data Command : Type -> Type where
      PutStr : String -> Command ()

tests/typedd-book/chapter11/ArithTotal.idr

@@ -1,7 +1,7 @@
 import Data.Primitives.Views
 import System
 
--- %default total
+%default total
 
 data InfIO : Type where
      Do : IO a -> (a -> Inf InfIO) -> InfIO

tests/typedd-book/chapter11/Greet.idr

@@ -1,4 +1,4 @@
--- %default total
+%default total
 
 data InfIO : Type where
      Do : IO a -> (a -> Inf InfIO) -> InfIO

tests/typedd-book/chapter11/InfIO.idr

@@ -1,4 +1,4 @@
--- %default total
+%default total
 
 data InfIO : Type where
      Do : IO a -> (a -> Inf InfIO) -> InfIO

tests/typedd-book/chapter11/RunIO.idr

@@ -1,4 +1,4 @@
--- %default total
+%default total
 
 data RunIO : Type -> Type where
      Quit : a -> RunIO a

tests/typedd-book/chapter12/ArithState.idr

@@ -2,7 +2,7 @@ import Data.Primitives.Views
 import Data.Strings
 import System
 
--- %default total
+%default total
 
 record Score where
        constructor MkScore

tests/typedd-book/chapter13/Door.idr

@@ -0,0 +1,18 @@
+data DoorState = DoorOpen | DoorClosed
+
+data DoorCmd : Type ->
+               DoorState -> DoorState ->
+               Type where
+  Open :     DoorCmd () DoorClosed DoorOpen
+  Close :    DoorCmd () DoorOpen   DoorClosed
+  RingBell : DoorCmd () DoorClosed DoorClosed
+
+  Pure : ty -> DoorCmd ty state state
+  (>>=) : DoorCmd a state1 state2 ->
+          (a -> DoorCmd b state2 state3) ->
+          DoorCmd b state1 state3
+
+doorProg : DoorCmd () DoorClosed DoorClosed
+doorProg = do RingBell
+              Open
+              Close

tests/typedd-book/chapter13/Stack.idr

@@ -0,0 +1,33 @@
+import Data.Vect
+
+data StackCmd : Type -> Nat -> Nat -> Type where
+  Push : Integer -> StackCmd ()      height     (S height)
+  Pop :             StackCmd Integer (S height) height
+  Top :             StackCmd Integer (S height) (S height)
+
+  Pure : ty -> StackCmd ty height height
+  (>>=) : StackCmd a height1 height2 ->
+          (a -> StackCmd b height2 height3) ->
+          StackCmd b height1 height3
+
+runStack : (stk : Vect inHeight Integer) ->
+           StackCmd ty inHeight outHeight ->
+           (ty, Vect outHeight Integer)
+runStack stk (Push val) = ((), val :: stk)
+runStack (val :: stk) Pop = (val, stk)
+runStack (val :: stk) Top = (val, val :: stk)
+runStack stk (Pure x) = (x, stk)
+runStack stk (x >>= f) = let (x', newStk) = runStack stk x in
+                             runStack newStk (f x')
+
+testAdd : StackCmd Integer 0 0
+testAdd = do Push 10
+             Push 20
+             val1 <- Pop
+             val2 <- Pop
+             Pure (val1 + val2)
+
+doAdd : StackCmd () (S (S height)) (S height)
+doAdd = do val1 <- Pop
+           val2 <- Pop
+           Push (val1 + val2)

tests/typedd-book/chapter13/StackIO.idr

@@ -0,0 +1,94 @@
+import Data.Vect
+
+data StackCmd : Type -> Nat -> Nat -> Type where
+  Push : Integer -> StackCmd ()      height     (S height)
+  Pop :             StackCmd Integer (S height) height
+  Top :             StackCmd Integer (S height) (S height)
+
+  GetStr : StackCmd String height height
+  PutStr : String -> StackCmd () height height
+
+  Pure : ty -> StackCmd ty height height
+  (>>=) : StackCmd a height1 height2 ->
+          (a -> StackCmd b height2 height3) ->
+          StackCmd b height1 height3
+
+runStack : (stk : Vect inHeight Integer) ->
+           StackCmd ty inHeight outHeight ->
+           IO (ty, Vect outHeight Integer)
+runStack stk (Push val) = pure ((), val :: stk)
+runStack (val :: stk) Pop = pure (val, stk)
+runStack (val :: stk) Top = pure (val, val :: stk)
+runStack stk GetStr = do x <- getLine
+                         pure (x, stk)
+runStack stk (PutStr x) = do putStr x
+                             pure ((), stk)
+runStack stk (Pure x) = pure (x, stk)
+runStack stk (x >>= f) = do (x', newStk) <- runStack stk x
+                            runStack newStk (f x')
+
+testAdd : StackCmd () 0 0
+testAdd = do Push 10
+             x <- GetStr
+             Push (cast x)
+             val1 <- Pop
+             val2 <- Pop
+             PutStr (show (val1 + val2) ++ "\n")
+
+data StackIO : Nat -> Type where
+  Do : StackCmd a height1 height2 ->
+       (a -> Inf (StackIO height2)) -> StackIO height1
+
+namespace StackDo
+  export
+  (>>=) : StackCmd a height1 height2 ->
+          (a -> Inf (StackIO height2)) -> StackIO height1
+  (>>=) = Do
+
+data Fuel = Dry | More (Lazy Fuel)
+
+partial
+forever : Fuel
+forever = More forever
+
+run : Fuel -> Vect height Integer -> StackIO height -> IO ()
+run Dry _ _ = pure ()
+run (More fuel) stk (Do c f) = do (res, newStk) <- runStack stk c
+                                  run fuel newStk (f res)
+
+doAdd : StackCmd () (S (S height)) (S height)
+doAdd = do val1 <- Pop
+           val2 <- Pop
+           Push (val1 + val2)
+
+data StkInput = Number Integer
+              | Add
+
+strToInput : String -> Maybe StkInput
+strToInput "" = Nothing
+strToInput "add" = Just Add
+strToInput x = if all isDigit (unpack x)
+                  then Just (Number $ cast x)
+                  else Nothing
+
+mutual
+  tryAdd : {height : _} -> StackIO height
+  tryAdd {height = S (S h)} = do doAdd
+                                 result <- Top
+                                 PutStr (show result ++ "\n")
+                                 stackCalc
+  tryAdd = do PutStr "Fewer than two items on the stack\n"
+              stackCalc
+
+  stackCalc : {height : _} -> StackIO height
+  stackCalc = do PutStr "> "
+                 input <- GetStr
+                 case strToInput input of
+                      Nothing => do PutStr "Invalid input\n"
+                                    stackCalc
+                      Just (Number x) => do Push x
+                                            stackCalc
+                      Just Add => tryAdd
+
+main : IO ()
+main = run forever [] stackCalc

tests/typedd-book/chapter13/Vending.idr

@@ -0,0 +1,109 @@
+import Data.Strings
+
+VendState : Type
+VendState = (Nat, Nat)
+
+data Input = COIN
+           | VEND
+           | CHANGE
+           | REFILL Nat
+
+strToInput : String -> Maybe Input
+strToInput "insert" = Just COIN
+strToInput "vend" = Just VEND
+strToInput "change" = Just CHANGE
+strToInput x = if all isDigit (unpack x)
+                  then Just (REFILL (stringToNatOrZ x))
+                  else Nothing
+
+data MachineCmd : Type ->
+                  VendState -> VendState ->
+                  Type where
+  InsertCoin : MachineCmd () (pounds, chocs)     (S pounds, chocs)
+  Vend :       MachineCmd () (S pounds, S chocs) (pounds, chocs)
+  GetCoins :   MachineCmd () (pounds, chocs)     (Z, chocs)
+
+  Refill : (bars : Nat) ->
+           MachineCmd () (Z, chocs) (Z, bars + chocs)
+
+  Display : String -> MachineCmd ()            state state
+  GetInput :          MachineCmd (Maybe Input) state state
+
+  Pure : ty -> MachineCmd ty state state
+  (>>=) : {state2 : _} ->
+          MachineCmd a state1 state2 ->
+          (a -> MachineCmd b state2 state3) ->
+          MachineCmd b state1 state3
+
+data MachineIO : VendState -> Type where
+  Do : {state1 : _} ->
+       MachineCmd a state1 state2 ->
+       (a -> Inf (MachineIO state2)) -> MachineIO state1
+
+runMachine : {inState : _} -> MachineCmd ty inState outState -> IO ty
+runMachine InsertCoin = putStrLn "Coin inserted"
+runMachine Vend = putStrLn "Please take your chocolate"
+runMachine {inState = (pounds, _)} GetCoins
+     = putStrLn (show pounds ++ " coins returned")
+runMachine (Display str) = putStrLn str
+runMachine (Refill bars)
+     = putStrLn ("Chocolate remaining: " ++ show bars)
+runMachine {inState = (pounds, chocs)} GetInput
+     = do putStrLn ("Coins: " ++ show pounds ++ "; " ++
+                    "Stock: " ++ show chocs)
+          putStr "> "
+          x <- getLine
+          pure (strToInput x)
+runMachine (Pure x) = pure x
+runMachine (cmd >>= prog) = do x <- runMachine cmd
+                               runMachine (prog x)
+namespace MachineDo
+  export
+  (>>=) : {state1 : _} ->
+          MachineCmd a state1 state2 ->
+          (a -> Inf (MachineIO state2)) -> MachineIO state1
+  (>>=) = Do
+
+data Fuel = Dry | More (Lazy Fuel)
+
+partial
+forever : Fuel
+forever = More forever
+
+run : Fuel -> MachineIO state -> IO ()
+run (More fuel) (Do c f)
+     = do res <- runMachine c
+          run fuel (f res)
+run Dry p = pure ()
+
+mutual
+  vend : {pounds : _} -> {chocs : _} -> MachineIO (pounds, chocs)
+  vend {pounds = (S p)} {chocs = (S c)} = do Vend
+                                             Display "Enjoy!"
+                                             machineLoop
+  vend {pounds = Z} = do Display "Insert a coin"
+                         machineLoop
+  vend {chocs = Z} = do Display "Out of stock"
+                        machineLoop
+
+  refill: {pounds : _} -> {chocs : _} -> (num : Nat) -> MachineIO (pounds, chocs)
+  refill {pounds = Z} num = do Refill num
+                               machineLoop
+  refill _ = do Display "Can't refill: Coins in machine"
+                machineLoop
+
+  machineLoop : {pounds : _} -> {chocs : _} -> MachineIO (pounds, chocs)
+  machineLoop = do Just x <- GetInput
+                             | Nothing => do Display "Invalid input"
+                                             machineLoop
+                   case x of
+                        COIN => do InsertCoin
+                                   machineLoop
+                        VEND => vend
+                        CHANGE => do GetCoins
+                                     Display "Change returned"
+                                     machineLoop
+                        REFILL num => refill num
+
+main : IO ()
+main = run forever (machineLoop {pounds = 0} {chocs = 1})

tests/typedd-book/chapter13/expected

@@ -0,0 +1,4 @@
+1/1: Building Door (Door.idr)
+1/1: Building Stack (Stack.idr)
+1/1: Building StackIO (StackIO.idr)
+1/1: Building Vending (Vending.idr)

tests/typedd-book/chapter13/run

@@ -0,0 +1,6 @@
+$1 Door.idr --check
+$1 Stack.idr --check
+$1 StackIO.idr --check
+$1 Vending.idr --check
+
+rm -rf build

tests/typedd-book/chapter14/ATM.idr

@@ -0,0 +1,91 @@
+import Data.Vect
+import Data.Strings
+
+data ATMState = Ready | CardInserted | Session
+
+data PINCheck = CorrectPIN | IncorrectPIN
+
+PIN : Type
+PIN = Vect 4 Char
+
+data HasCard : ATMState -> Type where
+  HasCI : HasCard CardInserted
+  HasSession : HasCard Session
+
+data ATMCmd : (ty : Type) -> ATMState -> (ty -> ATMState) -> Type where
+  InsertCard : ATMCmd ()  Ready        (const CardInserted)
+  EjectCard :  {auto prf : HasCard state} ->
+               ATMCmd ()  state        (const Ready)
+  GetPIN :     ATMCmd PIN CardInserted (const CardInserted)
+
+  CheckPIN : PIN -> ATMCmd PINCheck CardInserted (\check => case check of
+                                                                 CorrectPIN => Session
+                                                                 IncorrectPIN => CardInserted)
+
+  GetAmount :                   ATMCmd Nat state   (const state)
+  Dispense :  (amount : Nat) -> ATMCmd ()  Session (const Session)
+
+  Message :  String -> ATMCmd () state          (const state)
+  Pure : (res : ty) -> ATMCmd ty (state_fn res) state_fn
+  (>>=) : ATMCmd a state1 state2_fn ->
+          ((res : a) -> ATMCmd b (state2_fn res) state3_fn) ->
+          ATMCmd b state1 state3_fn
+
+readVect : (n : Nat) -> IO (Vect n Char)
+readVect Z = do discard <- getLine  -- rest of input up to enter
+                pure []
+readVect (S k) = do ch <- getChar
+                    chs <- readVect k
+                    pure (ch :: chs)
+
+testPIN : Vect 4 Char
+testPIN = ['1', '2', '3', '4']
+
+insertEject : ATMCmd () Ready (const Ready)
+insertEject = do InsertCard
+                 EjectCard  -- ?insertEject_rhs
+
+-- badATM : ATMCmd () Ready (const Ready)
+-- badATM = EjectCard
+
+runATM : ATMCmd res inState outState_fn -> IO res
+runATM InsertCard = do putStrLn "Please insert your card (press enter)"
+                       x <- getLine
+                       pure ()
+runATM EjectCard = putStrLn "Card ejected"
+runATM GetPIN = do putStr "Enter PIN: "
+                   readVect 4
+runATM (CheckPIN pin) = if pin == testPIN
+                           then pure CorrectPIN
+                           else pure IncorrectPIN
+runATM GetAmount = do putStr "How much would you like? "
+                      x <- getLine
+                      pure (stringToNatOrZ x)
+runATM (Dispense amount) = putStrLn ("Here is " ++ show amount)
+runATM (Message msg) = putStrLn msg
+runATM (Pure res) = pure res
+runATM (x >>= f) = do x' <- runATM x
+                      runATM (f x')
+
+atm : ATMCmd () Ready (const Ready)
+atm = do InsertCard
+         pin <- GetPIN
+         pinOK <- CheckPIN pin
+         case pinOK of
+              CorrectPIN => do cash <- GetAmount
+                               Dispense cash
+                               EjectCard
+              IncorrectPIN => EjectCard
+
+atm_alt : ATMCmd () Ready (const Ready)
+atm_alt = do InsertCard
+             pin <- GetPIN
+             cash <- GetAmount
+             pinOK <- CheckPIN pin
+             Message "Checking Card"
+             case pinOK of
+                  CorrectPIN => do Dispense cash
+                                   EjectCard
+                                   Message "Please remove your card and cash"
+                  IncorrectPIN => do Message "Incorrect PIN"
+                                     EjectCard

tests/typedd-book/chapter14/DoorJam.idr

@@ -0,0 +1,48 @@
+data DoorState = DoorClosed | DoorOpen
+
+data DoorResult = OK | Jammed
+
+data DoorCmd : (ty : Type) ->
+               DoorState ->
+               (ty -> DoorState) ->
+               Type where
+  Open :     DoorCmd DoorResult DoorClosed (\res => case res of
+                                                         OK => DoorOpen
+                                                         Jammed => DoorClosed)
+  Close :    DoorCmd ()         DoorOpen   (const DoorClosed)
+  RingBell : DoorCmd ()         DoorClosed (const DoorClosed)
+
+  Display : String -> DoorCmd () state (const state)
+
+  Pure : (res : ty) -> DoorCmd ty (state_fn res) state_fn
+  (>>=) : DoorCmd a state1 state2_fn ->
+          ((res: a) -> DoorCmd b (state2_fn res) state3_fn) ->
+          DoorCmd b state1 state3_fn
+
+logOpen : DoorCmd DoorResult DoorClosed
+                             (\res => case res of
+                                           OK => DoorOpen
+                                           Jammed => DoorClosed)
+logOpen = do Display "Trying to open the door"
+             OK <- Open | Jammed => do Display "Jammed"
+                                       Pure Jammed
+             Display "Success"
+             Pure OK
+
+doorProg : DoorCmd () DoorClosed (const DoorClosed)
+doorProg = do RingBell
+              jam <- Open
+              Display "Trying to open the door"
+              case jam of
+                   OK => do Display "Glad To Be Of Service"
+                            Close
+                   Jammed => Display "Door Jammed"
+
+doorProg2 : DoorCmd () DoorClosed (const DoorClosed)
+doorProg2 = do RingBell
+               OK <- Open | Jammed => Display "Door Jammed"
+               Display "Glad To Be Of Service"
+               Close
+               OK <- Open | Jammed => Display "Door Jammed"
+               Display "Glad To Be Of Service"
+               Close

tests/typedd-book/chapter14/Hangman.idr

@@ -0,0 +1,141 @@
+import Data.Vect
+import Data.List
+import Data.Strings
+
+%default total
+
+data GameState : Type where
+  NotRunning : GameState
+  Running : (guesses : Nat) -> (letters : Nat) -> GameState
+
+letters : String -> List Char
+letters str = nub (map toUpper (unpack str))
+
+data GuessResult = Correct | Incorrect
+
+data GameCmd : (ty : Type) -> GameState -> (ty -> GameState) -> Type where
+  NewGame : (word : String) ->
+            GameCmd () NotRunning (const (Running 6 (length (letters word))))
+
+  Won :  GameCmd () (Running (S guesses) 0) (const NotRunning)
+  Lost : GameCmd () (Running 0 (S guesses)) (const NotRunning)
+
+  Guess : (c : Char) ->
+          GameCmd GuessResult
+                  (Running (S guesses) (S letters))
+                  (\res => case res of
+                                Correct => Running (S guesses) letters
+                                Incorrect => Running guesses (S letters))
+
+  ShowState : GameCmd () state (const state)
+  Message : String -> GameCmd () state (const state)
+  ReadGuess : GameCmd Char state (const state)
+
+  Pure : (res : ty) -> GameCmd ty (state_fn res) state_fn
+  (>>=) : GameCmd a state1 state2_fn ->
+          ((res : a) -> GameCmd b (state2_fn res) state3_fn) ->
+          GameCmd b state1 state3_fn
+
+namespace Loop
+  public export
+  data GameLoop : (ty : Type) -> GameState -> (ty -> GameState) -> Type where
+    (>>=) : GameCmd a state1 state2_fn ->
+            ((res : a) -> Inf (GameLoop b (state2_fn res) state3_fn)) ->
+            GameLoop b state1 state3_fn
+    Exit : GameLoop () NotRunning (const NotRunning)
+
+gameLoop : {letters : _} -> {guesses : _} ->
+           GameLoop () (Running (S guesses) (S letters)) (const NotRunning)
+gameLoop {guesses} {letters} = do ShowState
+                                  g <- ReadGuess
+                                  ok <- Guess g
+                                  case ok of
+                                       Correct => case letters of
+                                                       Z => do Won
+                                                               ShowState
+                                                               Exit
+                                                       S k => do Message "Correct"
+                                                                 gameLoop
+                                       Incorrect => case guesses of
+                                                         Z => do Lost
+                                                                 ShowState
+                                                                 Exit
+                                                         S k => do Message "Incorrect"
+                                                                   gameLoop
+
+hangman : GameLoop () NotRunning (const NotRunning)
+hangman = do NewGame "testing"
+             gameLoop
+
+data Game : GameState -> Type where
+  GameStart : Game NotRunning
+  GameWon : (word : String) -> Game NotRunning
+  GameLost : (word : String) -> Game NotRunning
+  InProgress : {letters : _} -> (word : String) -> (guesses : Nat) ->
+               (missing : Vect letters Char) -> Game (Running guesses letters)
+
+Show (Game g) where
+  show GameStart = "Starting"
+  show (GameWon word) = "Game won: word was " ++ word
+  show (GameLost word) = "Game lost: word was " ++ word
+  show (InProgress word guesses missing) = "\n" ++ pack (map hideMissing (unpack word))
+                                        ++ "\n" ++ show guesses ++ " guesses left "
+  where
+    hideMissing : Char -> Char
+    hideMissing c = if c `elem` missing then '-' else c
+
+data Fuel = Dry | More (Lazy Fuel)
+
+removeElem : {n : _} -> (value : a) -> (xs : Vect (S n) a) -> {auto prf : Elem value xs} -> Vect n a
+removeElem value (value :: ys) {prf = Here} = ys
+removeElem {n = Z} value (y :: []) {prf = There later} = absurd later
+removeElem {n = (S k)} value (y :: ys) {prf = There later} = y :: removeElem value ys
+
+data GameResult : (ty : Type) -> (ty -> GameState) -> Type where
+  OK : (res : ty) -> Game (outState_fn res) -> GameResult ty outState_fn
+  OutOfFuel : GameResult ty outState_fn
+
+ok : (res : ty) -> Game (outstate_fn res) -> IO (GameResult ty outstate_fn)
+ok res st = pure (OK res st)
+
+runCmd : Fuel -> Game inState -> GameCmd ty inState outState_fn -> IO (GameResult ty outState_fn)
+runCmd fuel state (NewGame word) = ok () (InProgress (toUpper word) _ (fromList (letters word)))
+runCmd fuel (InProgress word _ missing) Won = ok () (GameWon word)
+runCmd fuel (InProgress word _ missing) Lost = ok () (GameLost word)
+runCmd fuel (InProgress word _ missing) (Guess c) = case isElem c missing of
+                                                         Yes prf => ok Correct (InProgress word _ (removeElem c missing))
+                                                         No contra => ok Incorrect (InProgress word _ missing)
+runCmd fuel state ShowState = do printLn state
+                                 ok () state
+runCmd fuel state (Message str) = do putStrLn str
+                                     ok () state
+runCmd (More fuel) state ReadGuess = do putStr "Guess: "
+                                        input <- getLine
+                                        case unpack input of
+                                             [x] => if isAlpha x
+                                                       then ok (toUpper x) state
+                                                       else do putStrLn "Invalid input"
+                                                               runCmd fuel state ReadGuess
+                                             _ => do putStrLn "Invalid input"
+                                                     runCmd fuel state ReadGuess
+runCmd fuel state (Pure res) = ok res state
+runCmd fuel state (cmd >>= next) = do OK cmdRes newSt <- runCmd fuel state cmd
+                                                         | OutOfFuel => pure OutOfFuel
+                                      runCmd fuel newSt (next cmdRes)
+runCmd Dry _ _ = pure OutOfFuel
+
+run : Fuel -> Game inState -> GameLoop ty inState outState_fn -> IO (GameResult ty outState_fn)
+run Dry _ _ = pure OutOfFuel
+run (More fuel) st Exit = ok () st
+run (More fuel) st (cmd >>= next) = do OK cmdRes newSt <- runCmd fuel st cmd
+                                                          | OutOfFuel => pure OutOfFuel
+                                       run fuel newSt (next cmdRes)
+
+partial
+forever : Fuel
+forever = More forever
+
+partial
+main : IO ()
+main = do run forever GameStart hangman
+          pure ()

tests/typedd-book/chapter14/expected

@@ -0,0 +1,3 @@
+1/1: Building DoorJam (DoorJam.idr)
+1/1: Building ATM (ATM.idr)
+1/1: Building Hangman (Hangman.idr)

tests/typedd-book/chapter14/run

@@ -0,0 +1,5 @@
+$1 DoorJam.idr --check
+$1 ATM.idr --check
+$1 Hangman.idr --check
+
+rm -rf build