State Machines in Types — Idris 1.0 documentation

# State Machines in Types

In the introduction, we saw the following state transition diagram representing the (abstract) states of a data store, and the actions we can perform on the store:

We say that these are the abstract states of the store, because the concrete state will contain a lot more information: for example, it might contain user names, hashed passwords, the store contents, and so on. However, as far as we are concerned for the actions `login`, `logout` and `readSecret`, it’s whether we are logged in or not which affects which are valid.

We’ve seen how to manipulate states using `ST`, and some small examples of dependent types in states. In this section, we’ll see how to use `ST` to provide a safe API for the data store. In the API, we’ll encode the above diagram in the types, in such a way that we can only execute the operations `login`, `logout` and `readSecret` when the state is valid.

So far, we’ve used `State` and the primitive operations, `new`, `read`, `write` and `delete` to manipulate states. For the data store API, however, we’ll begin by defining an interface (see Interfaces in the Idris tutorial) which describes the operations on the store, and explains in their types exactly when each operation is valid, and how it affects the store’s state. By using an interface, we can be sure that this is the only way to access the store.

## Defining an interface for the data store

We’ll begin by defining a data type, in a file `Login.idr`, which represents the two abstract states of the store, either `LoggedOut` or `LoggedIn`:

    data Access = LoggedOut | LoggedIn

We can define a data type for representing the current state of a store, holding all of the necessary information (this might be user names, hashed passwords, store contents and so on) and parameterise it by the logged in status of the store:

    Store : Access -> Type

Rather than defining a concrete type now, however, we’ll include this in a data store interface and define a concrete type later:

    interface DataStore (m : Type -> Type) where
      Store : Access -> Type

We can continue to populate this interface with operations on the store. Among other advantages, by separating the interface from its implementation we can provide different concrete implementations for different contexts. Furthermore, we can write programs which work with a store without needing to know any details of how the store is implemented.

We’ll need to be able to `connect` to a store, and `disconnect` when we’re done. Add the following methods to the `DataStore` interface:

    connect : ST m Var [add (Store LoggedOut)]
    disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]

The type of `connect` says that it returns a new resource which has the initial type `Store LoggedOut`. Conversely, `disconnect`, given a resource in the state `Store LoggedOut`, removes that resource. We can see more clearly what `connect` does by trying the following (incomplete) definition:

    doConnect : DataStore m => ST m () []
    doConnect = do st <- connect
                   ?whatNow

Note that we’re working in a generic context `m`, constrained so that there must be an implementation of `DataStore` for `m` to be able to execute `doConnect`. If we check the type of `?whatNow`, we’ll see that the remaining operations begin with a resource `st` in the state `Store LoggedOut`, and we need to finish with no resources.

      m : Type -> Type
      constraint : DataStore m
      st : Var
    --------------------------------------
    whatNow : STrans m () [st ::: Store LoggedOut] (\result => [])

Then, we can remove the resource using `disconnect`:

    doConnect : DataStore m => ST m () []
    doConnect = do st <- connect
                   disconnect st
                   ?whatNow

Now checking the type of `?whatNow` shows that we have no resources available:

      m : Type -> Type
      constraint : DataStore m
      st : Var
    --------------------------------------
    whatNow : STrans m () [] (\result => [])

To continue our implementation of the `DataStore` interface, next we’ll add a method for reading the secret data. This requires that the `store` is in the state `Store LoggedIn`:

    readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]

At this point we can try writing a function which connects to a store, reads the secret, then disconnects. However, it will be unsuccessful, because `readSecret` requires us to be logged in:

    badGet : DataStore m => ST m () []
    badGet = do st <- connect
                secret <- readSecret st
                disconnect st

This results in the following error, because `connect` creates a new store in the `LoggedOut` state, and `readSecret` requires the store to be in the `LoggedIn` state:

    When checking an application of function Control.ST.>>=:
        Error in state transition:
                Operation has preconditions: [st ::: Store LoggedOut]
                States here are: [st ::: Store LoggedIn]
                Operation has postconditions: \result => []
                Required result states here are: \result => []

The error message explains how the required input states (the preconditions) and the required output states (the postconditions) differ from the states in the operation. In order to use `readSecret`, we’ll need a way to get from a `Store LoggedOut` to a `Store LoggedIn`. As a first attempt, we can try the following type for `login`:

    login : (store : Var) -> ST m () [store ::: Store LoggedOut :-> Store LoggedIn] -- Incorrect type!

Note that in the interface we say nothing about how `login` works; merely how it affects the overall state. Even so, there is a problem with the type of `login`, because it makes the assumption that it will always succeed. If it fails - for example because the implementation prompts for a password and the user enters the password incorrectly - then it must not result in a `LoggedIn` store.

Instead, therefore, `login` will return whether logging in was successful, via the following type;

    data LoginResult = OK | BadPassword

