Composing State Machines

In the previous section, we defined a DataStore interface and used it to implement the following small program which allows a user to log in to the store then display the store’s contents;

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

This function only uses one state, the store itself. Usually, though, larger programs have lots of states, and might add, delete and update states over the course of its execution. Here, for example, a useful extension might be to loop forever, keeping count of the number of times there was a login failure in a state.

Furthermore, we may have hierarchies of state machines, in that one state machine could be implemented by composing several others. For example, we can have a state machine representing the state of a graphics system, and use this to implement a higher level graphics API such as turtle graphics, which uses the graphics system plus some additional state for the turtle.

In this section, we’ll see how to work with multiple states, and how to compose state machines to make higher level state machines. We’ll begin by seeing how to add a login failure counter to getData.

Working with multiple resources

To see how to work with multiple resources, we’ll modify getData so that it loops, and counts the total number of times the user fails to log in. For example, if we write a main program which initialises the count to zero, a session might run as follows:

*LoginCount> :exec main
Enter password: Mornington Crescent
Secret is: "Secret Data"
Enter password: Dollis Hill
Failure
Number of failures: 1
Enter password: Mornington Crescent
Secret is: "Secret Data"
Enter password: Codfanglers
Failure
Number of failures: 2
...

We’ll start by adding a state resource to getData to keep track of the number of failures:

getData : (ConsoleIO m, DataStore m) =>
          (failcount : Var) -> ST m () [failcount ::: State Integer]

Type checking getData

If you’re following along in the code, you’ll find that getData no longer compiles when you update this type. That is to be expected! For the moment, comment out the definition of getData. We’ll come back to it shortly.

Then, we can create a main program which initialises the state to 0 and invokes getData, as follows:

main : IO ()
main = run (do fc <- new 0
               getData fc
               delete fc)

We’ll start our implementation of getData just by adding the new argument for the failure count:

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

Unfortunately, this doesn’t type check, because we have the wrong resources for calling connect. The error messages shows how the resources don’t match:

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

In other words, connect requires that there are no resources on entry, but we have one, the failure count! This shouldn’t be a problem, though: the required resources are a subset of the resources we have, after all, and the additional resources (here, the failure count) are not relevant to connect. What we need, therefore, is a way to temporarily hide the additional resource.

We can achieve this with the call function:

getData : (ConsoleIO m, DataStore m) =>
          (failcount : Var) -> ST m () [failcount ::: State Integer]
getData failcount
   = do st <- call connect
        ?whatNow

Here we’ve left a hole for the rest of getData so that you can see the effect of call. It has removed the unnecessary parts of the resource list for calling connect, then reinstated them on return. The type of whatNow therefore shows that we’ve added a new resource st, and still have failcount available:

  failcount : Var
  m : Type -> Type
  constraint : ConsoleIO m
  constraint1 : DataStore m
  st : Var
--------------------------------------
whatNow : STrans m () [failcount ::: State Integer, st ::: Store LoggedOut]
                      (\result => [failcount ::: State Integer])

By the end of the function, whatNow says that we need to have finished with st, but still have failcount available. We can complete getData so that it works with an additional state resource by adding call whenever we invoke one of the operations on the data store, to reduce the list of resources:

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

This is a little noisy, and in fact we can remove the need for it by making call implicit. By default, you need to add the call explicitly, but if you import Control.ST.ImplicitCall, Idris will insert call where it is necessary.

import Control.ST.ImplicitCall

It’s now possible to write getData exactly as before:

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

There is a trade off here: if you import Control.ST.ImplicitCall then functions which use multiple resources are much easier to read, because the noise of call has gone. On the other hand, Idris has to work a little harder to type check your functions, and as a result it can take slightly longer, and the error messages can be less helpful.

It is instructive to see the type of call:

call : STrans m t sub new_f -> {auto res_prf : SubRes sub old} ->
       STrans m t old (\res => updateWith (new_f res) old res_prf)

The function being called has a list of resources sub, and there is an implicit proof, SubRes sub old that the resource list in the function being called is a subset of the overall resource list. The ordering of resources is allowed to change, although resources which appear in old can’t appear in the sub list more than once (you will get a type error if you try this).

