Introducing ST: Working with State

The Control.ST library provides facilities for creating, reading, writing and destroying state in Idris functions, and tracking changes of state in a function’s type. It is based around the concept of resources, which are, essentially, mutable variables, and a dependent type, STrans which tracks how those resources change when a function runs:

STrans : (m : Type -> Type) ->
         (resultType : Type) ->
         (in_res : Resources) ->
         (out_res : resultType -> Resources) ->
         Type

A value of type STrans m resultType in_res out_res_fn represents a sequence of actions which can manipulate state. The arguments are:

• m, which is an underlying computation context in which the actions will be executed. Usually, this will be a generic type with a Monad implementation, but it isn’t necessarily so. In particular, there is no need to understand monads to be able to use ST effectively!
• resultType, which is the type of the value the sequence will produce
• in_res, which is a list of resources available before executing the actions.
• out_res, which is a list of resources available after executing the actions, and may differ depending on the result of the actions.

We can use STrans to describe state transition systems in a function’s type. We’ll come to the definition of Resources shortly, but for the moment you can consider it an abstract representation of the “state of the world”. By giving the input resources (in_res) and the output resources (out_res) we are describing the preconditions under which a function is allowed to execute, and postconditions which describe how a function affects the overall state of the world.

We’ll begin in this section by looking at some small examples of STrans functions, and see how to execute them. We’ll also introduce ST, a type-level function which allows us to describe the state transitions of a stateful function concisely.

Type checking the examples

For the examples in this section, and throughout this tutorial, you’ll need to import Control.ST and add the contrib package by passing the -p contrib flag to idris.

Introductory examples: manipulating State

An STrans function explains, in its type, how it affects a collection of Resources. A resource has a label (of type Var), which we use to refer to the resource throughout the function, and we write the state of a resource, in the Resources list, in the form label ::: type.

For example, the following function has a resource x available on input, of type State Integer, and that resource is still a State Integer on output:

increment : (x : Var) -> STrans m () [x ::: State Integer]
                                     (const [x ::: State Integer])
increment x = do num <- read x
                 write x (num + 1)

Verbosity of the type of increment

The type of increment may seem somewhat verbose, in that the input and output resources are repeated, even though they are the same. We’ll introduce a much more concise way of writing this type at the end of this section (ST: Representing state transitions directly), when we describe the ST type itself.

This function reads the value stored at the resource x with read, increments it then writes the result back into the resource x with write. We’ll see the types of read and write shortly (see STrans Primitive operations). We can also create and delete resources:

makeAndIncrement : Integer -> STrans m Integer [] (const [])
makeAndIncrement init = do var <- new init
                           increment var
                           x <- read var
                           delete var
                           pure x

The type of makeAndIncrement states that it has no resources available on entry ([]) or exit (const []). It creates a new State resource with new (which takes an initial value for the resource), increments the value, reads it back, then deletes it using delete, returning the final value of the resource. Again, we’ll see the types of new and delete shortly.

The m argument to STrans (of type Type -> Type) is the computation context in which the function can be run. Here, the type level variable indicates that we can run it in any context. We can run it in the identity context with runPure. For example, try entering the above definitions in a file Intro.idr then running the following at the REPL:

*Intro> runPure (makeAndIncrement 93)
94 : Integer

It’s a good idea to take an interactive, type-driven approach to implementing STrans programs. For example, after creating the resource with new init, you can leave a hole for the rest of the program to see how creating the resource has affected the type:

makeAndIncrement : Integer -> STrans m Integer [] (const [])
makeAndIncrement init = do var <- new init
                           ?whatNext

If you check the type of ?whatNext, you’ll see that there is now a resource available, var, and that by the end of the function there should be no resource available:

  init : Integer
  m : Type -> Type
  var : Var
--------------------------------------
whatNext : STrans m Integer [var ::: State Integer] (\value => [])

These small examples work in any computation context m. However, usually, we are working in a more restricted context. For example, we might want to write programs which only work in a context that supports interactive programs. For this, we’ll need to see how to lift operations from the underlying context.

Lifting: Using the computation context

Let’s say that, instead of passing an initial integer to makeAndIncrement, we want to read it in from the console. Then, instead of working in a generic context m, we can work in the specific context IO:

ioMakeAndIncrement : STrans IO () [] (const [])

This gives us access to IO operations, via the lift function. We can define ioMakeAndIncrement as follows:

ioMakeAndIncrement : STrans IO () [] (const [])
ioMakeAndIncrement
   = do lift $ putStr "Enter a number: "
        init <- lift $ getLine
        var <- new (cast init)
        lift $ putStrLn ("var = " ++ show !(read var))
        increment var
        lift $ putStrLn ("var = " ++ show !(read var))
        delete var