Then, we can calculate the result state (see Manipulating State with dependent types) from the result. Add the following method to the `DataStore` interface:

    login : (store : Var) ->
            ST m LoginResult [store ::: Store LoggedOut :->
                               (\res => Store (case res of
                                                    OK => LoggedIn
                                                    BadPassword => LoggedOut))]

If `login` was successful, then the state after `login` is `Store LoggedIn`. Otherwise, the state is `Store LoggedOut`.

To complete the interface, we’ll add a method for logging out of the store. We’ll assume that logging out is always successful, and moves the store from the `Store LoggedIn` state to the `Store LoggedOut` state.

    logout : (store : Var) -> ST m () [store ::: Store LoggedIn :-> Store LoggedOut]

This completes the interface, repeated in full for reference below:

    interface DataStore (m : Type -> Type) where
      Store : Access -> Type

      connect : ST m Var [add (Store LoggedOut)]
      disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]

      readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]
      login : (store : Var) ->
              ST m LoginResult [store ::: Store LoggedOut :->
                                 (\res => Store (case res of
                                                      OK => LoggedIn
                                                      BadPassword => LoggedOut))]
      logout : (store : Var) -> ST m () [store ::: Store LoggedIn :-> Store LoggedOut]

Before we try creating any implementations of this interface, let’s see how we can write a function with it, to log into a data store, read the secret if login is successful, then log out again.

## Writing a function with the data store

As an example of working with the `DataStore` interface, we’ll write a function `getData`, which connects to a store in order to read some data from it. We’ll write this function interactively, step by step, using the types of the operations to guide its development. It has the following type:

    getData : (ConsoleIO m, DataStore m) => ST m () []

This type means that there are no resources available on entry or exit. That is, the overall list of actions is `[]`, meaning that at least externally, the function has no overall effect on the resources. In other words, for every resource we create during `getData`, we’ll also need to delete it before exit.

Since we want to use methods of the `DataStore` interface, we’ll constraint the computation context `m` so that there must be an implementation of `DataStore`. We also have a constraint `ConsoleIO m` so that we can display any data we read from the store, or any error messages.

We start by connecting to the store, creating a new resource `st`, then trying to `login`:

    getData : (ConsoleIO m, DataStore m) => ST m () []
    getData = do st <- connect
                 ok <- login st
                 ?whatNow

Logging in will either succeed or fail, as reflected by the value of `ok`. If we check the type of `?whatNow`, we’ll see what state the store currently has:

      m : Type -> Type
      constraint : ConsoleIO m
      constraint1 : DataStore m
      st : Var
      ok : LoginResult
    --------------------------------------
    whatNow : STrans m () [st ::: Store (case ok of
                                              OK => LoggedIn
                                              BadPassword => LoggedOut)]
                          (\result => [])

The current state of `st` therefore depends on the value of `ok`, meaning that we can make progress by case splitting on `ok`:

    getData : (ConsoleIO m, DataStore m) => ST m () []
    getData = do st <- connect
                 ok <- login st
                 case ok of
                      OK => ?whatNow_1
                      BadPassword => ?whatNow_2

The types of the holes in each branch, `?whatNow_1` and `?whatNow_2`, show how the state changes depending on whether logging in was successful. If it succeeded, the store is `LoggedIn`:

    --------------------------------------
    whatNow_1 : STrans m () [st ::: Store LoggedIn] (\result => [])

On the other hand, if it failed, the store is `LoggedOut`:

    --------------------------------------
    whatNow_2 : STrans m () [st ::: Store LoggedOut] (\result => [])

In `?whatNow_1`, since we’ve successfully logged in, we can now read the secret and display it to the console:

    getData : (ConsoleIO m, DataStore m) => ST m () []
    getData = do st <- connect
                 ok <- login st
                 case ok of
                      OK => do secret <- readSecret st
                               putStrLn ("Secret is: " ++ show secret)
                               ?whatNow_1
                      BadPassword => ?whatNow_2

We need to finish the `OK` branch with no resources available. We can do this by logging out of the store then disconnecting:

    getData : (ConsoleIO m, DataStore m) => ST m () []
    getData = do st <- connect
                 ok <- login st
                 case ok of
                      OK => do secret <- readSecret st
                               putStrLn ("Secret is: " ++ show secret)
                               logout st
                               disconnect st
                      BadPassword => ?whatNow_2

Note that we must `logout` of `st` before calling `disconnect`, because `disconnect` requires that the store is in the `LoggedOut` state.

Furthermore, we can’t simply use `delete` to remove the resource, as we did with the `State` examples in the previous section, because `delete` only works when the resource has type `State ty`, for some type `ty`. If we try to use `delete` instead of `disconnect`, we’ll see an error message like the following:

    When checking argument prf to function Control.ST.delete:
            Can't find a value of type
                    InState st (State st) [st ::: Store LoggedOut]

In other words, the type checker can’t find a proof that the resource `st` has a type of the form `State st`, because its type is `Store LoggedOut`. Since `Store` is part of the `DataStore` interface, we can’t yet know the concrete representation of the `Store`, so we need to remove the resource via the interface, with `disconnect`, rather than directly with `delete`.

