@@ -295,6 +295,480 @@ the overall resources.
295295Composite resources: Hierarchies of state machines
296296==================================================
297297
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.
303+
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:
306+
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
310+ the window
311+* Closing a window
312+
313+Then, we'll use this API to implement a higher level API for turtle graphics,
314+in an ``interface``.
315+This will require not only the ``Draw`` interface, but also a representation
316+of the turtle state (location, direction and pen colour).
317+
318+.. topic:: SDL bindings
319+
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.
326+
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.
330+
331+The ``Draw`` interface
332+----------------------
333+
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:
299338
339+.. code-block:: idris
340+
341+ interface Draw (m : Type -> Type) where
342+ Surface : Type
343+
344+We'll need to be able to create a new ``Surface`` by opening a window:
345+
346+.. code-block:: idris
347+
348+ initWindow : Int -> Int -> ST m Var [add Surface]
349+
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``
355+on success:
356+
357+.. code-block:: idris
358+
359+ initWindow : Int -> Int -> ST m (Maybe Var) [addIfJust Surface]
360+
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``.
364+
365+.. topic:: ``addIfJust`` and ``addIfRight``
366+
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``:
370+
371+ .. code-block:: idris
372+
373+ addIfJust : Type -> Action (Maybe Var)
374+ addIfRight : Type -> Action (Either a Var)
375+
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
378+ of an operation:
379+
380+ .. code-block:: idris
381+
382+ Add : (ty -> Resources) -> Action ty
383+
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:
387+
388+ .. code-block:: idris
389+
390+ addIfJust : Type -> Action (Maybe Var)
391+ addIfJust ty = Add (maybe [] (\var => [var ::: ty]))
392+
393+If we create windows, we'll also need to be able to delete them:
394+
395+.. code-block:: idris
396+
397+ closeWindow : (win : Var) -> ST m () [remove win Surface]
398+
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,
402+if any:
403+
404+.. code-block:: idris
405+
406+ poll : ST m (Maybe Event) []
407+
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``.
411+
412+.. code-block:: idris
413+
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]
417+
418+We define colours as follows, as four components (red, green, blue, alpha):
419+
420+.. code-block:: idris
421+
422+ data Col = MkCol Int Int Int Int
423+
424+ black : Col
425+ black = MkCol 0 0 0 255
426+
427+ red : Col
428+ red = MkCol 255 0 0 255
429+
430+ green : Col
431+ green = MkCol 0 255 0 255
432+
433+ -- Also blue, yellow, magenta, cyan, white, similarly...
434+
435+If you import ``Graphics.SDL``, you can implement the ``Draw`` interface
436+using the SDL bindings as follows:
437+
438+.. code-block:: idris
439+
440+ interface Draw IO where
441+ Surface = State SDLSurface
442+
443+ initWindow x y = do Just srf <- lift (startSDL x y)
444+ | pure Nothing
445+ var <- new srf
446+ pure (Just var)
447+
448+ closeWindow win = do lift endSDL
449+ delete win
450+
451+ flip win = do srf <- read win
452+ lift (flipBuffers srf)
453+ poll = lift pollEvent
454+
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
461+
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.
467+
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:
472+
473+.. code-block:: idris
474+
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
478+ flip win
479+
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.
484+
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
487+application:
488+
489+.. code-block:: idris
490+
491+ loop : Draw m => (win : Var) -> ST m () [win ::: Surface {m}]
492+ loop win = do render win
493+ Just AppQuit <- poll
494+ | _ => loop win
495+ pure ()
496+
497+Finally, we can create a main program which initialises a window, if
498+possible, then runs the main loop:
499+
500+.. code-block:: idris
501+
502+ drawMain : (ConsoleIO m, Draw m) => ST m () []
503+ drawMain = do Just win <- initWindow 640 480
504+ | Nothing => putStrLn "Can't open window"
505+ loop win
506+ closeWindow win
507+
508+We can try this at the REPL using ``run``:
509+
510+.. code::
511+
512+ *Draw> :exec run drawMain
513+
514+A higher level interface: ``TurtleGraphics``
515+--------------------------------------------
516+
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
522+following:
523+
524+.. code-block:: idris
525+
526+ interface TurtleGraphics (m : Type -> Type) where
527+ Turtle : Type
528+
529+ start : Int -> Int -> ST m (Maybe Var) [addIfJust Turtle]
530+ end : (t : Var) -> ST m () [Remove t Turtle]
531+
532+ fd : (t : Var) -> Int -> ST m () [t ::: Turtle]
533+ rt : (t : Var) -> Int -> ST m () [t ::: Turtle]
534+
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]
538+
539+ render : (t : Var) -> ST m () [t ::: Turtle]
540+
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:
546+
547+.. code-block:: idris
548+
549+ turtle : (ConsoleIO m, TurtleGraphics m) => ST m () []
550+ turtle = with ST do
551+ Just t <- start 640 480
552+ | Nothing => putStr "Can't make turtle\n"
553+ col t yellow
554+ fd t 100; rt t 90
555+ col t green
556+ fd t 100; rt t 90
557+ col t red
558+ fd t 100; rt t 90
559+ col t blue
560+ fd t 100; rt t 90
561+ render t
562+ end t
563+
564+.. topic:: ``with ST do``
565+
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.
571+
572+To implement the interface, we could try using ``Surface`` to represent
573+the surface for the turtle to draw on:
574+
575+.. code-block:: idris
576+
577+ implementation Draw m => TurtleGraphics m where
578+ Turtle = Surface {m}
579+
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*
586+resource.
587+
588+Introducing composite resources
589+-------------------------------
590+
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``:
593+
594+.. code-block:: idris
595+
596+ data Composite : List Type -> Type
597+
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:
601+
602+.. code-block:: idris
603+
604+ splitComp : (comp : Var) -> ST m () [comp ::: Composite [State Int, State String]]
605+ splitComp comp = do [int, str] <- split comp
606+ ?whatNow
607+
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:
612+
613+.. code-block:: idris
614+
615+ int : Var
616+ str : Var
617+ comp : Var
618+ m : Type -> Type
619+ --------------------------------------
620+ whatNow : STrans m () [int ::: State Int, str ::: State String, comp ::: State ()]
621+ (\result => [comp ::: Composite [State Int, State String]])
622+
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
626+resources after all.
627+
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``:
631+
632+.. code-block:: idris
633+
634+ splitComp : (comp : Var) ->
635+ ST m () [comp ::: Composite [State Int, State String]]
636+ splitComp comp = do [int, str] <- split comp
637+ update int (+ 1)
638+ update str (++ "\n")
639+ combine comp [int, str]
640+ ?whatNow
641+
642+As ever, we can check the type of ``whatNow`` to see the effect of
643+``combine``:
644+
645+.. code-block:: idris
646+
647+ comp : Var
648+ int : Var
649+ str : Var
650+ m : Type -> Type
651+ --------------------------------------
652+ whatNow : STrans m () [comp ::: Composite [State Int, State String]]
653+ (\result => [comp ::: Composite [State Int, State String]])
654+
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 ()``.
659+
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``
662+is the following:
663+
664+.. code-block:: idris
665+
666+ split : (lbl : Var) -> {auto prf : InState lbl (Composite vars) res} ->
667+ STrans m (VarList vars) res (\ vs => mkRes vs ++ updateRes res prf (State ()))
668+
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 ()``.
674+
675+The ``combine`` function does the inverse:
676+
677+.. code-block:: idris
678+
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))
683+
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.
689+
690+We can use composite resources to implement our higher level ``TurtleGraphics``
691+API in terms of ``Draw``, and any additional resources we need.
692+
693+Implementing ``Turtle``
694+-----------------------
695+
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``:
701+
702+.. code-block:: idris
703+
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
708+
709+A ``Line`` is defined as a start location, and end location, and a colour:
710+
711+.. code-block:: idris
712+
713+ Line : Type
714+ Line = ((Int, Int), (Int, Int), Col)
715+
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:
720+
721+.. code-block:: idris
722+
723+ start x y = do Just srf <- initWindow x y
724+ | Nothing => pure Nothing
725+ col <- new white
726+ pos <- new (320, 200, 0, True)
727+ lines <- new []
728+ turtle <- new ()
729+ combine turtle [srf, col, pos, lines]
730+ pure (Just turtle)
731+
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:
737+
738+.. code-block:: idris
739+
740+ end t = do [srf, col, pos, lines] <- split t
741+ closeWindow srf; delete col; delete pos; delete lines; delete t
742+
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``:
746+
747+.. code-block:: idris
748+
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
753+
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:
757+
758+.. code-block:: idris
300759
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]
765+ Just ev <- poll
766+ | Nothing => render t -- Keep going until a key is pressed
767+ case ev of
768+ KeyUp _ => pure () -- Key pressed, so quit
769+ _ => render t
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
774+ drawAll srf xs