@@ -295,6 +295,480 @@ the overall resources.
295Composite resources: Hierarchies of state machines
295Composite resources: Hierarchies of state machines
296==================================================
296==================================================
298−Composite resources: Graphics
298+We've now seen how to use multiple resources in one function, which is
299+necessary for any realistic program which manipulates state. We can think
300+of this as "horizontal" composition: using multiple resources at once.
301+We'll often also need "vertical" composition: implementing one resource
302+in terms of one or more other resources.
304+We'll see an example of this in this section. First, we'll implement a
305+small 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
313+Then, we'll use this API to implement a higher level API for turtle graphics,
315+This will require not only the ``Draw`` interface, but also a representation
316+of 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.
331+The ``Draw`` interface
332+----------------------
334+We're going to use the Idris SDL bindings for this API, so you'll need
335+to import ``Graphics.SDL`` once you've installed the bindings.
336+We'll start by defining the ``Draw`` interface, which includes a data type
337+representing a surface on which we'll draw lines and rectangles:
339+.. code-block:: idris
341+ interface Draw (m : Type -> Type) where
344+We'll need to be able to create a new ``Surface`` by opening a window:
346+.. code-block:: idris
348+ initWindow : Int -> Int -> ST m Var [add Surface]
350+However, this isn't quite right. It's possible that opening a window
351+will fail, for example if our program is running in a termina without
352+a windowing system available. So, somehow, ``initWindow`` needs to cope
353+with the possibility of failure. We can do this by returning a
354+``Maybe Var``, rather than a ``Var``, and only adding the ``Surface``
357+.. code-block:: idris
359+ initWindow : Int -> Int -> ST m (Maybe Var) [addIfJust Surface]
361+This uses a type level function ``addIfJust``, defined in ``Control.ST``
362+which returns an ``Action`` that only adds a resource if the operation
363+succeeds (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]))
393+If we create windows, we'll also need to be able to delete them:
395+.. code-block:: idris
397+ closeWindow : (win : Var) -> ST m () [remove win Surface]
399+We'll also need to respond to events such as keypresses and mouse clicks.
400+The ``Graphics.SDL`` library provides an ``Event`` type for this, and
401+we can ``poll`` for events which returns the last event which occurred,
404+.. code-block:: idris
406+ poll : ST m (Maybe Event) []
408+The remaining methods of ``Draw`` are ``flip``, which flips the buffers
409+displaying everything that we've drawn since the previous ``flip``, and
410+two methods for drawing: ``filledRectangle`` and ``drawLine``.
412+.. code-block:: idris
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]
418+We define colours as follows, as four components (red, green, blue, alpha):
420+.. code-block:: idris
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...
435+If you import ``Graphics.SDL``, you can implement the ``Draw`` interface
436+using the SDL bindings as follows:
438+.. code-block:: idris
440+ interface 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)
456+ = do srf <- read win
457+ lift $ filledRect srf x y ex ey r g b a
458+ drawLine win (x, y) (ex, ey) (MkCol r g b a)
459+ = do srf <- read win
460+ lift $ drawLine srf x y ex ey r g b a
462+In this implementation, we've used ``startSDL`` to initialise a window, which,
463+returns ``Nothing`` if it fails. Since the type of ``initWindow`` states that
464+it adds a resource when it returns a value of the form ``Just val``, we
465+add the surface returned by ``startSDL`` on success, and nothing on
466+failure. We can only successfully initialise if ``startDSL`` succeeds.
468+Now that we have an implementation of ``Draw``, we can try writing some
469+functions for drawing into a window and execute them via the SDL bindings.
470+For 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:
473+.. code-block:: idris
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
480+The ``flip win`` at the end is necessary because the drawing primitives
481+are double buffered, to prevent flicker. We draw onto one buffer, off-screen,
482+and display the other. When we call ``flip``, it displays the off-screen
483+buffer, and creates a new off-screen buffer for drawing the next frame.
485+To include this in a program, we'll write a main loop which renders our
486+image and waits for an event to indicate the user wants to close the
489+.. code-block:: idris
491+ loop : Draw m => (win : Var) -> ST m () [win ::: Surface {m}]
492+ loop win = do render win
493+ Just AppQuit <- poll
497+Finally, we can create a main program which initialises a window, if
498+possible, then runs the main loop:
500+.. code-block:: idris
502+ drawMain : (ConsoleIO m, Draw m) => ST m () []
503+ drawMain = do Just win <- initWindow 640 480
504+ | Nothing => putStrLn "Can't open window"
508+We can try this at the REPL using ``run``:
512+ *Draw> :exec run drawMain
514+A higher level interface: ``TurtleGraphics``
515+--------------------------------------------
517+Turtle graphics involves a "turtle" moving around the screen, drawing a line as
518+it moves with a "pen". A turtle has attributes describing its location, the
519+direction it's facing, and the current pen colour. There are commands for
520+moving the turtle forwards, turning through an angle, and changing the
521+pen colour, among other things. One possible interface would be the
524+.. code-block:: idris
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]
541+Like ``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
543+draw on. There is also a ``render`` method, which is intended to render the
544+picture drawn so far in a window. One possible program with this interface
545+is the following, with draws a colourful square:
547+.. code-block:: idris
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.
572+To implement the interface, we could try using ``Surface`` to represent
573+the surface for the turtle to draw on:
575+.. code-block:: idris
577+ implementation Draw m => TurtleGraphics m where
578+ Turtle = Surface {m}
580+Knowing that a ``Turtle`` is represented as a ``Surface``, we can use the
581+methods provided by ``Draw`` to implement the turtle. Unfortunately, though,
582+this isn't quite enough. We need to store more information: in particular, the
583+turtle has several attributes which we need to store somewhere.
584+So, not only do we need to represent the turtle as a ``Surface``, we need
585+to store some additional state. We can achieve this using a *composite*
588+Introducing composite resources
589+-------------------------------
591+A *composite* resource is built up from a list of other resources, and
592+is implemented using the following type, defined by ``Control.ST``:
594+.. code-block:: idris
596+ data Composite : List Type -> Type
598+If we have a composite resource, we can split it into its constituent
599+resources, and create new variables for each of those resources, using
600+the *split* function. For example:
602+.. code-block:: idris
604+ splitComp : (comp : Var) -> ST m () [comp ::: Composite [State Int, State String]]
605+ splitComp comp = do [int, str] <- split comp
608+The call ``split comp`` extracts the ``State Int`` and ``State String`` from
609+the composite resource ``comp``, and stores them in the variables ``int``
610+and ``str`` respectively. If we check the type of ``whatNow``, we'll see
611+how this has affected the resource list:
613+.. code-block:: idris
619+ --------------------------------------
620+ whatNow : STrans m () [int ::: State Int, str ::: State String, comp ::: State ()]
621+ (\result => [comp ::: Composite [State Int, State String]])
623+So, 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.
625+This is to be expected: we've just extracted the data into individual
628+Now that we've extracted the individual resources, we can manipulate them
629+directly (say, incrementing the ``Int`` and adding a newline to the
630+``String``) then rebuild the composite resource using ``combine``:
632+.. code-block:: idris
634+ splitComp : (comp : Var) ->
635+ ST m () [comp ::: Composite [State Int, State String]]
636+ splitComp comp = do [int, str] <- split comp
638+ update str (++ "\n")
639+ combine comp [int, str]
642+As ever, we can check the type of ``whatNow`` to see the effect of
645+.. code-block:: idris
651+ --------------------------------------
652+ whatNow : STrans m () [comp ::: Composite [State Int, State String]]
653+ (\result => [comp ::: Composite [State Int, State String]])
655+The effect of ``combine``, therefore, is to take existing
656+resources and merge them into one composite resource. Before we run
657+``combine``, the target resource must exist (``comp`` here) and must be
658+of type ``State ()``.
660+It is instructive to look at the types of ``split`` and combine to see
661+the requirements on resource lists they work with. The type of ``split``
664+.. code-block:: idris
666+ split : (lbl : Var) -> {auto prf : InState lbl (Composite vars) res} ->
667+ STrans m (VarList vars) res (\ vs => mkRes vs ++ updateRes res prf (State ()))
669+The implicit ``prf`` argument says that the ``lbl`` being split must be
670+a composite resource. It returns a variable list, built from the composite
671+resource, and the ``mkRes`` function makes a list of resources of the
672+appropriate types. Finally, ``updateRes`` updates the composite resource to
673+have the type ``State ()``.
675+The ``combine`` function does the inverse:
677+.. code-block:: idris
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))
684+The implicit ``prf`` argument here ensures that the target resource ``comp``
685+has type ``State ()``. That is, we're not overwriting any other data.
686+The implicit ``var_prf`` argument is similar to ``SubRes`` in ``call``, and
687+ensures that every variable we're using to build the composite resource
688+really does exist in the current resource list.
690+We can use composite resources to implement our higher level ``TurtleGraphics``
691+API in terms of ``Draw``, and any additional resources we need.
693+Implementing ``Turtle``
694+-----------------------
696+Now that we've seen how to build a new resource from an existing collection,
697+we can implement ``Turtle`` using a composite resource, containing the
698+``Surface`` to draw on, and individual states for the pen colour and the
699+pen location and direction. We also have a list of lines, which describes
700+what we'll draw onto the ``Surface`` when we call ``render``:
702+.. code-block:: idris
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
709+A ``Line`` is defined as a start location, and end location, and a colour:
711+.. code-block:: idris
714+ Line = ((Int, Int), (Int, Int), Col)
716+To implement ``start``, which creates a new ``Turtle`` (or returns ``Nothing``)
717+if this is impossible, we begin by initialising the drawing surface then
718+all of the components of the state. Finally, we combine all of these
719+into a composite resource for the turtle:
721+.. code-block:: idris
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]
732+To implement ``end``, which needs to dispose of the turtle,
733+we deconstruct the composite resource, close the window,
734+then remove each individual resource. Remember that we can only ``delete``
735+a ``State``, so we need to ``split`` the composite resource, close the
736+drawing surface cleanly with ``closeWindow``, then ``delete`` the states:
738+.. code-block:: idris
740+ end t = do [srf, col, pos, lines] <- split t
741+ closeWindow srf; delete col; delete pos; delete lines; delete t
743+For the other methods, we need to ``split`` the resource to get each
744+component, and ``combine`` into a composite resource when we're done.
745+As an example, here's ``penup``:
747+.. code-block:: idris
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
754+The remaining operations on the turtle follow a similar pattern. See
755+``samples/ST/Graphics/Turtle.idr`` in the Idris distribution for the full
756+details. It remains to render the image created by the turtle:
758+.. code-block:: idris
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