Overview

Pure functional languages with dependent types such as Idris support reasoning about programs directly in the type system, promising that we can know a program will run correctly (i.e. according to the specification in its type) simply because it compiles.

Realistically, though, software relies on state, and many components rely on state machines. For example, they describe network transport protocols like TCP, and implement event-driven systems and regular expression matching. Furthermore, many fundamental resources like network sockets and files are, implicitly, managed by state machines, in that certain operations are only valid on resources in certain states, and those operations can change the states of the underlying resource. For example, it only makes sense to send a message on a connected network socket, and closing a socket changes its state from “open” to “closed”. State machines can also encode important security properties. For example, in the software which implements an ATM, it’s important that the ATM dispenses cash only when the machine is in a state where a card has been inserted and the PIN verified.

In this tutorial we will introduce the Control.ST library, which is included with the Idris distribution (currently as part of the contrib package) and supports programming and reasoning with state and side effects. This tutorial assumes familiarity with pure programming in Idris, as described in The Idris Tutorial. For further background information, the ST library is based on ideas discussed in Chapter 13 (available as a free sample chapter) and Chapter 14 of Type-Driven Development with Idris.

The ST library allows us to write programs which are composed of multiple state transition systems. It supports composition in two ways: firstly, we can use several independently implemented state transition systems at once; secondly, we can implement one state transition system in terms of others.

Introductory example: a data store requiring a login

Many software components rely on some form of state, and there may be operations which are only valid in specific states. For example, consider a secure data store in which a user must log in before getting access to some secret data. This system can be in one of two states:

• LoggedIn, in which the user is allowed to read the secret
• LoggedOut, in which the user has no access to the secret

We can provide commands to log in, log out, and read the data, as illustrated in the following diagram:

The login command, if it succeeds, moves the overall system state from LoggedOut to LoggedIn. The logout command moves the state from LoggedIn to LoggedOut. Most importantly, the readSecret command is only valid when the system is in the LoggedIn state.

We routinely use type checkers to ensure that variables and arguments are used consistently. However, statically checking that operations are performed only on resources in an appropriate state is not well supported by mainstream type systems. In the data store example, for example, it’s important to check that the user is successfully logged in before using readSecret. The ST library allows us to represent this kind of protocol in the type system, and ensure at compile-time that the secret is only read when the user is logged in.

Outline

This tutorial starts (Introducing ST: Working with State) by describing how to manipulate individual states, introduces a data type STrans for describing stateful functions, and ST which describes top level state transitions. Next (State Machines in Types) it describes how to represent state machines in types, and how to define interfaces for describing stateful systems. Then (Composing State Machines) it describes how to compose systems of multiple state machines. It explains how to implement systems which use several state machines at once, and how to implement a high level stateful system in terms of lower level systems. Finally (Example: Network Socket Programming) we’ll see a specific example of a stateful API in practice, implementing the POSIX network sockets API.

The Control.ST library is also described in a draft paper by Edwin Brady, “State Machines All The Way Down”, available here. This paper presents many of the examples from this tutorial, and describes the motivation, design and implementation of the library in more depth.