Example: A “Mystery Word” Guessing Game¶

In this section, we will use the techniques and specific effects discussed in the tutorial so far to implement a larger example, a simple text-based word-guessing game. In the game, the computer chooses a word, which the player must guess letter by letter. After a limited number of wrong guesses, the player loses [1].

We will implement the game by following these steps:

1. Define the game state, in enough detail to express the rules
2. Define the rules of the game (i.e. what actions the player may take, and how these actions affect the game state)
3. Implement the rules of the game (i.e. implement state updates for each action)
4. Implement a user interface which allows a player to direct actions

Step 2 may be achieved by defining an effect which depends on the state defined in step 1. Then step 3 involves implementing a Handler for this effect. Finally, step 4 involves implementing a program in Eff using the newly defined effect (and any others required to implement the interface).

Step 1: Game State¶

First, we categorise the game states as running games (where there are a number of guesses available, and a number of letters still to guess), or non-running games (i.e. games which have not been started, or games which have been won or lost).

data GState = Running Nat Nat | NotRunning


Notice that at this stage, we say nothing about what it means to make a guess, what the word to be guessed is, how to guess letters, or any other implementation detail. We are only interested in what is necessary to describe the game rules.

We will, however, parameterise a concrete game state Mystery over this data:

data Mystery : GState -> Type


Step 2: Game Rules¶

We describe the game rules as a dependent effect, where each action has a precondition (i.e. what the game state must be before carrying out the action) and a postcondition (i.e. how the action affects the game state). Informally, these actions with the pre- and postconditions are:

Guess

Guess a letter in the word.

• Precondition: The game must be running, and there must be both guesses still available, and letters still to be guessed.
• Postcondition: If the guessed letter is in the word and not yet guessed, reduce the number of letters, otherwise reduce the number of guesses.
Won

Declare victory

• Precondition: The game must be running, and there must be no letters still to be guessed.
• Postcondition: The game is no longer running.
Lost

Accept defeat

• Precondition: The game must be running, and there must be no guesses left.
• Postcondition: The game is no longer running.
NewWord

Set a new word to be guessed

• Precondition: The game must not be running.
• Postcondition: The game is running, with 6 guesses available (the choice of 6 is somewhat arbitrary here) and the number of unique letters in the word still to be guessed.
Get
Get a string representation of the game state. This is for display purposes; there are no pre- or postconditions.

We can make these rules precise by declaring them more formally in an effect signature:

data MysteryRules : Effect where
Guess : (x : Char) ->
sig MysteryRules Bool
(Mystery (Running (S g) (S w)))
(\inword => if inword
then Mystery (Running (S g) w)
else Mystery (Running g (S w)))
Won  : sig MysteryRules () (Mystery (Running g 0))
(Mystery NotRunning)
Lost : sig MysteryRules () (Mystery (Running 0 g))
(Mystery NotRunning)
NewWord : (w : String) ->
sig MysteryRules () (Mystery NotRunning) (Mystery (Running 6 (length (letters w))))
Get : sig MysteryRules String (Mystery h)


This description says nothing about how the rules are implemented. In particular, it does not specify how to tell whether a guessed letter was in a word, just that the result of Guess depends on it.

Nevertheless, we can still create an EFFECT from this, and use it in an Eff program. Implementing a Handler for MysteryRules will then allow us to play the game.

MYSTERY : GState -> EFFECT
MYSTERY h = MkEff (Mystery h) MysteryRules


Step 3: Implement Rules¶

To implement the rules, we begin by giving a concrete definition of game state:

data Mystery : GState -> Type where
Init     : Mystery NotRunning
GameWon  : (word : String) -> Mystery NotRunning
GameLost : (word : String) -> Mystery NotRunning
MkG      : (word : String) ->
(guesses : Nat) ->
(got : List Char) ->
(missing : Vect m Char) ->
Mystery (Running guesses m)


If a game is NotRunning, that is either because it has not yet started (Init) or because it is won or lost (GameWon and GameLost, each of which carry the word so that showing the game state will reveal the word to the player). Finally, MkG captures a running game’s state, including the target word, the letters successfully guessed, and the missing letters. Using a Vect for the missing letters is convenient since its length is used in the type.

To initialise the state, we implement the following functions: letters, which returns a list of unique letters in a String (ignoring spaces) and initState which sets up an initial state considered valid as a postcondition for NewWord.

letters : String -> List Char
initState : (x : String) -> Mystery (Running 6 (length (letters x)))


When checking if a guess is in the vector of missing letters, it is convenient to return a proof that the guess is in the vector, using isElem below, rather than merely a Bool:

