@@ -4,10 +4,296 @@
4Composing State Machines
4Composing State Machines
5************************
5************************
7−Adding a login fail counter to the data store
7+In the previous section, we defined a ``DataStore`` interface and used it
8−(horizontal composition)
8+to implement the following small program which allows a user to log in to
9+the store then display the store's contents;
10−Vertical composition (what example?)
11+.. code-block:: idris
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)
23+This function only uses one state, the store itself. Usually, though,
24+larger programs have lots of states, and might add, delete and update
25+states over the course of its execution. Here, for example, a useful
26+extension might be to loop forever, keeping count of the number of times
27+there was a login failure in a state.
29+Furthermore, we may have *hierarchies* of state machines, in that one
30+state machine could be implemented by composing several others. For
31+example, we can have a state machine representing the state of a
32+graphics system, and use this to implement a *higher level* graphics API
33+such as turtle graphics, which uses the graphics system plus some additional
36+In this section, we'll see how to work with multiple states, and how to
37+compose state machines to make higher level state machines. We'll begin by
38+seeing how to add a login failure counter to ``getData``.
40+Working with multiple resources
41+===============================
43+To see how to work with multiple resources, we'll modify ``getData`` so
44+that it loops, and counts the total number of times the user fails to
45+log in. For example, if we write a ``main`` program which initialises the
46+count 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
55+ Number of failures: 1
56+ Enter password: Mornington Crescent
57+ Secret is: "Secret Data"
58+ Enter password: Codfanglers
60+ Number of failures: 2
63+We'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
78+Then, we can create a ``main`` program which initialises the state to ``0``
79+and invokes ``getData``, as follows:
84+ main = run (do fc <- new 0
88+We'll start our implementation of ``getData`` just by adding the new
89+argument 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)
105+Unfortunately, this doesn't type check, because we have the wrong resources
106+for calling ``connect``. The error messages shows how the resources don't
109+.. code-block:: idris
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
118+In other words, ``connect`` requires that there are *no* resources on
119+entry, but we have *one*, the failure count!
120+This shouldn't be a problem, though: the required resources are a *subset* of
121+the resources we have, after all, and the additional resources (here, the
122+failure count) are not relevant to ``connect``. What we need, therefore,
123+is a way to temporarily *hide* the additional resource.
125+We can achieve this with the ``call`` function:
127+.. code-block:: idris
129+ getData : (ConsoleIO m, DataStore m) =>
130+ (failcount : Var) -> ST m () [failcount ::: State Integer]
132+ = do st <- call connect
135+Here we've left a hole for the rest of ``getData`` so that you can see the
136+effect of ``call``. It has removed the unnecessary parts of the resource
137+list 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
139+have ``failcount`` available:
141+.. code-block:: idris
145+ constraint : ConsoleIO m
146+ constraint1 : DataStore m
148+ --------------------------------------
149+ whatNow : STrans m () [failcount ::: State Integer, st ::: Store LoggedOut]
150+ (\result => [failcount ::: State Integer])
152+By 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``
154+so that it works with an additional state resource by adding ``call`` whenever
155+we invoke one of the operations on the data store, to reduce the list of
158+.. code-block:: idris
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"
166+ call $ disconnect st
167+ secret <- call $ readSecret st
168+ putStrLn ("Secret is: " ++ show secret)
170+ call $ disconnect st
172+This is a little noisy, and in fact we can remove the need for it by
173+making ``call`` implicit. By default, you need to add the ``call`` explicitly,
174+but if you import ``Control.ST.ImplicitCall``, Idris will insert ``call``
175+where it is necessary.
177+.. code-block:: idris
179+ import Control.ST.ImplicitCall
181+It's now possible to write ``getData`` exactly as before:
183+.. code-block:: idris
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)
197+There is a trade off here: if you import ``Control.ST.ImplicitCall`` then
198+functions which use multiple resources are much easier to read, because the
199+noise of ``call`` has gone. On the other hand, Idris has to work a little
200+harder to type check your functions, and as a result it can take slightly
201+longer, and the error messages can be less helpful.
203+It is instructive to see the type of ``call``:
205+.. code-block:: idris
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)
210+The function being called has a list of resources ``sub``, and
211+there is an implicit proof, ``SubRes sub old`` that the resource list in
212+the function being called is a subset of the overall resource list. The
213+ordering of resources is allowed to change, although resources which
214+appear in ``old`` can't appear in the ``sub`` list more than once (you will
215+get a type error if you try this).
217+The function ``updateWith`` takes the *output* resources of the
218+called function, and updates them in the current resource list. It makes
219+an effort to preserve ordering as far as possible, although this isn't
220+always 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.
230+Finally, we can update ``getData`` so that it loops, and keeps
231+``failCount`` updated as necessary:
233+.. code-block:: idris
235+ getData : (ConsoleIO m, DataStore m) =>
236+ (failcount : Var) -> ST m () [failcount ::: State Integer]
238+ = do st <- call connect
240+ | BadPassword => do putStrLn "Failure"
241+ fc <- read failcount
242+ write failcount (fc + 1)
243+ putStrLn ("Number of failures: " ++ show (fc + 1))
246+ secret <- readSecret st
247+ putStrLn ("Secret is: " ++ show secret)
252+Note that here, we're connecting and disconnecting on every iteration.
253+Another way to implement this would be to ``connect`` first, then call
254+``getData``, and implement ``getData`` as follows:
256+.. code-block:: idris
258+ getData : (ConsoleIO m, DataStore m) =>
259+ (st, failcount : Var) -> ST m () [st ::: Store {m} LoggedOut, failcount ::: State Integer]
260+ getData st failcount
262+ | BadPassword => do putStrLn "Failure"
263+ fc <- read failcount
264+ write failcount (fc + 1)
265+ putStrLn ("Number of failures: " ++ show (fc + 1))
266+ getData st failcount
267+ secret <- readSecret st
268+ putStrLn ("Secret is: " ++ show secret)
270+ getData st failcount
272+It is important to add the explicit ``{m}`` in the type of ``Store {m}
273+LoggedOut`` for ``st``, because this gives Idris enough information to know
274+which implementation of ``DataStore`` to use to find the appropriate
275+implementation for ``Store``. Otherwise, if we only write ``Store LoggedOut``,
276+there's no way to know that the ``Store`` is linked with the computation
279+We can then ``connect`` and ``disconnect`` only once, in ``main``:
281+.. code-block:: idris
284+ main = run (do fc <- new 0
290+By using ``call``, and importing ``Control.ST.ImplicitCall``, we can
291+write programs which use multiple resources, and reduce the list of
292+resources as necessary when calling functions which only use a subset of
293+the overall resources.
295+Composite resources: Hierarchies of state machines
296+==================================================
12Composite resources: Graphics
298Composite resources: Graphics