3***************************************
4Example: A “Mystery Word” Guessing Game
5***************************************
7In this section, we will use the techniques and specific effects
8discussed in the tutorial so far to implement a larger example, a simple
9text-based word-guessing game. In the game, the computer chooses a word,
10which the player must guess letter by letter. After a limited number of
11wrong guesses, the player loses [1]_.
13We will implement the game by following these steps:
15#. Define the game state, in enough detail to express the rules
17#. Define the rules of the game (i.e. what actions the player may take,
18 and how these actions affect the game state)
20#. Implement the rules of the game (i.e. implement state updates for
23#. Implement a user interface which allows a player to direct actions
25Step 2 may be achieved by defining an effect which depends on the state
26defined in step 1. Then step 3 involves implementing a ``Handler`` for
27this effect. Finally, step 4 involves implementing a program in ``Eff``
28using the newly defined effect (and any others required to implement the
34First, we categorise the game states as running games (where there are a
35number of guesses available, and a number of letters still to guess), or
36non-running games (i.e. games which have not been started, or games
37which have been won or lost).
41 data GState = Running Nat Nat | NotRunning
43Notice that at this stage, we say nothing about what it means to make a
44guess, what the word to be guessed is, how to guess letters, or any
45other implementation detail. We are only interested in what is necessary
46to describe the game rules.
48We will, however, parameterise a concrete game state ``Mystery`` over
53 data Mystery : GState -> Type
58We describe the game rules as a dependent effect, where each action has
59a *precondition* (i.e. what the game state must be before carrying out
60the action) and a *postcondition* (i.e. how the action affects the game
61state). Informally, these actions with the pre- and postconditions are:
64 Guess a letter in the word.
66 - Precondition: The game must be running, and there must be both
67 guesses still available, and letters still to be guessed.
69 - Postcondition: If the guessed letter is in the word and not yet
70 guessed, reduce the number of letters, otherwise reduce the
76 - Precondition: The game must be running, and there must be no
77 letters still to be guessed.
79 - Postcondition: The game is no longer running.
84 - Precondition: The game must be running, and there must be no
87 - Postcondition: The game is no longer running.
90 Set a new word to be guessed
92 - Precondition: The game must not be running.
94 - Postcondition: The game is running, with 6 guesses available (the
95 choice of 6 is somewhat arbitrary here) and the number of unique
96 letters in the word still to be guessed.
99 Get a string representation of the game state. This is for display
100 purposes; there are no pre- or postconditions.
102We can make these rules precise by declaring them more formally in an
107 data MysteryRules : Effect where
108 Guess : (x : Char) ->
109 { Mystery (Running (S g) (S w)) ==>
110 {inword} if inword then Mystery (Running (S g) w)
111 else Mystery (Running g (S w)) }
113 Won : { Mystery (Running g 0) ==> Mystery NotRunning } MysteryRules ()
114 Lost : { Mystery (Running 0 g) ==> Mystery NotRunning } MysteryRules ()
115 NewWord : (w : String) ->
116 { Mystery NotRunning ==>
117 Mystery (Running 6 (length (letters w))) } MysteryRules ()
118 StrState : { Mystery h } MysteryRules String
120This description says nothing about how the rules are implemented. In
121particular, it does not specify *how* to tell whether a guessed letter
122was in a word, just that the result of ``Guess`` depends on it.
124Nevertheless, we can still create an ``EFFECT`` from this, and use it in
125an ``Eff`` program. Implementing a ``Handler`` for ``MysteryRules`` will
126then allow us to play the game.
130 MYSTERY : GState -> EFFECT
131 MYSTERY h = MkEff (Mystery h) MysteryRules
133Step 3: Implement Rules
134=======================
136To *implement* the rules, we begin by giving a concrete definition of
141 data Mystery : GState -> Type where
142 Init : Mystery NotRunning
143 GameWon : (word : String) -> Mystery NotRunning
144 GameLost : (word : String) -> Mystery NotRunning
145 MkG : (word : String) ->
148 (missing : Vect m Char) ->
149 Mystery (Running guesses m)
151If a game is ``NotRunning``, that is either because it has not yet
152started (``Init``) or because it is won or lost (``GameWon`` and
153``GameLost``, each of which carry the word so that showing the game
154state will reveal the word to the player). Finally, ``MkG`` captures a
155running game’s state, including the target word, the letters
156successfully guessed, and the missing letters. Using a ``Vect`` for the
157missing letters is convenient since its length is used in the type.
159To initialise the state, we implement the following functions:
160``letters``, which returns a list of unique letters in a ``String``
161(ignoring spaces) and ``initState`` which sets up an initial state
162considered valid as a postcondition for ``NewWord``.
166 letters : String -> List Char
167 initState : (x : String) -> Mystery (Running 6 (length (letters x)))
169When checking if a guess is in the vector of missing letters, it is
170convenient to return a *proof* that the guess is in the vector, using
171``isElem`` below, rather than merely a ``Bool``:
175 data IsElem : a -> Vect n a -> Type where
176 First : IsElem x (x :: xs)
177 Later : IsElem x xs -> IsElem x (y :: xs)
179 isElem : DecEq a => (x : a) -> (xs : Vect n a) -> Maybe (IsElem x xs)
181The reason for returning a proof is that we can use it to remove an
182element from the correct position in a vector:
186 shrink : (xs : Vect (S n) a) -> IsElem x xs -> Vect n a
188We leave the definitions of ``letters``, ``init``, ``isElem`` and
189``shrink`` as exercises. Having implemented these, the ``Handler``
190implementation for ``MysteryRules`` is surprisingly straightforward:
194 instance Handler MysteryRules m where
195 handle (MkG w g got []) Won k = k () (GameWon w)
196 handle (MkG w Z got m) Lost k = k () (GameLost w)
198 handle st StrState k = k (show st) st
199 handle st (NewWord w) k = k () (initState w)
201 handle (MkG w (S g) got m) (Guess x) k =
203 Nothing => k False (MkG w _ got m)
204 (Just p) => k True (MkG w _ (x :: got) (shrink m p))
206Each case simply involves directly updating the game state in a way
207which is consistent with the declared rules. In particular, in
208``Guess``, if the handler claims that the guessed letter is in the word
209(by passing ``True`` to ``k``), there is no way to update the state in
210such a way that the number of missing letters or number of guesses does
213Step 4: Implement Interface
214===========================
216Having described the rules, and implemented state transitions which
217follow those rules as an effect handler, we can now write an interface
218for the game which uses the ``MYSTERY`` effect:
222 game : { [MYSTERY (Running (S g) w), STDIO] ==>
223 [MYSTERY NotRunning, STDIO] } Eff ()
225The type indicates that the game must start in a running state, with
226some guesses available, and eventually reach a not-running state (i.e.
227won or lost). The only way to achieve this is by correctly following the
230Note that the type of ``game`` makes no assumption that there are
231letters to be guessed in the given word (i.e. it is ``w`` rather than
232``S w``). This is because we will be choosing a word at random from a
233vector of ``String``, and at no point have we made it explicit that
234those ``String`` are non-empty.
236Finally, we need to initialise the game by picking a word at random from
237a list of candidates, setting it as the target using ``NewWord``, then
242 runGame : { [MYSTERY NotRunning, RND, SYSTEM, STDIO] } Eff ()
243 runGame = do srand (cast !time)
244 let w = index !(rndFin WEWEWE) words
249We use the system time (``time`` from the ``SYSTEM`` effect; see
250Appendix :ref:`sect-appendix`) to initialise the random number
251generator, then pick a random ``Fin`` to index into a list of
252``words``. For example, we could initialise a word list as follows:
257 words = with Vect ["idris","agda","haskell","miranda",
258 "java","javascript","fortran","basic",
259 "coffeescript","rust"]
264 Rather than have to explicitly declare a type with the vector’s
265 length, it is convenient to give a metavariable ``?wtype`` and let
266 Idris’s proof search mechanism find the type. This is a
267 limited form of type inference, but very useful in practice.
269A possible complete implementation of ``game`` is
274 game : { [MYSTERY (Running (S g) w), STDIO] ==>
275 [MYSTERY NotRunning, STDIO] } Eff ()
278 = do putStrLn !StrState
279 putStr "Enter guess: "
280 let guess = trim !getStr
281 case choose (not (guess == "")) of
282 (Left p) => processGuess (strHead' guess p)
283 (Right p) => do putStrLn "Invalid input!"
286 processGuess : Char -> { [MYSTERY (Running (S g) (S w)), STDIO] ==>
287 [MYSTERY NotRunning, STDIO] }
289 processGuess {g} {w} c
290 = case !(Main.Guess c) of
291 True => do putStrLn "Good guess!"
295 False => do putStrLn "No, sorry"
303Writing the rules separately as an effect, then an implementation
304which uses that effect, ensures that the implementation must follow
305the rules. This has practical applications in more serious contexts;
306``MysteryRules`` for example can be though of as describing a
307*protocol* that a game player most follow, or alternative a
308*precisely-typed API*.
310In practice, we wouldn’t really expect to write rules first then
311implement the game once the rules were complete. Indeed, I didn’t do
312so when constructing this example! Rather, I wrote down a set of
313likely rules making any assumptions *explicit* in the state
314transitions for ``MysteryRules``. Then, when implementing ``game`` at
315first, any incorrect assumption was caught as a type error. The
316following errors were caught during development:
318- Not realising that allowing ``NewWord`` to be an arbitrary string
319 would mean that ``game`` would have to deal with a zero-length word
322- Forgetting to check whether a game was won before recursively
323 calling ``processGuess``, thus accidentally continuing a finished
326- Accidentally checking the number of missing letters, rather than the
327 number of remaining guesses, when checking if a game was lost.
329These are, of course, simple errors, but were caught by the type
330checker before any testing of the game.
333 Readers may recognise this game by the name “Hangman”.
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list