data IsElem : a -> Vect n a -> Type where
First : IsElem x (x :: xs)
Later : IsElem x xs -> IsElem x (y :: xs)

isElem : DecEq a => (x : a) -> (xs : Vect n a) -> Maybe (IsElem x xs)


The reason for returning a proof is that we can use it to remove an element from the correct position in a vector:

shrink : (xs : Vect (S n) a) -> IsElem x xs -> Vect n a


We leave the definitions of letters, init, isElem and shrink as exercises. Having implemented these, the Handler implementation for MysteryRules is surprisingly straightforward:

Handler MysteryRules m where
handle (MkG w g got []) Won k = k () (GameWon w)
handle (MkG w Z got m) Lost k = k () (GameLost w)

handle st Get k = k (show st) st
handle st (NewWord w) k = k () (initState w)

handle (MkG w (S g) got m) (Guess x) k =
case isElem x m of
Nothing => k False (MkG w _ got m)
(Just p) => k True (MkG w _ (x :: got) (shrink m p))


Each case simply involves directly updating the game state in a way which is consistent with the declared rules. In particular, in Guess, if the handler claims that the guessed letter is in the word (by passing True to k), there is no way to update the state in such a way that the number of missing letters or number of guesses does not follow the rules.

Step 4: Implement Interface¶

Having described the rules, and implemented state transitions which follow those rules as an effect handler, we can now write an interface for the game which uses the MYSTERY effect:

game : Eff () [MYSTERY (Running (S g) w), STDIO]
[MYSTERY NotRunning, STDIO]


The type indicates that the game must start in a running state, with some guesses available, and eventually reach a not-running state (i.e. won or lost). The only way to achieve this is by correctly following the stated rules.

Note that the type of game makes no assumption that there are letters to be guessed in the given word (i.e. it is w rather than S w). This is because we will be choosing a word at random from a vector of String, and at no point have we made it explicit that those String are non-empty.

Finally, we need to initialise the game by picking a word at random from a list of candidates, setting it as the target using NewWord, then running game:

runGame : Eff () [MYSTERY NotRunning, RND, SYSTEM, STDIO]
runGame = do srand !time
let w = index !(rndFin _) words
call \$ NewWord w
game
putStrLn !(call Get)


We use the system time (time from the SYSTEM effect; see Appendix Effects Summary) to initialise the random number generator, then pick a random Fin to index into a list of words. For example, we could initialise a word list as follows:

words : ?wtype
"java","javascript","fortran","basic",
"coffeescript","rust"]

wtype = proof search


Note

Rather than have to explicitly declare a type with the vector’s length, it is convenient to give a hole ?wtype and let Idris’s proof search mechanism find the type. This is a limited form of type inference, but very useful in practice.

A possible complete implementation of game is presented below:

game : Eff () [MYSTERY (Running (S g) w), STDIO]
[MYSTERY NotRunning, STDIO]
game {w=Z} = Won
game {w=S _}
= do putStrLn !Get
putStr "Enter guess: "
let guess = trim !getStr
case choose (not (guess == "")) of
(Left p) => processGuess (strHead' guess p)
(Right p) => do putStrLn "Invalid input!"
game
where
processGuess : Char -> Eff () [MYSTERY (Running (S g) (S w)), STDIO]
[MYSTERY NotRunning, STDIO]
processGuess {g} {w} c
= case !(Main.Guess c) of
True => do putStrLn "Good guess!"
case w of
Z => Won
(S k) => game
False => do putStrLn "No, sorry"
case g of
Z => Lost
(S k) => game


Discussion¶

Writing the rules separately as an effect, then an implementation which uses that effect, ensures that the implementation must follow the rules. This has practical applications in more serious contexts; MysteryRules for example can be though of as describing a protocol that a game player most follow, or alternative a precisely-typed API.

In practice, we wouldn’t really expect to write rules first then implement the game once the rules were complete. Indeed, I didn’t do so when constructing this example! Rather, I wrote down a set of likely rules making any assumptions explicit in the state transitions for MysteryRules. Then, when implementing game at first, any incorrect assumption was caught as a type error. The following errors were caught during development:

• Not realising that allowing NewWord to be an arbitrary string would mean that game would have to deal with a zero-length word as a starting state.
• Forgetting to check whether a game was won before recursively calling processGuess, thus accidentally continuing a finished game.
• Accidentally checking the number of missing letters, rather than the number of remaining guesses, when checking if a game was lost.

These are, of course, simple errors, but were caught by the type checker before any testing of the game.

 [1] Readers may recognise this game by the name “Hangman”.