The function updateWith takes the output resources of the called function, and updates them in the current resource list. It makes an effort to preserve ordering as far as possible, although this isn’t always possible if the called function does some complicated resource manipulation.

Newly created resources in called functions

If the called function creates any new resources, these will typically appear at the end of the resource list, due to the way updateWith works. You can see this in the type of whatNow in our incomplete definition of getData above.

Finally, we can update getData so that it loops, and keeps failCount updated as necessary:

getData : (ConsoleIO m, DataStore m) =>
          (failcount : Var) -> ST m () [failcount ::: State Integer]
getData failcount
   = do st <- call connect
        OK <- login st
           | BadPassword => do putStrLn "Failure"
                               fc <- read failcount
                               write failcount (fc + 1)
                               putStrLn ("Number of failures: " ++ show (fc + 1))
                               disconnect st
                               getData failcount
        secret <- readSecret st
        putStrLn ("Secret is: " ++ show secret)
        logout st
        disconnect st
        getData failcount

Note that here, we’re connecting and disconnecting on every iteration. Another way to implement this would be to connect first, then call getData, and implement getData as follows:

getData : (ConsoleIO m, DataStore m) =>
          (st, failcount : Var) -> ST m () [st ::: Store {m} LoggedOut, failcount ::: State Integer]
getData st failcount
   = do OK <- login st
           | BadPassword => do putStrLn "Failure"
                               fc <- read failcount
                               write failcount (fc + 1)
                               putStrLn ("Number of failures: " ++ show (fc + 1))
                               getData st failcount
        secret <- readSecret st
        putStrLn ("Secret is: " ++ show secret)
        logout st
        getData st failcount

It is important to add the explicit {m} in the type of Store {m} LoggedOut for st, because this gives Idris enough information to know which implementation of DataStore to use to find the appropriate implementation for Store. Otherwise, if we only write Store LoggedOut, there’s no way to know that the Store is linked with the computation context m.

We can then connect and disconnect only once, in main:

main : IO ()
main = run (do fc <- new 0
               st <- connect
               getData st fc
               disconnect st
               delete fc)

By using call, and importing Control.ST.ImplicitCall, we can write programs which use multiple resources, and reduce the list of resources as necessary when calling functions which only use a subset of the overall resources.

Composite resources: Hierarchies of state machines

We’ve now seen how to use multiple resources in one function, which is necessary for any realistic program which manipulates state. We can think of this as “horizontal” composition: using multiple resources at once. We’ll often also need “vertical” composition: implementing one resource in terms of one or more other resources.

We’ll see an example of this in this section. First, we’ll implement a small API for graphics, in an interface Draw, supporting:

  • Opening a window, creating a double-buffered surface to draw on
  • Drawing lines and rectangles onto a surface
  • “Flipping” buffers, displaying the surface we’ve just drawn onto in the window
  • Closing a window

Then, we’ll use this API to implement a higher level API for turtle graphics, in an interface. This will require not only the Draw interface, but also a representation of the turtle state (location, direction and pen colour).

SDL bindings

For the examples in this section, you’ll need to install the (very basic!) SDL bindings for Idris, available from https://github.com/edwinb/SDL-idris. These bindings implement a small subset of the SDL API, and are for illustrative purposes only. Nevertheless, they are enough to implement small graphical programs and demonstrate the concepts of this section.

Once you’ve installed this package, you can start Idris with the -p sdl flag, for the SDL bindings, and the -p contrib flag, for the Control.ST library.

The Draw interface

We’re going to use the Idris SDL bindings for this API, so you’ll need to import Graphics.SDL once you’ve installed the bindings. We’ll start by defining the Draw interface, which includes a data type representing a surface on which we’ll draw lines and rectangles:

interface Draw (m : Type -> Type) where
    Surface : Type

We’ll need to be able to create a new Surface by opening a window:

initWindow : Int -> Int -> ST m Var [add Surface]

However, this isn’t quite right. It’s possible that opening a window will fail, for example if our program is running in a terminal without a windowing system available. So, somehow, initWindow needs to cope with the possibility of failure. We can do this by returning a Maybe Var, rather than a Var, and only adding the Surface on success:

