Idris state machines in JavaScript apps

Writing JavaScript applications that behave the way you want them to is difficult. Because JavaScript is dynamically typed, the programmer usually gets no indication from the interpreter if there is a bug in his program.

In this article, I’m going to demonstrate a way to develop JavaScript applications using the dependently-typed functional programming language Idris. A dependent type is a type whose definition depends on another value. You can define very precise types in Idris and catch a lot of errors at compile time. Idris is particularly good for writing programs based on state machines. I’ll show how to create a simple battle game using Idris, and internally model the game as a state machine. Thanks to Idris’ powerful type checking capabilities, we’ll define a state machine that ensures it is only possible to make legal moves between states according to rules we define.

The tools we will be using for this task are Idris, JavaScript and HTML, plus the mobile framework Onsen UI for styling. We’ll write all of the logic of the application in Idris, and then using the compiler flag --codegen javascript, will compile the code to a JavaScript file, which can then be used like in any normal web application.

First we’ll make a file called Battle.idr where we’ll be writing all the Idris code. This is compiled with:

idris --codegen javascript -o battle.js Battle.idr

This command compiles the Idris code and outputs a JavaScript file called battle.js.

The game

(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. Safe, Dead, and Won are constructors that take no arguments. NotDead takes: health, the player’s current health; and enemy, the opponent’s current health, both of which are natural numbers.

Operations

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:

• Start moves the game from the Safe state to the NotDead state. NotDead is initialised with the player’s starting health and the enemy’s starting health, both of which are 10. Start doesn’t return a value so the return type is (), the unit type.
• Die has NotDead 0 _ as its precondition, meaning to run Die the game must be in the NotDead state and the player’s health must be zero. After execution the game must be in the Dead state.
• Win requires that the player’s health is greater than zero (S k means 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, Win can be executed and the game moves to the Won state.

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 Kick then 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 Pure and >>= 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!

User interface

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.

First, a basic HTML page with the imports for Onsen UI, our compiled Idris program, and a file with some helper JavaScript functions that we’ll define later on:

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 ons-bottom-toolbar:

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 ons-list-item. Later on, we’ll dynamically add messages to the list as they are generated using JavaScript. For now though, the UI body should be as follows:

Managing state

Now that we have the UI and the abstract logic of the game nailed down, we need to bring the two parts together.

JavaScript state

Firstly, we’re going to have to store the state of the game somewhere as a JavaScript object. In other applications of state machines in Idris, such as a command line application, we don’t need to explicitly write the state anywhere because the program runs in a loop, and therefore can “hold on” to the state. However, JavaScript is a bit more tricky because it is event-driven. When the user clicks a button, we need to run an Idris function which will affect the state of the game, but that function terminates when the work is done, unlike a command line application, which will loop and wait for more input. Because of this, we need to hold the state somewhere in between function calls, and make sure to read and write the state properly at the beginning and end of each function.

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. "DEAD", "NOTDEAD") and any extra information needed to recreate the state in Idris (e.g. player health in the NotDead state).
• The top-level object gameState which exposes all the functions for manipulating state. The state object 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.

We can call JavaScript functions from Idris code by using Idris’ Foreign Function Interface (FFI). There is a special function foreign for this purpose. Here is a function onClick that takes a JavaScript query selector as a String and a callback function, and adds a click event listener to the selected element:

The important parts here are: the second argument to foreign, a String containing the JavaScript to be run; and the third argument which is the type of the JavaScript function being called. In the JavaScript code string, the special symbols %0 and %1 mean replace this with the zeroth and first arguments respectively.

We need to add a wrapper function for each function in helpers.js:

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 BattleCmd:

• Ready is the state of the system before any game state data has been read in.
• Done is the state after the game state has been written back out.
• ReadError is entered if there was a problem reading the game state.

• ReadState attempts to read in the game state. If it was successful, the next state is the loaded state; otherwise, it goes to the ReadError state.
• WriteState writes the state back out then moves to Done.
• GiveUp can 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 Dead and NotDead, from states used for reading and writing housekeeping, such as Ready and Done. We use Writable in the definitions of ReadState and 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 Show for 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

At the moment, we have some Idris functions that call out to JavaScript functions that manipulate persistent state, and a way of defining sequences of abstract commands that ensure we remember to read and write state properly, but we haven’t said what should actually happen when a command is executed. To do this, we’ll define a function runCmd' that translates values of type BattleCmd into IO operations. This is where the JavaScript helper functions defined in the previous section will come in useful:

For some of the commands that move between game states, such as Start and Die, there’s no IO action that needs to be performed, so the right-hand side of these equations is pure (), effectively “do nothing”. Punch, Kick and Magic require that we return a randomly generated move for the enemy, so we call out to enemyResponse, one of the Idris-wrapped JavaScript helper functions. The commands related to reading and writing state also call out to helper functions.

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 Ready and 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 runCmd:

Now the only way to turn sequences of commands into real world actions is if the sequence includes actions that read and write state.

User commands

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 BattleCmd.

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 doKick, doPunch and doMagic. These three functions are very similar so I’ll only go over doKick in detail.

• Just (state ** w) <- ReadState | Nothing => GiveUp reads in the game state from a JavaScript object, or goes to GiveUp if there was an error.
• We match on the state with case state of. If the state is not NotDead with 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 Kick command, capturing its return value — the attack the enemy used — in res.
• We match on res.
• If res was a kick, neither player should lose any health (we don’t have a choice here; this is enforced by the type system), so we log that the enemy used a kick, show the state of the game, and write the state back to the JavaScript object. Note that to call ShowStatus and WriteState, we need to pass in a Writable value of the state we want to show or write. This makes sure that we can only ever write or show a game state.
• If res was 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 Won state with the Win command. In either case, the state is shown to the UI and written back to the JavaScript object.
• If res was 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 Die to move to the Dead state. As always the state is shown to the UI and written back to the JavaScript object.

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 helpers.js:

Be careful that these are defined outside the gameState function — 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:

• doAction links a user command to the corresponding IO actions.
• setUp creates 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.
• main runs 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!

Conclusion

It’s certainly more upfront work writing JavaScript applications using Idris, but I think this is more than made up for by the increased confidence a programmer has in the correctness of her application. Figuring out how to write this sample program took me longer than it would have had I made it in plain JavaScript, but I haven’t had any head-scratching bugs either. In the rare case where I did manage to get bugs through the type checker, it was usually because I messed up something in the HTML or JavaScript side. The small battle game in this article is only a toy program, but I hope I’ve demonstrated one way that Idris can be used to create JavaScript applications that do what you want them to do.