.. _sect-hangman: *************************************** 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: #. Define the game state, in enough detail to express the rules #. Define the rules of the game (i.e. what actions the player may take, and how these actions affect the game state) #. Implement the rules of the game (i.e. implement state updates for each action) #. 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). .. code-block:: idris 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: .. code-block:: idris 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: .. code-block:: idris 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. .. code-block:: idris 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: .. code-block:: idris 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``. .. code-block:: idris 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``: .. code-block:: idris 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: .. code-block:: idris 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: .. code-block:: idris 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: .. code-block:: idris 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``: .. code-block:: idris 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 :ref:`sect-appendix`) 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: .. code-block:: idris words : ?wtype words = with Vect ["idris","agda","haskell","miranda", "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: .. code-block:: idris 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”.