We can complete `getData` as follows, using a pattern matching bind alternative (see the Idris tutorial, Monads and do-notation) rather than a `case` statement to catch the possibility of an error with `login`:

    getData : (ConsoleIO m, DataStore m) => ST m () []
    getData = do st <- connect
                 OK <- login st
                    | BadPassword => do putStrLn "Failure"
                                        disconnect st
                 secret <- readSecret st
                 putStrLn ("Secret is: " ++ show secret)
                 logout st
                 disconnect st

We can’t yet try this out, however, because we don’t have any implementations of `DataStore`! If we try to execute it in an `IO` context, for example, we’ll get an error saying that there’s no implementation of `DataStore IO`:

    *Login> :exec run {m = IO} getData
    When checking an application of function Control.ST.run:
            Can't find implementation for DataStore IO

The final step in implementing a data store which correctly follows the state transition diagram, therefore, is to provide an implementation of `DataStore`.

## Implementing the interface

To execute `getData` in `IO`, we’ll need to provide an implementation of `DataStore` which works in the `IO` context. We can begin as follows:

    implementation DataStore IO where

Then, we can ask Idris to populate the interface with skeleton definitions for the necessary methods (press `Ctrl-Alt-A` in Atom for “add definition” or the corresponding shortcut for this in the Idris mode in your favourite editor):

    implementation DataStore IO where
      Store x = ?DataStore_rhs_1
      connect = ?DataStore_rhs_2
      disconnect store = ?DataStore_rhs_3
      readSecret store = ?DataStore_rhs_4
      login store = ?DataStore_rhs_5
      logout store = ?DataStore_rhs_6

The first decision we’ll need to make is how to represent the data store. We’ll keep this simple, and store the data as a single `String`, using a hard coded password to gain access. So, we can define `Store` as follows, using a `String` to represent the data no matter whether we are `LoggedOut` or `LoggedIn`:

    Store x = State String

Now that we’ve given a concrete type for `Store`, we can implement operations for connecting, disconnecting, and accessing the data. And, since we used `State`, we can use `new`, `delete`, `read` and `write` to manipulate the store.

Looking at the types of the holes tells us how we need to manipulate the state. For example, the `?DataStore_rhs_2` hole tells us what we need to do to implement `connect`. We need to return a new `Var` which represents a resource of type `State String`:

    --------------------------------------
    DataStore_rhs_2 : STrans IO Var [] (\result => [result ::: State String])

We can implement this by creating a new variable with some data for the content of the store (we can use any `String` for this) and returning that variable:

    connect = do store <- new "Secret Data"
                 pure store

For `disconnect`, we only need to delete the resource:

    disconnect store = delete store

For `readSecret`, we need to read the secret data and return the `String`. Since we now know the concrete representation of the data is a `State String`, we can use `read` to access the data directly:

    readSecret store = read store

We’ll do `logout` next and return to `login`. Checking the hole reveals the following:

      store : Var
    --------------------------------------
    DataStore_rhs_6 : STrans IO () [store ::: State String] (\result => [store ::: State String])

So, in this minimal implementation, we don’t actually have to do anything!

    logout store = pure ()

For `login`, we need to return whether logging in was successful. We’ll do this by prompting for a password, and returning `OK` if it matches a hard coded password, or `BadPassword` otherwise:

    login store = do putStr "Enter password: "
                     p <- getStr
                     if p == "Mornington Crescent"
                        then pure OK
                        else pure BadPassword

For reference, here is the complete implementation which allows us to execute a `DataStore` program at the REPL:

    implementation DataStore IO where
      Store x = State String
      connect = do store <- new "Secret Data"
                   pure store
      disconnect store = delete store
      readSecret store = read store
      login store = do putStr "Enter password: "
                       p <- getStr
                       if p == "Mornington Crescent"
                          then pure OK
                          else pure BadPassword
      logout store = pure ()

Finally, we can try this at the REPL as follows (Idris defaults to the `IO` context at the REPL if there is an implementation available, so no need to give the `m` argument explicitly here):

    *Login> :exec run getData
    Enter password: Mornington Crescent
    Secret is: "Secret Data"

    *Login> :exec run getData
    Enter password: Dollis Hill
    Failure

We can only use `read`, `write`, `new` and `delete` on a resource with a `State` type. So, within the implementation of `DataStore`, or anywhere where we know the context is `IO`, we can access the data store however we like: this is where the internal details of `DataStore` are implemented. However, if we merely have a constraint `DataStore m`, we can’t know how the store is implemented, so we can only access via the API given by the `DataStore` interface.

It is therefore good practice to use a generic context `m` for functions like `getData`, and constrain by only the interfaces we need, rather than using a concrete context `IO`.

We’ve now seen how to manipulate states, and how to encapsulate state transitions for a specific system like the data store in an interface. However, realistic systems will need to compose state machines. We’ll either need to use more than one state machine at a time, or implement one state machine in terms of one or more others. We’ll see how to achieve this in the next section.