First we’ll make a file called
Battle.idr where we’ll be writing all the Idris code. This is compiled with:
(The full source code for this article is available here.)
The game is a simple text-based game where the player has to defeat an enemy using different moves. The player can make three different moves: punch, kick and magic. The enemy also has these moves. The player and enemy take turns making moves until one of them has no health remaining. If they both use the same move, neither’s health is affected. If one uses kick and the other uses punch, the punching player loses one health point. If one uses punch and the other uses magic, the magic user loses one health point. If one combatant uses magic and the other uses kick, the kicking player loses one health point.
The game can be in one of four states at any given time:
- Safe: The game hasn’t started yet.
- Not Dead: The game has started and neither player has won.
- Dead: Your health has dropped to zero. You have lost the game.
- Won: Your opponent’s health has dropped to zero. You have won the game.
We can represent these states in Idris by defining a new type:
The first line defines a new type, and the following lines define the constructors that create values of that type.
Won are constructors that take no arguments.
health, the player’s current health; and
enemy, the opponent’s current health, both of which are natural numbers.
Now that we have the states of our game, we need to define the operations for moving between states. Idris allows us to express what state the game must be in before we can execute an operation, and what state the game must be in after the operation has been executed. Therefore we can make it literally impossible to execute an operation when it would not be valid to do so. For example, we can guarantee that it is impossible to move to the
Won state — that is, win the game — unless the enemy’s health is at zero. Let’s define the type of an operation:
BattleCmd is the type of all operations that can change the game state. Its first parameter is the type of the value that is returned by a command. Its second parameter is the precondition — the state that the game must be in before the operation can be executed. Its third parameter is the postcondition — the state the game must be left in after the command has finished execution. Actually, this parameter is a function that takes the value returned by the command and itself returns the postcondition state. This is useful because we might we want to enter a different state depending on what was returned by the command. Now we can define some operations:
Let’s examine these more carefully:
Startmoves the game from the
Safestate to the
NotDeadis initialised with the player’s starting health and the enemy’s starting health, both of which are 10.
Startdoesn’t return a value so the return type is
(), the unit type.
NotDead 0 _as its precondition, meaning to run
Diethe game must be in the
NotDeadstate and the player’s health must be zero. After execution the game must be in the
Winrequires that the player’s health is greater than zero (
S kmeans the successor of some natural number
k— in other words some number greater than zero) and that the enemy’s health is zero. If this condition is met,
Wincan be executed and the game moves to the
The remaining three commands cover the three moves that the player can make to attack the enemy. Each requires that the state is
NotDead and that the enemy and player both have some remaining health. The value returned by these commands is of type
EnemyResponse and represents the move the enemy chooses to make in response to the player. The post-condition is a function that takes this response and determines what the state should be afterwards. These three functions are very similar, so we’ll look at just the function of
Kick as an example:
- If the enemy response was
Kickthen both players used the same move so the both players’ health should remain the same.
- If the enemy used
Punch, the enemy’s health should decrease by one and the player’s should remain the same, because kicking beats punching by the rules of our game.
- If the enemy used
Magic, the player’s health drops by one and the enemy’s remains the same because magic beats kicking.
For convenience, we also defined
Log for printing messages, as well as
>>= which allow us to easily write sequences of commands using Idris’ do-notation. Let’s do just that:
This function defines a sequence of commands that: start the game; log a message that the game has started. Note that if we tried to do the following, Idris would throw an error while type checking:
The reason for the error is that at the point where we try to use
Win, the enemy’s health is 10, not zero, therefore the precondition of
Win is not met. In other words, Idris has caught a bug in the program at compile time!
So far we have defined the possible states of the game and the commands to move between those states. Let’s briefly jump out of the land of Idris and create a user interface using HTML with Onsen UI.
The user interface needs buttons for the three user attacks (kick, punch, magic) as well as a way of displaying the status of the game — including the user’s and enemy’s health — and somewhere to log messages to. Onsen UI has components suitable for all of these things.
For the buttons, we’ll use the
ons-button component. It works the same way as the normal
button component. For the styling to work properly, they have to be defined inside an
ons-page tag. The buttons should be fixed to the bottom of the page — for that we can use
At the top of the page, the status will be displayed. To fix some text to the top of the screen,
ons-toolbar is the correct component to use:
Finally we need a way of displaying a log of messages that will be generated while the game runs. We’ll use an
ons-list component to hold all the messages, where each message is an
Now that we have the UI and the abstract logic of the game nailed down, we need to bring the two parts together.
So let’s first create a file
helpers.js for holding the concrete state of the game. In it, we’ll add the following:
There are three parts to this:
state, the object that holds the current state of the game. It is initialised as an empty object.
- The functions for manipulating
state. The functions that write state information add attributes to the state object corresponding to the name of the current state (e.g.
"NOTDEAD") and any extra information needed to recreate the state in Idris (e.g. player health in the
- The top-level object
gameStatewhich exposes all the functions for manipulating state. The
stateobject is private to this top-level function so the concrete game state can’t be accidentally changed by another function.
Calling from Idris
Next we need a way to call the functions defined in
helpers.js from Idris code.
foreign for this purpose. Here is a function
The important parts here are: the second argument to
%1 mean replace this with the zeroth and first arguments respectively.
We need to add a wrapper function for each function in
Keeping it safe
Now we have a way of manipulating the concrete game state using Idris functions and having it persist in between function calls. This sounds like exactly the sort of thing we don’t want in a pure functional programming language, but in this case it is a necessary evil. Nevertheless, we can at least try to be more safe about the way we use these state manipulation functions by making use of the tools Idris provides for us.
We want to ensure that every time we perform some action that manipulates the game state, we remember to: read the state; run the game action on that state; and write out the resulting game state. We can enforce this by adding some new states to
BattleState and commands to
Readyis the state of the system before any game state data has been read in.
Doneis the state after the game state has been written back out.
ReadErroris entered if there was a problem reading the game state.
ReadStateattempts to read in the game state. If it was successful, the next state is the loaded state; otherwise, it goes to the ReadError state.
WriteStatewrites the state back out then moves to Done.
GiveUpcan only be executed in ReadError and moves to Done.
Notice we also defined a new type
Writable. This type is used to separate states used to represent the game, such as
NotDead, from states used for reading and writing housekeeping, such as
Done. We use
Writable in the definitions of
WriteState to make sure that we never accidentally write or read the game state as something nonsensical like
Ready. If you have a value of type
Writable someState, that means
someState is a state that represents what’s going on in the game, instead of a state that represents where the program is at in the reading/writing process. We should also define an instance of
Writable so that we can easily get a string representation of a game state:
With these new states, we can write commands of the type:
BattleCmd () Ready (const Done)
Any value of that type describes a sequence of actions that move from the state
Ready to the state
Done. Since the only way to move from
Ready is to call
ReadState, and the only way to move to
Done is to call
WriteState, values of this type will always read the state first and write the state last.
Real world actions
runCmd' that translates values of type
For some of the commands that move between game states, such as
Die, there’s no IO action that needs to be performed, so the right-hand side of these equations is
pure (), effectively “do nothing”.
Magic require that we return a randomly generated move for the enemy, so we call out to
We have all the pieces we need to make the program do things in the real world. One thing we haven’t done though, is use the
Done states to make sure the IO actions we get from
runCmd' always include reading and writing state at their head and tail. We can enforce this by hiding
runCmd' inside the
where block of another function
Now the only way to turn sequences of commands into real world actions is if the sequence includes actions that read and write state.
Let’s next define a type for all the different commands the user can perform. There is one command for each button in the UI:
Now we can create a function that takes a user command and returns the sequence of actions that should be performed for that command:
(The right-side of each equation has a ‘?’ symbol that indicates a “hole” in Idris — a value that is temporarily left undefined during development.)
It isn’t strictly necessary in this application to bother with the user command type. As I’ll show in a moment,
Input is only used to link an action listener to a callback function, and we could just link them directly. But if we use
Input, we are explicit about the exactly which actions a user can perform. More importantly, we can check that
actions is total i.e. has well-defined behaviour for every value of
Input, so we know that every user command has a corresponding
How to kick, punch and use magic
In the last section, we left holes for the functions to run when the user presses the kick, punch or magic buttons, so let’s go back and define them as
doMagic. These three functions are very similar so I’ll only go over
doKick in detail.
GiveUpif there was an error.
- We match on the state with
case state of. If the state is not
NotDeadwith non-zero player and enemy health, write the state back out and quit.
- We print out a message with
Log "you kicked!"then actually do the
Kickcommand, capturing its return value — the attack the enemy used — in
- We match on
WriteState, we need to pass in a
Writablevalue of the state we want to show or write. This makes sure that we can only ever write or show a game state.
reswas a punch, the enemy loses one health point (again, we don’t have to do anything here because this change of state is encoded in the type). We check if the enemy’s health has dropped to zero; if so, we move to the
Wonstate with the
reswas magic, this time the player loses one health point and we check if the player’s health has dropped to zero. If it has, we call
Dieto move to the
Clicking it all together
The only thing left to do now is to add some extra functions to glue everything together and a main function so we can run the program.
There are some more helper functions to add to
Be careful that these are defined outside the
gameStatefunction — these new functions don’t need access to the state of the game.
Then there are the corresponding Idris wrappers for these new functions:
Finally we need these three functions to do some setup at the start of the game:
doActionlinks a user command to the corresponding IO actions.
setUpcreates the initial persistent state and adds listeners to the user action buttons in the UI for each of the different moves the user can perform.
mainruns setUp once everything has been initialised.
Now if we compile
Battle.idr and open
battle.html in the browser, we can see the finished application. Try playing a game. You’ll notice that once the game has been won or lost, the three action buttons no longer do anything — exactly as we defined in the abstract state machine commands!