3************************
4Composing State Machines
5************************
7In the previous section, we defined a ``DataStore`` interface and used it
8to implement the following small program which allows a user to log in to
9the store then display the store's contents;
13 getData : (ConsoleIO m, DataStore m) => ST m () []
14 getData = do st <- connect
16 | BadPassword => do putStrLn "Failure"
18 secret <- readSecret st
19 putStrLn ("Secret is: " ++ show secret)
23This function only uses one state, the store itself. Usually, though,
24larger programs have lots of states, and might add, delete and update
25states over the course of its execution. Here, for example, a useful
26extension might be to loop forever, keeping count of the number of times
27there was a login failure in a state.
29Furthermore, we may have *hierarchies* of state machines, in that one
30state machine could be implemented by composing several others. For
31example, we can have a state machine representing the state of a
32graphics system, and use this to implement a *higher level* graphics API
33such as turtle graphics, which uses the graphics system plus some additional
36In this section, we'll see how to work with multiple states, and how to
37compose state machines to make higher level state machines. We'll begin by
38seeing how to add a login failure counter to ``getData``.
40Working with multiple resources
41===============================
43To see how to work with multiple resources, we'll modify ``getData`` so
44that it loops, and counts the total number of times the user fails to
45log in. For example, if we write a ``main`` program which initialises the
46count to zero, a session might run as follows:
50 *LoginCount> :exec main
51 Enter password: Mornington Crescent
52 Secret is: "Secret Data"
53 Enter password: Dollis Hill
56 Enter password: Mornington Crescent
57 Secret is: "Secret Data"
58 Enter password: Codfanglers
63We'll start by adding a state resource to ``getData`` to keep track of the
68 getData : (ConsoleIO m, DataStore m) =>
69 (failcount : Var) -> ST m () [failcount ::: State Integer]
71.. topic:: Type checking ``getData``
73 If you're following along in the code, you'll find that ``getData``
74 no longer compiles when you update this type. That is to be expected!
75 For the moment, comment out the definition of ``getData``. We'll come back
78Then, we can create a ``main`` program which initialises the state to ``0``
79and invokes ``getData``, as follows:
84 main = run (do fc <- new 0
88We'll start our implementation of ``getData`` just by adding the new
89argument for the failure count:
93 getData : (ConsoleIO m, DataStore m) =>
94 (failcount : Var) -> ST m () [failcount ::: State Integer]
98 | BadPassword => do putStrLn "Failure"
100 secret <- readSecret st
101 putStrLn ("Secret is: " ++ show secret)
105Unfortunately, this doesn't type check, because we have the wrong resources
106for calling ``connect``. The error messages shows how the resources don't
111 When checking an application of function Control.ST.>>=:
112 Error in state transition:
113 Operation has preconditions: []
114 States here are: [failcount ::: State Integer]
115 Operation has postconditions: \result => [result ::: Store LoggedOut] ++ []
116 Required result states here are: st2_fn
118In other words, ``connect`` requires that there are *no* resources on
119entry, but we have *one*, the failure count!
120This shouldn't be a problem, though: the required resources are a *subset* of
121the resources we have, after all, and the additional resources (here, the
122failure count) are not relevant to ``connect``. What we need, therefore,
123is a way to temporarily *hide* the additional resource.
125We can achieve this with the ``call`` function:
129 getData : (ConsoleIO m, DataStore m) =>
130 (failcount : Var) -> ST m () [failcount ::: State Integer]
132 = do st <- call connect
135Here we've left a hole for the rest of ``getData`` so that you can see the
136effect of ``call``. It has removed the unnecessary parts of the resource
137list for calling ``connect``, then reinstated them on return. The type of
138``whatNow`` therefore shows that we've added a new resource ``st``, and still
139have ``failcount`` available:
145 constraint : ConsoleIO m
146 constraint1 : DataStore m
148 --------------------------------------
149 whatNow : STrans m () [failcount ::: State Integer, st ::: Store LoggedOut]
150 (\result => [failcount ::: State Integer])
152By the end of the function, ``whatNow`` says that we need to have finished with
153``st``, but still have ``failcount`` available. We can complete ``getData``
154so that it works with an additional state resource by adding ``call`` whenever
155we invoke one of the operations on the data store, to reduce the list of
160 getData : (ConsoleIO m, DataStore m) =>
161 (failcount : Var) -> ST m () [failcount ::: State Integer]
163 = do st <- call connect
164 OK <- call $ login st
165 | BadPassword => do putStrLn "Failure"
167 secret <- call $ readSecret st
168 putStrLn ("Secret is: " ++ show secret)
172This is a little noisy, and in fact we can remove the need for it by
173making ``call`` implicit. By default, you need to add the ``call`` explicitly,
174but if you import ``Control.ST.ImplicitCall``, Idris will insert ``call``
175where it is necessary.
179 import Control.ST.ImplicitCall
181It's now possible to write ``getData`` exactly as before:
185 getData : (ConsoleIO m, DataStore m) =>
186 (failcount : Var) -> ST m () [failcount ::: State Integer]
190 | BadPassword => do putStrLn "Failure"
192 secret <- readSecret st
193 putStrLn ("Secret is: " ++ show secret)
197There is a trade off here: if you import ``Control.ST.ImplicitCall`` then
198functions which use multiple resources are much easier to read, because the
199noise of ``call`` has gone. On the other hand, Idris has to work a little
200harder to type check your functions, and as a result it can take slightly
201longer, and the error messages can be less helpful.
203It is instructive to see the type of ``call``:
207 call : STrans m t sub new_f -> {auto res_prf : SubRes sub old} ->
208 STrans m t old (\res => updateWith (new_f res) old res_prf)
210The function being called has a list of resources ``sub``, and
211there is an implicit proof, ``SubRes sub old`` that the resource list in
212the function being called is a subset of the overall resource list. The
213ordering of resources is allowed to change, although resources which
214appear in ``old`` can't appear in the ``sub`` list more than once (you will
215get a type error if you try this).
217The function ``updateWith`` takes the *output* resources of the
218called function, and updates them in the current resource list. It makes
219an effort to preserve ordering as far as possible, although this isn't
220always possible if the called function does some complicated resource
223.. topic:: Newly created resources in called functions
225 If the called function creates any new resources, these will typically
226 appear at the *end* of the resource list, due to the way ``updateWith``
227 works. You can see this in the type of ``whatNow`` in our incomplete
228 definition of ``getData`` above.
230Finally, we can update ``getData`` so that it loops, and keeps
231``failCount`` updated as necessary:
235 getData : (ConsoleIO m, DataStore m) =>
236 (failcount : Var) -> ST m () [failcount ::: State Integer]
238 = do st <- call connect
240 | BadPassword => do putStrLn "Failure"
242 write failcount (fc + 1)
243 putStrLn ("Number of failures: " ++ show (fc + 1))
246 secret <- readSecret st
247 putStrLn ("Secret is: " ++ show secret)
252Note that here, we're connecting and disconnecting on every iteration.
253Another way to implement this would be to ``connect`` first, then call
254``getData``, and implement ``getData`` as follows:
258 getData : (ConsoleIO m, DataStore m) =>
259 (st, failcount : Var) -> ST m () [st ::: Store {m} LoggedOut, failcount ::: State Integer]
262 | BadPassword => do putStrLn "Failure"
264 write failcount (fc + 1)
265 putStrLn ("Number of failures: " ++ show (fc + 1))
267 secret <- readSecret st
268 putStrLn ("Secret is: " ++ show secret)
272It is important to add the explicit ``{m}`` in the type of ``Store {m}
273LoggedOut`` for ``st``, because this gives Idris enough information to know
274which implementation of ``DataStore`` to use to find the appropriate
275implementation for ``Store``. Otherwise, if we only write ``Store LoggedOut``,
276there's no way to know that the ``Store`` is linked with the computation
279We can then ``connect`` and ``disconnect`` only once, in ``main``:
284 main = run (do fc <- new 0
290By using ``call``, and importing ``Control.ST.ImplicitCall``, we can
291write programs which use multiple resources, and reduce the list of
292resources as necessary when calling functions which only use a subset of
293the overall resources.
295Composite resources: Hierarchies of state machines
296==================================================
298We've now seen how to use multiple resources in one function, which is
299necessary for any realistic program which manipulates state. We can think
300of this as "horizontal" composition: using multiple resources at once.
301We'll often also need "vertical" composition: implementing one resource
302in terms of one or more other resources.
304We'll see an example of this in this section. First, we'll implement a
305small API for graphics, in an interface ``Draw``, supporting:
307* Opening a window, creating a double-buffered surface to draw on
308* Drawing lines and rectangles onto a surface
309* "Flipping" buffers, displaying the surface we've just drawn onto in
313Then, we'll use this API to implement a higher level API for turtle graphics,
315This will require not only the ``Draw`` interface, but also a representation
316of the turtle state (location, direction and pen colour).
318.. topic:: SDL bindings
320 For the examples in this section, you'll need to install the
321 (very basic!) SDL bindings for Idris, available from
322 https://github.com/edwinb/SDL-idris. These bindings implement a small
323 subset of the SDL API, and are for illustrative purposes only.
324 Nevertheless, they are enough to implement small graphical programs
325 and demonstrate the concepts of this section.
327 Once you've installed this package, you can start Idris with the
328 ``-p sdl`` flag, for the SDL bindings, and the ``-p contrib`` flag,
329 for the ``Control.ST`` library.
331The ``Draw`` interface
332----------------------
334We're going to use the Idris SDL bindings for this API, so you'll need
335to import ``Graphics.SDL`` once you've installed the bindings.
336We'll start by defining the ``Draw`` interface, which includes a data type
337representing a surface on which we'll draw lines and rectangles:
341 interface Draw (m : Type -> Type) where
344We'll need to be able to create a new ``Surface`` by opening a window:
348 initWindow : Int -> Int -> ST m Var [add Surface]
350However, this isn't quite right. It's possible that opening a window
351will fail, for example if our program is running in a terminal without
352a windowing system available. So, somehow, ``initWindow`` needs to cope
353with the possibility of failure. We can do this by returning a
354``Maybe Var``, rather than a ``Var``, and only adding the ``Surface``
359 initWindow : Int -> Int -> ST m (Maybe Var) [addIfJust Surface]
361This uses a type level function ``addIfJust``, defined in ``Control.ST``
362which returns an ``Action`` that only adds a resource if the operation
363succeeds (that is, returns a result of the form ``Just val``.
365.. topic:: ``addIfJust`` and ``addIfRight``
367 ``Control.ST`` defines functions for constructing new resources if an
368 operation succeeds. As well as ``addIfJust``, which adds a resource if
369 an operation returns ``Just ty``, there's also ``addIfRight``:
371 .. code-block:: idris
373 addIfJust : Type -> Action (Maybe Var)
374 addIfRight : Type -> Action (Either a Var)
376 Each of these is implemented in terms of the following primitive action
377 ``Add``, which takes a function to construct a resource list from the result
380 .. code-block:: idris
382 Add : (ty -> Resources) -> Action ty
384 Using this, you can create your own actions to add resources
385 based on the result of an operation, if required. For example,
386 ``addIfJust`` is implemented as follows:
388 .. code-block:: idris
390 addIfJust : Type -> Action (Maybe Var)
391 addIfJust ty = Add (maybe [] (\var => [var ::: ty]))
393If we create windows, we'll also need to be able to delete them:
397 closeWindow : (win : Var) -> ST m () [remove win Surface]
399We'll also need to respond to events such as keypresses and mouse clicks.
400The ``Graphics.SDL`` library provides an ``Event`` type for this, and
401we can ``poll`` for events which returns the last event which occurred,
406 poll : ST m (Maybe Event) []
408The remaining methods of ``Draw`` are ``flip``, which flips the buffers
409displaying everything that we've drawn since the previous ``flip``, and
410two methods for drawing: ``filledRectangle`` and ``drawLine``.
414 flip : (win : Var) -> ST m () [win ::: Surface]
415 filledRectangle : (win : Var) -> (Int, Int) -> (Int, Int) -> Col -> ST m () [win ::: Surface]
416 drawLine : (win : Var) -> (Int, Int) -> (Int, Int) -> Col -> ST m () [win ::: Surface]
418We define colours as follows, as four components (red, green, blue, alpha):
422 data Col = MkCol Int Int Int Int
425 black = MkCol 0 0 0 255
428 red = MkCol 255 0 0 255
431 green = MkCol 0 255 0 255
433 -- Also blue, yellow, magenta, cyan, white, similarly...
435If you import ``Graphics.SDL``, you can implement the ``Draw`` interface
436using the SDL bindings as follows:
440 implementation Draw IO where
441 Surface = State SDLSurface
443 initWindow x y = do Just srf <- lift (startSDL x y)
448 closeWindow win = do lift endSDL
451 flip win = do srf <- read win
452 lift (flipBuffers srf)
453 poll = lift pollEvent
455 filledRectangle win (x, y) (ex, ey) (MkCol r g b a)
457 lift $ filledRect srf x y ex ey r g b a
458 drawLine win (x, y) (ex, ey) (MkCol r g b a)
460 lift $ drawLine srf x y ex ey r g b a
462In this implementation, we've used ``startSDL`` to initialise a window, which,
463returns ``Nothing`` if it fails. Since the type of ``initWindow`` states that
464it adds a resource when it returns a value of the form ``Just val``, we
465add the surface returned by ``startSDL`` on success, and nothing on
466failure. We can only successfully initialise if ``startDSL`` succeeds.
468Now that we have an implementation of ``Draw``, we can try writing some
469functions for drawing into a window and execute them via the SDL bindings.
470For example, assuming we have a surface ``win`` to draw onto, we can write a
471``render`` function as follows which draws a line onto a black background:
475 render : Draw m => (win : Var) -> ST m () [win ::: Surface {m}]
476 render win = do filledRectangle win (0,0) (640,480) black
477 drawLine win (100,100) (200,200) red
480The ``flip win`` at the end is necessary because the drawing primitives
481are double buffered, to prevent flicker. We draw onto one buffer, off-screen,
482and display the other. When we call ``flip``, it displays the off-screen
483buffer, and creates a new off-screen buffer for drawing the next frame.
485To include this in a program, we'll write a main loop which renders our
486image and waits for an event to indicate the user wants to close the
491 loop : Draw m => (win : Var) -> ST m () [win ::: Surface {m}]
492 loop win = do render win
497Finally, we can create a main program which initialises a window, if
498possible, then runs the main loop:
502 drawMain : (ConsoleIO m, Draw m) => ST m () []
503 drawMain = do Just win <- initWindow 640 480
504 | Nothing => putStrLn "Can't open window"
508We can try this at the REPL using ``run``:
512 *Draw> :exec run drawMain
514A higher level interface: ``TurtleGraphics``
515--------------------------------------------
517Turtle graphics involves a "turtle" moving around the screen, drawing a line as
518it moves with a "pen". A turtle has attributes describing its location, the
519direction it's facing, and the current pen colour. There are commands for
520moving the turtle forwards, turning through an angle, and changing the
521pen colour, among other things. One possible interface would be the
526 interface TurtleGraphics (m : Type -> Type) where
529 start : Int -> Int -> ST m (Maybe Var) [addIfJust Turtle]
530 end : (t : Var) -> ST m () [Remove t Turtle]
532 fd : (t : Var) -> Int -> ST m () [t ::: Turtle]
533 rt : (t : Var) -> Int -> ST m () [t ::: Turtle]
535 penup : (t : Var) -> ST m () [t ::: Turtle]
536 pendown : (t : Var) -> ST m () [t ::: Turtle]
537 col : (t : Var) -> Col -> ST m () [t ::: Turtle]
539 render : (t : Var) -> ST m () [t ::: Turtle]
541Like ``Draw``, we have a command for initialising the turtle (here called
542``start``) which might fail if it can't create a surface for the turtle to
543draw on. There is also a ``render`` method, which is intended to render the
544picture drawn so far in a window. One possible program with this interface
545is the following, with draws a colourful square:
549 turtle : (ConsoleIO m, TurtleGraphics m) => ST m () []
551 Just t <- start 640 480
552 | Nothing => putStr "Can't make turtle\n"
564.. topic:: ``with ST do``
566 The purpose of ``with ST do`` in ``turtle`` is to disambiguate ``(>>=)``,
567 which could be either the version from the ``Monad`` interface, or the
568 version from ``ST``. Idris can work this out itself, but it takes time to
569 try all of the possibilities, so the ``with`` clause can
570 speed up type checking.
572To implement the interface, we could try using ``Surface`` to represent
573the surface for the turtle to draw on:
577 implementation Draw m => TurtleGraphics m where
580Knowing that a ``Turtle`` is represented as a ``Surface``, we can use the
581methods provided by ``Draw`` to implement the turtle. Unfortunately, though,
582this isn't quite enough. We need to store more information: in particular, the
583turtle has several attributes which we need to store somewhere.
584So, not only do we need to represent the turtle as a ``Surface``, we need
585to store some additional state. We can achieve this using a *composite*
588Introducing composite resources
589-------------------------------
591A *composite* resource is built up from a list of other resources, and
592is implemented using the following type, defined by ``Control.ST``:
596 data Composite : List Type -> Type
598If we have a composite resource, we can split it into its constituent
599resources, and create new variables for each of those resources, using
600the *split* function. For example:
604 splitComp : (comp : Var) -> ST m () [comp ::: Composite [State Int, State String]]
605 splitComp comp = do [int, str] <- split comp
608The call ``split comp`` extracts the ``State Int`` and ``State String`` from
609the composite resource ``comp``, and stores them in the variables ``int``
610and ``str`` respectively. If we check the type of ``whatNow``, we'll see
611how this has affected the resource list:
619 --------------------------------------
620 whatNow : STrans m () [int ::: State Int, str ::: State String, comp ::: State ()]
621 (\result => [comp ::: Composite [State Int, State String]])
623So, we have two new resources ``int`` and ``str``, and the type of
624``comp`` has been updated to the unit type, so currently holds no data.
625This is to be expected: we've just extracted the data into individual
628Now that we've extracted the individual resources, we can manipulate them
629directly (say, incrementing the ``Int`` and adding a newline to the
630``String``) then rebuild the composite resource using ``combine``:
634 splitComp : (comp : Var) ->
635 ST m () [comp ::: Composite [State Int, State String]]
636 splitComp comp = do [int, str] <- split comp
639 combine comp [int, str]
642As ever, we can check the type of ``whatNow`` to see the effect of
651 --------------------------------------
652 whatNow : STrans m () [comp ::: Composite [State Int, State String]]
653 (\result => [comp ::: Composite [State Int, State String]])
655The effect of ``combine``, therefore, is to take existing
656resources and merge them into one composite resource. Before we run
657``combine``, the target resource must exist (``comp`` here) and must be
660It is instructive to look at the types of ``split`` and ``combine`` to see
661the requirements on resource lists they work with. The type of ``split``
666 split : (lbl : Var) -> {auto prf : InState lbl (Composite vars) res} ->
667 STrans m (VarList vars) res (\vs => mkRes vs ++ updateRes res prf (State ()))
669The implicit ``prf`` argument says that the ``lbl`` being split must be
670a composite resource. It returns a variable list, built from the composite
671resource, and the ``mkRes`` function makes a list of resources of the
672appropriate types. Finally, ``updateRes`` updates the composite resource to
673have the type ``State ()``.
675The ``combine`` function does the inverse:
679 combine : (comp : Var) -> (vs : List Var) ->
680 {auto prf : InState comp (State ()) res} ->
681 {auto var_prf : VarsIn (comp :: vs) res} ->
682 STrans m () res (const (combineVarsIn res var_prf))
684The implicit ``prf`` argument here ensures that the target resource ``comp``
685has type ``State ()``. That is, we're not overwriting any other data.
686The implicit ``var_prf`` argument is similar to ``SubRes`` in ``call``, and
687ensures that every variable we're using to build the composite resource
688really does exist in the current resource list.
690We can use composite resources to implement our higher level ``TurtleGraphics``
691API in terms of ``Draw``, and any additional resources we need.
693Implementing ``Turtle``
694-----------------------
696Now that we've seen how to build a new resource from an existing collection,
697we can implement ``Turtle`` using a composite resource, containing the
698``Surface`` to draw on, and individual states for the pen colour and the
699pen location and direction. We also have a list of lines, which describes
700what we'll draw onto the ``Surface`` when we call ``render``:
704 Turtle = Composite [Surface {m}, -- surface to draw on
705 State Col, -- pen colour
706 State (Int, Int, Int, Bool), -- pen location/direction/d
707 State (List Line)] -- lines to draw on render
709A ``Line`` is defined as a start location, and end location, and a colour:
714 Line = ((Int, Int), (Int, Int), Col)
716To implement ``start``, which creates a new ``Turtle`` (or returns ``Nothing``
717if this is impossible), we begin by initialising the drawing surface then
718all of the components of the state. Finally, we combine all of these
719into a composite resource for the turtle:
723 start x y = do Just srf <- initWindow x y
724 | Nothing => pure Nothing
726 pos <- new (320, 200, 0, True)
729 combine turtle [srf, col, pos, lines]
732To implement ``end``, which needs to dispose of the turtle,
733we deconstruct the composite resource, close the window,
734then remove each individual resource. Remember that we can only ``delete``
735a ``State``, so we need to ``split`` the composite resource, close the
736drawing surface cleanly with ``closeWindow``, then ``delete`` the states:
740 end t = do [srf, col, pos, lines] <- split t
741 closeWindow srf; delete col; delete pos; delete lines; delete t
743For the other methods, we need to ``split`` the resource to get each
744component, and ``combine`` into a composite resource when we're done.
745As an example, here's ``penup``:
749 penup t = do [srf, col, pos, lines] <- split t -- Split the composite resource
750 (x, y, d, _) <- read pos -- Deconstruct the pen position
751 write pos (x, y, d, False) -- Set the pen down flag to False
752 combine t [srf, col, pos, lines] -- Recombine the components
754The remaining operations on the turtle follow a similar pattern. See
755``samples/ST/Graphics/Turtle.idr`` in the Idris distribution for the full
756details. It remains to render the image created by the turtle:
760 render t = do [srf, col, pos, lines] <- split t -- Split the composite resource
761 filledRectangle srf (0, 0) (640, 480) black -- Draw a background
762 drawAll srf !(read lines) -- Render the lines drawn by the turtle
763 flip srf -- Flip the buffers to display the image
764 combine t [srf, col, pos, lines]
766 | Nothing => render t -- Keep going until a key is pressed
768 KeyUp _ => pure () -- Key pressed, so quit
770 where drawAll : (srf : Var) -> List Line -> ST m () [srf ::: Surface {m}]
771 drawAll srf [] = pure ()
772 drawAll srf ((start, end, col) :: xs)
773 = do drawLine srf start end col -- Draw a line in the appropriate colour
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list