The lift function allows us to use funtions from the underlying computation context (IO here) directly. Again, we’ll see the exact type of lift shortly.

!-notation

In ioMakeAndIncrement we’ve used !(read var) to read from the resource. You can read about this !-notation in the main Idris tutorial (see Monads and do-notation). In short, it allows us to use an STrans function inline, rather than having to bind the result to a variable first.

Conceptually, at least, you can think of it as having the following type:

(!) : STrans m a state_in state_out -> a

It is syntactic sugar for binding a variable immediately before the current action in a do block, then using that variable in place of the !-expression.

In general, though, it’s bad practice to use a specific context like IO. Firstly, it requires us to sprinkle lift liberally throughout our code, which hinders readability. Secondly, and more importantly, it will limit the safety of our functions, as we’ll see in the next section (State Machines in Types).

So, instead, we define interfaces to restrict the computation context. For example, Control.ST defines a ConsoleIO interface which provides the necessary methods for performing basic console interaction:

interface ConsoleIO (m : Type -> Type) where
  putStr : String -> STrans m () res (const res)
  getStr : STrans m String res (const res)

That is, we can write to and read from the console with any available resources res, and neither will affect the available resources. This has the following implementation for IO:

ConsoleIO IO where
  putStr str = lift (Interactive.putStr str)
  getStr = lift Interactive.getLine

Now, we can define ioMakeAndIncrement as follows:

ioMakeAndIncrement : ConsoleIO io => STrans io () [] (const [])
ioMakeAndIncrement
   = do putStr "Enter a number: "
        init <- getStr
        var <- new (cast init)
        putStrLn ("var = " ++ show !(read var))
        increment var
        putStrLn ("var = " ++ show !(read var))
        delete var

Instead of working in IO specifically, this works in a generic context io, provided that there is an implementation of ConsoleIO for that context. This has several advantages over the first version:

• All of the calls to lift are in the implementation of the interface, rather than ioMakeAndIncrement
• We can provide alternative implementations of ConsoleIO, perhaps supporting exceptions or logging in addition to basic I/O.
• As we’ll see in the next section (State Machines in Types), it will allow us to define safe APIs for manipulating specific resources more precisely.

Earlier, we used runPure to run makeAndIncrement in the identity context. Here, we use run, which allows us to execute an STrans program in any context (as long as it has an implementation of Applicative) and we can execute ioMakeAndIncrement at the REPL as follows:

*Intro> :exec run ioMakeAndIncrement
Enter a number: 93
var = 93
var = 94

Manipulating State with dependent types

In our first example of State, when we incremented the value its type remained the same. However, when we’re working with dependent types, updating a state may also involve updating its type. For example, if we’re adding an element to a vector stored in a state, its length will change:

addElement : (vec : Var) -> (item : a) ->
             STrans m () [vec ::: State (Vect n a)]
                  (const [vec ::: State (Vect (S n) a)])
addElement vec item = do xs <- read vec
                         write vec (item :: xs)

Note that you’ll need to import Data.Vect to try this example.

Updating a state directly with update

Rather than using read and write separately, you can also use update which reads from a State, applies a function to it, then writes the result. Using update you could write addElement as follows:

addElement : (vec : Var) -> (item : a) ->
             STrans m () [vec ::: State (Vect n a)]
                  (const [vec ::: State (Vect (S n) a)])
addElement vec item = update vec (item ::)

We don’t always know how exactly the type will change in the course of a sequence actions, however. For example, if we have a state containing a vector of integers, we might read an input from the console and only add it to the vector if the input is a valid integer. Somehow, we need a different type for the output state depending on whether reading the integer was successful, so neither of the following types is quite right:

readAndAdd_OK : ConsoleIO io => (vec : Var) ->
                STrans m ()  -- Returns an empty tuple
                            [vec ::: State (Vect n Integer)]
                     (const [vec ::: State (Vect (S n) Integer)])
readAndAdd_Fail : ConsoleIO io => (vec : Var) ->
                  STrans m ()  -- Returns an empty tuple
                              [vec ::: State (Vect n Integer)]
                       (const [vec ::: State (Vect n Integer)])

Remember, though, that the output resource types can be computed from the result of a function. So far, we’ve used const to note that the output resources are always the same, but here, instead, we can use a type level function to calculate the output resources. We start by returning a Bool instead of an empty tuple, which is True if reading the input was successful, and leave a hole for the output resources:

readAndAdd : ConsoleIO io => (vec : Var) ->
             STrans m Bool [vec ::: State (Vect n Integer)]
                           ?output_res

If you check the type of ?output_res, you’ll see that Idris expects a function of type Bool -> Resources, meaning that the output resource type can be different depending on the result of readAndAdd:

  n : Nat
  m : Type -> Type
  io : Type -> Type
  constraint : ConsoleIO io
  vec : Var