initWindow : Int -> Int -> ST m (Maybe Var) [addIfJust Surface]

This uses a type level function addIfJust, defined in Control.ST which returns an Action that only adds a resource if the operation succeeds (that is, returns a result of the form Just val.

addIfJust and addIfRight

Control.ST defines functions for constructing new resources if an operation succeeds. As well as addIfJust, which adds a resource if an operation returns Just ty, there’s also addIfRight:

addIfJust : Type -> Action (Maybe Var)
addIfRight : Type -> Action (Either a Var)

Each of these is implemented in terms of the following primitive action Add, which takes a function to construct a resource list from the result of an operation:

Add : (ty -> Resources) -> Action ty

Using this, you can create your own actions to add resources based on the result of an operation, if required. For example, addIfJust is implemented as follows:

addIfJust : Type -> Action (Maybe Var)
addIfJust ty = Add (maybe [] (\var => [var ::: ty]))

If we create windows, we’ll also need to be able to delete them:

closeWindow : (win : Var) -> ST m () [remove win Surface]

We’ll also need to respond to events such as keypresses and mouse clicks. The Graphics.SDL library provides an Event type for this, and we can poll for events which returns the last event which occurred, if any:

poll : ST m (Maybe Event) []

The remaining methods of Draw are flip, which flips the buffers displaying everything that we’ve drawn since the previous flip, and two methods for drawing: filledRectangle and drawLine.

flip : (win : Var) -> ST m () [win ::: Surface]
filledRectangle : (win : Var) -> (Int, Int) -> (Int, Int) -> Col -> ST m () [win ::: Surface]
drawLine : (win : Var) -> (Int, Int) -> (Int, Int) -> Col -> ST m () [win ::: Surface]

We define colours as follows, as four components (red, green, blue, alpha):

data Col = MkCol Int Int Int Int

black : Col
black = MkCol 0 0 0 255

red : Col
red = MkCol 255 0 0 255

green : Col
green = MkCol 0 255 0 255

-- Also blue, yellow, magenta, cyan, white, similarly...

If you import Graphics.SDL, you can implement the Draw interface using the SDL bindings as follows:

implementation Draw IO where
  Surface = State SDLSurface

  initWindow x y = do Just srf <- lift (startSDL x y)
                           | pure Nothing
                      var <- new srf
                      pure (Just var)

  closeWindow win = do lift endSDL
                       delete win

  flip win = do srf <- read win
                lift (flipBuffers srf)
  poll = lift pollEvent

  filledRectangle win (x, y) (ex, ey) (MkCol r g b a)
       = do srf <- read win
            lift $ filledRect srf x y ex ey r g b a
  drawLine win (x, y) (ex, ey) (MkCol r g b a)
       = do srf <- read win
            lift $ drawLine srf x y ex ey r g b a

In this implementation, we’ve used startSDL to initialise a window, which, returns Nothing if it fails. Since the type of initWindow states that it adds a resource when it returns a value of the form Just val, we add the surface returned by startSDL on success, and nothing on failure. We can only successfully initialise if startDSL succeeds.

Now that we have an implementation of Draw, we can try writing some functions for drawing into a window and execute them via the SDL bindings. For example, assuming we have a surface win to draw onto, we can write a render function as follows which draws a line onto a black background:

render : Draw m => (win : Var) -> ST m () [win ::: Surface {m}]
render win = do filledRectangle win (0,0) (640,480) black
                drawLine win (100,100) (200,200) red
                flip win

The flip win at the end is necessary because the drawing primitives are double buffered, to prevent flicker. We draw onto one buffer, off-screen, and display the other. When we call flip, it displays the off-screen buffer, and creates a new off-screen buffer for drawing the next frame.

To include this in a program, we’ll write a main loop which renders our image and waits for an event to indicate the user wants to close the application:

loop : Draw m => (win : Var) -> ST m () [win ::: Surface {m}]
loop win = do render win
              Just AppQuit <- poll
                   | _ => loop win
              pure ()

Finally, we can create a main program which initialises a window, if possible, then runs the main loop:

drawMain : (ConsoleIO m, Draw m) => ST m () []
drawMain = do Just win <- initWindow 640 480
                 | Nothing => putStrLn "Can't open window"
              loop win
              closeWindow win

We can try this at the REPL using run:

*Draw> :exec run drawMain

A higher level interface: TurtleGraphics

Turtle graphics involves a “turtle” moving around the screen, drawing a line as it moves with a “pen”. A turtle has attributes describing its location, the direction it’s facing, and the current pen colour. There are commands for moving the turtle forwards, turning through an angle, and changing the pen colour, among other things. One possible interface would be the following:

interface TurtleGraphics (m : Type -> Type) where
  Turtle : Type

  start : Int -> Int -> ST m (Maybe Var) [addIfJust Turtle]
  end : (t : Var) -> ST m () [Remove t Turtle]

  fd : (t : Var) -> Int -> ST m () [t ::: Turtle]
  rt : (t : Var) -> Int -> ST m () [t ::: Turtle]

  penup : (t : Var) -> ST m () [t ::: Turtle]
  pendown : (t : Var) -> ST m () [t ::: Turtle]
  col : (t : Var) -> Col -> ST m () [t ::: Turtle]

  render : (t : Var) -> ST m () [t ::: Turtle]

Like Draw, we have a command for initialising the turtle (here called start) which might fail if it can’t create a surface for the turtle to draw on. There is also a render method, which is intended to render the picture drawn so far in a window. One possible program with this interface is the following, with draws a colourful square:

turtle : (ConsoleIO m, TurtleGraphics m) => ST m () []
turtle = with ST do
            Just t <- start 640 480
                 | Nothing => putStr "Can't make turtle\n"
            col t yellow
            fd t 100; rt t 90
            col t green
            fd t 100; rt t 90
            col t red
            fd t 100; rt t 90
            col t blue
            fd t 100; rt t 90
            render t
            end t

with ST do

The purpose of with ST do in turtle is to disambiguate (>>=), which could be either the version from the Monad interface, or the version from ST. Idris can work this out itself, but it takes time to try all of the possibilities, so the with clause can speed up type checking.

To implement the interface, we could try using Surface to represent the surface for the turtle to draw on:

implementation Draw m => TurtleGraphics m where
  Turtle = Surface {m}

Knowing that a Turtle is represented as a Surface, we can use the methods provided by Draw to implement the turtle. Unfortunately, though, this isn’t quite enough. We need to store more information: in particular, the turtle has several attributes which we need to store somewhere. So, not only do we need to represent the turtle as a Surface, we need to store some additional state. We can achieve this using a composite resource.

Introducing composite resources

A composite resource is built up from a list of other resources, and is implemented using the following type, defined by Control.ST:

data Composite : List Type -> Type

If we have a composite resource, we can split it into its constituent resources, and create new variables for each of those resources, using the split function. For example:

splitComp : (comp : Var) -> ST m () [comp ::: Composite [State Int, State String]]
splitComp comp = do [int, str] <- split comp
                    ?whatNow

The call split comp extracts the State Int and State String from the composite resource comp, and stores them in the variables int and str respectively. If we check the type of whatNow, we’ll see how this has affected the resource list:

  int : Var
  str : Var
  comp : Var
  m : Type -> Type
--------------------------------------
whatNow : STrans m () [int ::: State Int, str ::: State String, comp ::: State ()]
                      (\result => [comp ::: Composite [State Int, State String]])

So, we have two new resources int and str, and the type of comp has been updated to the unit type, so currently holds no data. This is to be expected: we’ve just extracted the data into individual resources after all.

Now that we’ve extracted the individual resources, we can manipulate them directly (say, incrementing the Int and adding a newline to the String) then rebuild the composite resource using combine:

splitComp : (comp : Var) ->
            ST m () [comp ::: Composite [State Int, State String]]
splitComp comp = do [int, str] <- split comp
                    update int (+ 1)
                    update str (++ "\n")
                    combine comp [int, str]
                    ?whatNow

As ever, we can check the type of whatNow to see the effect of combine:

  comp : Var
  int : Var
  str : Var
  m : Type -> Type
--------------------------------------
whatNow : STrans m () [comp ::: Composite [State Int, State String]]
                 (\result => [comp ::: Composite [State Int, State String]])

The effect of combine, therefore, is to take existing resources and merge them into one composite resource. Before we run combine, the target resource must exist (comp here) and must be of type State ().

It is instructive to look at the types of split and combine to see the requirements on resource lists they work with. The type of split is the following:

split : (lbl : Var) -> {auto prf : InState lbl (Composite vars) res} ->
        STrans m (VarList vars) res (\vs => mkRes vs ++ updateRes res prf (State ()))

The implicit prf argument says that the lbl being split must be a composite resource. It returns a variable list, built from the composite resource, and the mkRes function makes a list of resources of the appropriate types. Finally, updateRes updates the composite resource to have the type State ().

The combine function does the inverse:

combine : (comp : Var) -> (vs : List Var) ->
          {auto prf : InState comp (State ()) res} ->
          {auto var_prf : VarsIn (comp :: vs) res} ->
          STrans m () res (const (combineVarsIn res var_prf))

The implicit prf argument here ensures that the target resource comp has type State (). That is, we’re not overwriting any other data. The implicit var_prf argument is similar to SubRes in call, and ensures that every variable we’re using to build the composite resource really does exist in the current resource list.

We can use composite resources to implement our higher level TurtleGraphics API in terms of Draw, and any additional resources we need.

Implementing Turtle

Now that we’ve seen how to build a new resource from an existing collection, we can implement Turtle using a composite resource, containing the Surface to draw on, and individual states for the pen colour and the pen location and direction. We also have a list of lines, which describes what we’ll draw onto the Surface when we call render:

Turtle = Composite [Surface {m}, -- surface to draw on
                    State Col,  -- pen colour
                    State (Int, Int, Int, Bool), -- pen location/direction/d
                    State (List Line)] -- lines to draw on render

A Line is defined as a start location, and end location, and a colour:

Line : Type
Line = ((Int, Int), (Int, Int), Col)

To implement start, which creates a new Turtle (or returns Nothing if this is impossible), we begin by initialising the drawing surface then all of the components of the state. Finally, we combine all of these into a composite resource for the turtle:

start x y = do Just srf <- initWindow x y
                    | Nothing => pure Nothing
               col <- new white
               pos <- new (320, 200, 0, True)
               lines <- new []
               turtle <- new ()
               combine turtle [srf, col, pos, lines]
               pure (Just turtle)

To implement end, which needs to dispose of the turtle, we deconstruct the composite resource, close the window, then remove each individual resource. Remember that we can only delete a State, so we need to split the composite resource, close the drawing surface cleanly with closeWindow, then delete the states:

end t = do [srf, col, pos, lines] <- split t
           closeWindow srf; delete col; delete pos; delete lines; delete t

For the other methods, we need to split the resource to get each component, and combine into a composite resource when we’re done. As an example, here’s penup:

penup t = do [srf, col, pos, lines] <- split t -- Split the composite resource
             (x, y, d, _) <- read pos          -- Deconstruct the pen position
             write pos (x, y, d, False)        -- Set the pen down flag to False
             combine t [srf, col, pos, lines]  -- Recombine the components

The remaining operations on the turtle follow a similar pattern. See samples/ST/Graphics/Turtle.idr in the Idris distribution for the full details. It remains to render the image created by the turtle:

render t = do [srf, col, pos, lines] <- split t -- Split the composite resource
              filledRectangle srf (0, 0) (640, 480) black -- Draw a background
              drawAll srf !(read lines)         -- Render the lines drawn by the turtle
              flip srf                          -- Flip the buffers to display the image
              combine t [srf, col, pos, lines]
              Just ev <- poll
                | Nothing => render t           -- Keep going until a key is pressed
              case ev of
                   KeyUp _ => pure ()           -- Key pressed, so quit
                   _ => render t
 where drawAll : (srf : Var) -> List Line -> ST m () [srf ::: Surface {m}]
       drawAll srf [] = pure ()
       drawAll srf ((start, end, col) :: xs)
          = do drawLine srf start end col       -- Draw a line in the appropriate colour
               drawAll srf xs