@@ -4,10 +4,296 @@
44Composing State Machines
55************************
66
7−Adding a login fail counter to the data store
8−(horizontal composition)
7+In the previous section, we defined a ``DataStore`` interface and used it
8+to implement the following small program which allows a user to log in to
9+the store then display the store's contents;
910
10−Vertical composition (what example?)
11+.. code-block:: idris
12+
13+ getData : (ConsoleIO m, DataStore m) => ST m () []
14+ getData = do st <- connect
15+ OK <- login st
16+ | BadPassword => do putStrLn "Failure"
17+ disconnect st
18+ secret <- readSecret st
19+ putStrLn ("Secret is: " ++ show secret)
20+ logout st
21+ disconnect st
22+
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.
28+
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
34+state for the turtle.
35+
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``.
39+
40+Working with multiple resources
41+===============================
42+
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:
47+
48+.. code::
49+
50+ *LoginCount> :exec main
51+ Enter password: Mornington Crescent
52+ Secret is: "Secret Data"
53+ Enter password: Dollis Hill
54+ Failure
55+ Number of failures: 1
56+ Enter password: Mornington Crescent
57+ Secret is: "Secret Data"
58+ Enter password: Codfanglers
59+ Failure
60+ Number of failures: 2
61+ ...
62+
63+We'll start by adding a state resource to ``getData`` to keep track of the
64+number of failures:
65+
66+.. code-block:: idrs
67+
68+ getData : (ConsoleIO m, DataStore m) =>
69+ (failcount : Var) -> ST m () [failcount ::: State Integer]
70+
71+.. topic:: Type checking ``getData``
72+
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
76+ to it shortly.
77+
78+Then, we can create a ``main`` program which initialises the state to ``0``
79+and invokes ``getData``, as follows:
80+
81+.. code-block:: idris
82+
83+ main : IO ()
84+ main = run (do fc <- new 0
85+ getData fc
86+ delete fc)
87+
88+We'll start our implementation of ``getData`` just by adding the new
89+argument for the failure count:
90+
91+.. code-block:: idris
92+
93+ getData : (ConsoleIO m, DataStore m) =>
94+ (failcount : Var) -> ST m () [failcount ::: State Integer]
95+ getData failcount
96+ = do st <- connect
97+ OK <- login st
98+ | BadPassword => do putStrLn "Failure"
99+ disconnect st
100+ secret <- readSecret st
101+ putStrLn ("Secret is: " ++ show secret)
102+ logout st
103+ disconnect st
104+
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
107+match:
108+
109+.. code-block:: idris
110+
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
117+
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.
124+
125+We can achieve this with the ``call`` function:
126+
127+.. code-block:: idris
128+
129+ getData : (ConsoleIO m, DataStore m) =>
130+ (failcount : Var) -> ST m () [failcount ::: State Integer]
131+ getData failcount
132+ = do st <- call connect
133+ ?whatNow
134+
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:
140+
141+.. code-block:: idris
142+
143+ failcount : Var
144+ m : Type -> Type
145+ constraint : ConsoleIO m
146+ constraint1 : DataStore m
147+ st : Var
148+ --------------------------------------
149+ whatNow : STrans m () [failcount ::: State Integer, st ::: Store LoggedOut]
150+ (\result => [failcount ::: State Integer])
151+
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
156+resources:
157+
158+.. code-block:: idris
159+
160+ getData : (ConsoleIO m, DataStore m) =>
161+ (failcount : Var) -> ST m () [failcount ::: State Integer]
162+ getData failcount
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)
169+ call $ logout st
170+ call $ disconnect st
171+
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.
176+
177+.. code-block:: idris
178+
179+ import Control.ST.ImplicitCall
180+
181+It's now possible to write ``getData`` exactly as before:
182+
183+.. code-block:: idris
184+
185+ getData : (ConsoleIO m, DataStore m) =>
186+ (failcount : Var) -> ST m () [failcount ::: State Integer]
187+ getData failcount
188+ = do st <- connect
189+ OK <- login st
190+ | BadPassword => do putStrLn "Failure"
191+ disconnect st
192+ secret <- readSecret st
193+ putStrLn ("Secret is: " ++ show secret)
194+ logout st
195+ disconnect st
196+
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.
202+
203+It is instructive to see the type of ``call``:
204+
205+.. code-block:: idris
206+
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)
209+
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).
216+
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
221+manipulation.
222+
223+.. topic:: Newly created resources in called functions
224+
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.
229+
230+Finally, we can update ``getData`` so that it loops, and keeps
231+``failCount`` updated as necessary:
232+
233+.. code-block:: idris
234+
235+ getData : (ConsoleIO m, DataStore m) =>
236+ (failcount : Var) -> ST m () [failcount ::: State Integer]
237+ getData failcount
238+ = do st <- call connect
239+ OK <- login st
240+ | BadPassword => do putStrLn "Failure"
241+ fc <- read failcount
242+ write failcount (fc + 1)
243+ putStrLn ("Number of failures: " ++ show (fc + 1))
244+ disconnect st
245+ getData failcount
246+ secret <- readSecret st
247+ putStrLn ("Secret is: " ++ show secret)
248+ logout st
249+ disconnect st
250+ getData failcount
251+
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:
255+
256+.. code-block:: idris
257+
258+ getData : (ConsoleIO m, DataStore m) =>
259+ (st, failcount : Var) -> ST m () [st ::: Store {m} LoggedOut, failcount ::: State Integer]
260+ getData st failcount
261+ = do OK <- login st
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)
269+ logout st
270+ getData st failcount
271+
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
277+context ``m``.
278+
279+We can then ``connect`` and ``disconnect`` only once, in ``main``:
280+
281+.. code-block:: idris
282+
283+ main : IO ()
284+ main = run (do fc <- new 0
285+ st <- connect
286+ getData st fc
287+ disconnect st
288+ delete fc)
289+
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.
294+
295+Composite resources: Hierarchies of state machines
296+==================================================
11297
12298Composite resources: Graphics
13299