--------------------------------------
output_res : Bool -> Resources

So, the output resource is either a Vect n Integer if the input is invalid (i.e. readAndAdd returns False) or a Vect (S n) Integer if the input is valid. We can express this in the type as follows:

readAndAdd : ConsoleIO io => (vec : Var) ->
             STrans io Bool [vec ::: State (Vect n Integer)]
                   (\res => [vec ::: State (if res then Vect (S n) Integer
                                                   else Vect n Integer)])

Then, when we implement readAndAdd we need to return the appropriate value for the output state. If we’ve added an item to the vector, we need to return True, otherwise we need to return False:

readAndAdd : ConsoleIO io => (vec : Var) ->
             STrans io Bool [vec ::: State (Vect n Integer)]
                   (\res => [vec ::: State (if res then Vect (S n) Integer
                                                   else Vect n Integer)])
readAndAdd vec = do putStr "Enter a number: "
                    num <- getStr
                    if all isDigit (unpack num)
                       then do
                         update vec ((cast num) ::)
                         pure True     -- added an item, so return True
                       else pure False -- didn't add, so return False

There is a slight difficulty if we’re developing interactively, which is that if we leave a hole, the required output state isn’t easily visible until we know the value that’s being returned. For example. in the following incomplete definition of readAndAdd we’ve left a hole for the successful case:

readAndAdd vec = do putStr "Enter a number: "
                    num <- getStr
                    if all isDigit (unpack num)
                       then ?whatNow
                       else pure False

We can look at the type of ?whatNow, but it is unfortunately rather less than informative:

  vec : Var
  n : Nat
  io : Type -> Type
  constraint : ConsoleIO io
  num : String
--------------------------------------
whatNow : STrans io Bool [vec ::: State (Vect (S n) Integer)]
                 (\res =>
                    [vec :::
                     State (ifThenElse res
                                       (Delay (Vect (S n) Integer))
                                       (Delay (Vect n Integer)))])

The problem is that we’ll only know the required output state when we know the value we’re returning. To help with interactive development, Control.ST provides a function returning which allows us to specify the return value up front, and to update the state accordingly. For example, we can write an incomplete readAndAdd as follows:

readAndAdd vec = do putStr "Enter a number: "
                    num <- getStr
                    if all isDigit (unpack num)
                       then returning True ?whatNow
                       else pure False

This states that, in the successful branch, we’ll be returning True, and ?whatNow should explain how to update the states appropriately so that they are correct for a return value of True. We can see this by checking the type of ?whatNow, which is now a little more informative:

  vec : Var
  n : Nat
  io : Type -> Type
  constraint : ConsoleIO io
  num : String
--------------------------------------
whatnow : STrans io () [vec ::: State (Vect n Integer)]
                 (\value => [vec ::: State (Vect (S n) Integer)])

This type now shows, in the output resource list of STrans, that we can complete the definition by adding an item to vec, which we can do as follows:

readAndAdd vec = do putStr "Enter a number: "
                    num <- getStr
                    if all isDigit (unpack num)
                       then returning True (update vec ((cast num) ::))
                       else returning False (pure ()) -- returning False, so no state update required

STrans Primitive operations

Now that we’ve written a few small examples of STrans functions, it’s a good time to look more closely at the types of the state manipulation functions we’ve used. First, to read and write states, we’ve used read and write:

read : (lbl : Var) -> {auto prf : InState lbl (State ty) res} ->
       STrans m ty res (const res)
