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
and supports programming and reasoning with state and side effects. This
tutorial assumes familiarity with pure programming in Idris, as described in
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.
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:
login command, if it succeeds, moves the overall system state from
logout command moves the state from
LoggedOut. Most importantly, the
is only valid when the system is in the
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
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.
This tutorial starts (:ref:`introst`) by describing how to manipulate
individual states, introduces a data type
STrans for describing stateful
ST which describes top level state transitions.
Next (:ref:`smstypes`) it describes how to represent state machines in
types, and how to define interfaces for describing stateful systems.
Then (:ref:`composing`) 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 (:ref:`netexample`) we'll see a specific example of a stateful
API in practice, implementing the POSIX network sockets API.
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.