@@ -4,3 +4,385 @@
44State Machines in Types
55***********************
66
7+In the introduction, we saw the following state transition diagram representing
8+the (abstract) states of a data store, and the actions we can perform on the
9+store:
10+
11+|login|
12+
13+We say that these are the *abstract* states of the store, because the concrete
14+state will contain a lot more information: for example, it might contain
15+user names, hashed passwords, the store contents, and so on. However, as far
16+as we are concerned for the actions ``login``, ``logout`` and ``readSecret``,
17+it's whether we are logged in or not which affects which are valid.
18+
19+We've seen how to manipulate states using ``ST``, and some small examples
20+of dependent types in states. In this section, we'll see how to use
21+``ST`` to provide a safe API for the data store. In the API, we'll encode
22+the above diagram in the types, in such a way that we can only execute the
23+operations ``login``, ``logout`` and ``readSecret`` when the state is
24+valid.
25+
26+So far, we've used ``State`` and the primitive operations, ``new``, ``read``,
27+``write`` and ``delete`` to manipulate states. For the data store API,
28+however, we'll begin by defining an *interface* (see :ref:`sect-interfaces` in
29+the Idris tutorial) which describes the operations on the store, and explains
30+in their types exactly when each operation is valid, and how it affects
31+the store's state. By using an interface, we can be sure that
32+this is the *only* way to access the store.
33+
34+Defining an interface for the data store
35+========================================
36+
37+We'll begin by defining a data type which represents the two abstract states
38+of the store, either ``LoggedOut`` or ``LoggedIn``:
39+
40+.. code-block:: idris
41+
42+ data Access = LoggedOut | LoggedIn
43+
44+We can define a data type for representing the current state of a store,
45+holding all of the necessary information (this might be user names, hashed
46+passwords, store contents and so on) and parameterise it by the logged in
47+status of the store:
48+
49+.. code-block:: idris
50+
51+ Store : Access -> Type
52+
53+Rather than defining a concrete type now, however, we'll include this in
54+a data store *interface* and define a concrete type later:
55+
56+.. code-block:: idris
57+
58+ interface DataStore (m : Type -> Type) where
59+ Store : Access -> Type
60+
61+We can continue to populate this interface with operations on the store. Among
62+other advantages, by separating the *interface* from its *implementation* we
63+can provide different concrete implementations for different contexts.
64+Furthermore, we can write programs which work with a store without needing
65+to know any details of how the store is implemented.
66+
67+We'll need to be able to ``connect`` to a store, and ``disconnect`` when
68+we're done. Add the following methods to the ``DataStore`` interface:
69+
70+.. code-block:: idris
71+
72+ connect : ST m Var [add (Store LoggedOut)]
73+ disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]
74+
75+The type of ``connect`` says that it returns a new resource which has the
76+initial type ``Store LoggedOut``. Conversely, ``disconnect``, given a
77+resource in the state ``Store LoggedOut``, removes that resource.
78+We can see more clearly what ``connect`` does by trying the following
79+(incomplete) definition:
80+
81+.. code-block:: idris
82+
83+ doConnect : DataStore m => ST m () []
84+ doConnect = do st <- connect
85+ ?whatNow
86+
87+Note that we're working in a *generic* context ``m``, constrained so that
88+there must be an implementation of ``DataStore`` for ``m`` to be able to
89+execute ``doConnect``.
90+If we check the type of ``?whatNow``, we'll see that the remaining
91+operations begin with a resource ``st`` in the state ``Store LoggedOut``,
92+and we need to finish with no resources.
93+
94+.. code-block:: idris
95+
96+ m : Type -> Type
97+ constraint : DataStore m
98+ st : Var
99+ --------------------------------------
100+ whatNow : STrans m () [st ::: Store LoggedOut] (\result => [])
101+
102+Then, we can remove the resource using ``disconnect``:
103+
104+.. code-block:: idris
105+
106+ doConnect : DataStore m => ST m () []
107+ doConnect = do st <- connect
108+ disconnect st
109+ ?whatNow
110+
111+Now checking the type of ``?whatNow`` shows that we have no resources
112+available:
113+
114+.. code-block:: idris
115+
116+ m : Type -> Type
117+ constraint : DataStore m
118+ st : Var
119+ --------------------------------------
120+ whatNow : STrans m () [] (\result => [])
121+
122+To continue our implementation of the ``DataStore`` interface, next we'll add a
123+method for reading the secret data. This requires that the ``store`` is in the
124+state ``Store LoggedIn``:
125+
126+.. code-block:: idris
127+
128+ readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]
129+
130+At this point we can try writing a function which connects to a store,
131+reads the secret, then disconnects. However, it will be unsuccessful, because
132+``readSecret`` requires us to be logged in:
133+
134+.. code-block:: idris
135+
136+ badGet : DataStore m => ST m () []
137+ badGet = do st <- connect
138+ secret <- readSecret st
139+ disconnect st
140+
141+This results in the following error, because ``connect`` creates a new
142+store in the ``LoggedOut`` state, and ``readSecret`` requires the store
143+to be in the ``LoggedIn`` state:
144+
145+.. code-block:: idris
146+
147+ When checking an application of function Control.ST.>>=:
148+ Error in state transition:
149+ Operation has preconditions: [st ::: Store LoggedOut]
150+ States here are: [st ::: Store LoggedIn]
151+ Operation has postconditions: \result => []
152+ Required result states here are: \result => []
153+
154+The error message explains how the required input states (the preconditions)
155+and the required output states (the postconditions) differ from the states
156+in the operation. In order to use ``readSecret``, we'll need a way to get
157+from a ``Store LoggedOut`` to a ``Store LoggedIn``. As a first attempt,
158+we can try the following type for ``login``:
159+
160+.. code-block:: idris
161+
162+ login : (store : Var) -> ST m () [store ::: Store LoggedOut :-> Store LoggedIn] -- Incorrect type!
163+
164+Note that in the *interface* we say nothing about *how* ``login`` works;
165+merely how it affects the overall state. Even so, there is a problem with
166+the type of ``login``, because it makes the assumption that it will always
167+succeed. If it fails - for example because the implementation prompts for
168+a password and the user enters the password incorrectly - then it must not
169+result in a ``LoggedIn`` store.
170+
171+Instead, therefore, ``login`` will return whether logging in was successful,
172+via the following type;
173+
174+.. code-block:: idris
175+
176+ data LoginResult = OK | BadPassword
177+
178+Then, we can *calculate* the result state (see :ref:`depstate`) from the
179+result. Add the following method to the ``DataStore`` interface:
180+
181+.. code-block:: idris
182+
183+ login : (store : Var) ->
184+ ST m LoginResult [store ::: Store LoggedOut :->
185+ (\res => Store (case res of
186+ OK => LoggedIn
187+ BadPassword => LoggedOut))]
188+
189+If ``login`` was successful, then the state after ``login`` is
190+``Store LoggedIn``. Otherwise, the state is ``Store LoggedOut``.
191+
192+To complete the interface, we'll add a method for logging out of the store.
193+We'll assume that logging out is always successful, and moves the store
194+from the ``Store LoggedIn`` state to the ``Store LoggedOut`` state.
195+
196+.. code-block:: idris
197+
198+ logout : (store : Var) -> ST m () [store ::: Store LoggedIn :-> Store LoggedOut]
199+
200+This completes the interface, repeated in full for reference below:
201+
202+.. code-block:: idris
203+
204+ interface DataStore (m : Type -> Type) where
205+ Store : Access -> Type
206+
207+ connect : ST m Var [add (Store LoggedOut)]
208+ disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]
209+
210+ readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]
211+ login : (store : Var) ->
212+ ST m LoginResult [store ::: Store LoggedOut :->
213+ (\res => Store (case res of
214+ OK => LoggedIn
215+ BadPassword => LoggedOut))]
216+ logout : (store : Var) -> ST m () [store ::: Store LoggedIn :-> Store LoggedOut]
217+
218+Before we try creating any implementations of this interface, let's see how
219+we can write a function with it, to log into a data store, read the secret
220+if login is successful, then log out again.
221+
222+Writing a function with the data store
223+======================================
224+
225+As an example of working with the ``DataStore`` interface, we'll write a
226+function ``getData``, which connects to a store in order to read some data from
227+it. We'll write this function interactively, step by step, using the types of
228+the operations to guide its development. It has the following type:
229+
230+.. code-block:: idris
231+
232+ getData : (ConsoleIO m, DataStore m) => ST m () []
233+
234+This type means that there are no resources available on entry or exit.
235+That is, the overall list of actions is ``[]``, meaning that at least
236+externally, the function has no overall effect on the resources. In other
237+words, for every resource we create during ``getData``, we'll also need to
238+delete it before exit.
239+
240+Since we want to use methods of the ``DataStore`` interface, we'll
241+constraint the computation context ``m`` so that there must be an
242+implementation of ``DataStore``. We also have a constraint ``ConsoleIO m``
243+so that we can display any data we read from the store, or any error
244+messages.
245+
246+We start by connecting to the store, creating a new resource ``st``, then
247+trying to ``login``:
248+
249+.. code-block:: idris
250+
251+ getData : (ConsoleIO m, DataStore m) => ST m () []
252+ getData = do st <- connect
253+ ok <- login st
254+ ?whatNow
255+
256+Logging in will either succeed or fail, as reflected by the value of
257+``ok``. If we check the type of ``?whatNow``, we'll see what state the
258+store currently has:
259+
260+.. code-block:: idris
261+
262+ m : Type -> Type
263+ constraint : ConsoleIO m
264+ constraint1 : DataStore m
265+ st : Var
266+ ok : LoginResult
267+ --------------------------------------
268+ whatNow : STrans m () [st ::: Store (case ok of
269+ OK => LoggedIn
270+ BadPassword => LoggedOut)]
271+ (\result => [])
272+
273+The current state of ``st`` therefore depends on the value of ``ok``,
274+meaning that we can make progress by case splitting on ``ok``:
275+
276+.. code-block:: idris
277+
278+ getData : (ConsoleIO m, DataStore m) => ST m () []
279+ getData = do st <- connect
280+ ok <- login st
281+ case ok of
282+ OK => ?whatNow_1
283+ BadPassword => ?whatNow_2
284+
285+The types of the holes in each branch, ``?whatNow_1`` and ``?whatNow_2``,
286+show how the state changes depending on whether logging in was successful.
287+If it succeeded, the store is ``LoggedIn``:
288+
289+.. code-block:: idris
290+
291+ --------------------------------------
292+ whatNow_1 : STrans m () [st ::: Store LoggedIn] (\result => [])
293+
294+On the other hand, if it failed, the store is ``LoggedOut``:
295+
296+.. code-block:: idris
297+
298+ --------------------------------------
299+ whatNow_2 : STrans m () [st ::: Store LoggedOut] (\result => [])
300+
301+In ``?whatNow_1``, since we've successfully logged in, we can now read
302+the secret and display it to the console:
303+
304+.. code-block:: idris
305+
306+ getData : (ConsoleIO m, DataStore m) => ST m () []
307+ getData = do st <- connect
308+ ok <- login st
309+ case ok of
310+ OK => do secret <- readSecret st
311+ putStrLn ("Secret is: " ++ show secret)
312+ ?whatNow_1
313+ BadPassword => ?whatNow_2
314+
315+We need to finish the ``OK`` branch with no resources available. We can
316+do this by logging out of the store then disconnecting:
317+
318+.. code-block:: idris
319+
320+ getData : (ConsoleIO m, DataStore m) => ST m () []
321+ getData = do st <- connect
322+ ok <- login st
323+ case ok of
324+ OK => do secret <- readSecret st
325+ putStrLn ("Secret is: " ++ show secret)
326+ logout st
327+ disconnect st
328+ BadPassword => ?whatNow_2
329+
330+Note that we *must* ``logout`` of ``st`` before calling ``disconnect``,
331+because ``disconnect`` requires that the store is in the ``LoggedOut``
332+state.
333+
334+Furthermore, we can't simply use ``delete`` to remove the resource, as
335+we did with the ``State`` examples in the previous section, because
336+``delete`` only works when the resource has type ``State ty``, for some
337+type ``ty``. If we try to use ``delete`` instead of ``disconnect``, we'll
338+see an error message like the following:
339+
340+.. code-block:: idris
341+
342+ When checking argument prf to function Control.ST.delete:
343+ Can't find a value of type
344+ InState st (State st) [st ::: Store LoggedOut]
345+
346+In other words, the type checker can't find a proof that the resource
347+``st`` has a type of the form ``State st``, because its type is
348+``Store LoggedOut``. Since ``Store`` is part of the ``DataStore`` interface,
349+we *can't* yet know the concrete representation of the ``Store``, so we
350+need to remove the resource via the interface, with ``disconnect``, rather
351+than directly with ``delete``.
352+
353+We can complete ``getData`` as follows, using a pattern matching bind
354+alternative (see the Idris tutorial, :ref:`monadsdo`) rather than a
355+``case`` statement to catch the possibilty of an error with ``login``:
356+
357+.. code-block:: idris
358+
359+ getData : (ConsoleIO m, DataStore m) => ST m () []
360+ getData = do st <- connect
361+ OK <- login st
362+ | BadPassword => do putStr "Failure\n"
363+ disconnect st
364+ secret <- readSecret st
365+ putStr ("Secret is: " ++ show secret ++ "\n")
366+ logout st
367+ disconnect st
368+
369+We can't yet try this out, however, because we don't have any implementations
370+of ``getData``! If we try to execute it in an ``IO`` context, for example,
371+we'll get an error saying that there's no implementation of ``DataStore IO``:
372+
373+.. code::
374+
375+ *Login> :exec run {m = IO} getData
376+ When checking an application of function Control.ST.run:
377+ Can't find implementation for DataStore IO
378+
379+The final step in implementing a data store which correctly follows the
380+state transition diagram, therefore, is to provide an implementation
381+of ``DataStore``.
382+
383+Implementing the interface
384+==========================
385+
386+
387+.. |login| image:: ../image/login.png
388+ :width: 500px