write : (lbl : Var) -> {auto prf : InState lbl ty res} ->
        (val : ty') ->
        STrans m () res (const (updateRes res prf (State ty')))

These types may look a little daunting at first, particularly due to the implicit prf argument, which has the following type:

prf : InState lbl (State ty) res}

This relies on a predicate InState. A value of type InState x ty res means that the reference x must have type ty in the list of resources res. So, in practice, all this type means is that we can only read or write a resource if a reference to it exists in the list of resources.

Given a resource label res, and a proof that res exists in a list of resources, updateRes will update the type of that resource. So, the type of write states that the type of the resource will be updated to the type of the given value.

The type of update is similar to that for read and write, requiring that the resource has the input type of the given function, and updating it to have the output type of the function:

update : (lbl : Var) -> {auto prf : InState lbl (State ty) res} ->
         (ty -> ty') ->
         STrans m () res (const (updateRes res prf (State ty')))

The type of new states that it returns a Var, and given an initial value of type state, the output resources contains a new resource of type State state:

new : (val : state) ->
      STrans m Var res (\lbl => (lbl ::: State state) :: res)

It’s important that the new resource has type State state, rather than merely state, because this will allow us to hide implementation details of APIs. We’ll see more about what this means in the next section, State Machines in Types.

The type of delete states that the given label will be removed from the list of resources, given an implicit proof that the label exists in the input resources:

delete : (lbl : Var) -> {auto prf : InState lbl (State st) res} ->
         STrans m () res (const (drop res prf))

Here, drop is a type level function which updates the resource list, removing the given resource lbl from the list.

We’ve used lift to run functions in the underlying context. It has the following type:

lift : Monad m => m t -> STrans m t res (const res)

Given a result value, pure is an STrans program which produces that value, provided that the current list of resources is correct when producing that value:

pure : (result : ty) -> STrans m ty (out_fn result) out_fn

We can use returning to break down returning a value from an STrans functions into two parts: providing the value itself, and updating the resource list so that it is appropriate for returning that value:

returning : (result : ty) ->
            STrans m () res (const (out_fn result)) ->
            STrans m ty res out_fn

Finally, we’ve used run and runPure to execute STrans functions in a specific context. run will execute a function in any context, provided that there is an Applicative implementation for that context, and runPure will execute a function in the identity context:

run : Applicative m => STrans m a [] (const []) -> m a
runPure : STrans Basics.id a [] (const []) -> a

Note that in each case, the input and output resource list must be empty. There’s no way to provide an initial resource list, or extract the final resources. This is deliberate: it ensures that all resource management is carried out in the controlled STrans environment and, as we’ll see, this allows us to implement safe APIs with precise types explaining exactly how resources are tracked throughout a program.

These functions provide the core of the ST library; there are some others which we’ll encounter later, for more advanced situations, but the functions we have seen so far already allow quite sophisticated state-aware programming and reasoning in Idris.

ST: Representing state transitions directly

We’ve seen a few examples of small STrans functions now, and their types can become quite verbose given that we need to provide explicit input and output resource lists. This is convenient for giving types for the primitive operations, but for more general use it’s much more convenient to be able to express transitions on individual resources, rather than giving input and output resource lists in full. We can do this with ST:

ST : (m : Type -> Type) ->
     (resultType : Type) ->
     List (Action resultType) -> Type

ST is a type level function which computes an appropriate STrans type given a list of actions, which describe transitions on resources. An Action in a function type can take one of the following forms (plus some others which we’ll see later in the tutorial):

• lbl ::: ty expresses that the resource lbl begins and ends in the state ty
• lbl ::: ty_in :-> ty_out expresses that the resource lbl begins in state ty_in and ends in state ty_out
• lbl ::: ty_in :-> (\res -> ty_out) expresses that the resource lbl begins in state ty_in and ends in a state ty_out, where ty_out is computed from the result of the function res.

So, we can write some of the function types we’ve seen so far as follows:

increment : (x : Var) -> ST m () [x ::: State Integer]

That is, increment begins and ends with x in state State Integer.

makeAndIncrement : Int -> ST m Int []

That is, makeAndIncrement begins and ends with no resources.

addElement : (vec : Var) -> (item : a) ->
             ST m () [vec ::: State (Vect n a) :-> State (Vect (S n) a)]

That is, addElement changes vec from State (Vect n a) to State (Vect (S n) a).

readAndAdd : ConsoleIO io => (vec : Var) ->
             ST io Bool
                   [vec ::: State (Vect n Integer) :->
                    \res => State (if res then Vect (S n) Integer
                                          else Vect n Integer)]

By writing the types in this way, we express the minimum necessary to explain how each function affects the overall resource state. If there is a resource update depending on a result, as with readAndAdd, then we need to describe it in full. Otherwise, as with increment and makeAndIncrement, we can write the input and output resource lists without repetition.

An Action can also describe adding and removing states:

• add ty, assuming the operation returns a Var, adds a new resource of type ty.
• remove lbl ty expresses that the operation removes the resource named lbl, beginning in state ty from the resource list.

So, for example, we can write:

newState : ST m Var [add (State Int)]
removeState : (lbl : Var) -> ST m () [remove lbl (State Int)]

The first of these, newState, returns a new resource label, and adds that resource to the list with type State Int. The second, removeState, given a label lbl, removes the resource from the list. These types are equivalent to the following:

newState : STrans m Var [] (\lbl => [lbl ::: State Int])
removeState : (lbl : Var) -> STrans m () [lbl ::: State Int] (const [])

These are the primitive methods of constructing an Action. Later, we will encounter some other ways using type level functions to help with readability.

In the remainder of this tutorial, we will generally use ST except on the rare occasions we need the full precision of STrans. In the next section, we’ll see how to use the facilities provided by ST to write a precise API for a system with security properties: a data store requiring a login.