@@ -4,3 +4,385 @@
4State Machines in Types
4State Machines in Types
5***********************
5***********************
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
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.
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
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.
34+Defining an interface for the data store
35+========================================
37+We'll begin by defining a data type which represents the two abstract states
38+of the store, either ``LoggedOut`` or ``LoggedIn``:
42+ data Access = LoggedOut | LoggedIn
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
51+ Store : Access -> Type
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:
58+ interface DataStore (m : Type -> Type) where
59+ Store : Access -> Type
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.
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:
72+ connect : ST m Var [add (Store LoggedOut)]
73+ disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]
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:
83+ doConnect : DataStore m => ST m () []
84+ doConnect = do st <- connect
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.
97+ constraint : DataStore m
99+ --------------------------------------
100+ whatNow : STrans m () [st ::: Store LoggedOut] (\result => [])
102+Then, we can remove the resource using ``disconnect``:
104+.. code-block:: idris
106+ doConnect : DataStore m => ST m () []
107+ doConnect = do st <- connect
111+Now checking the type of ``?whatNow`` shows that we have no resources
114+.. code-block:: idris
117+ constraint : DataStore m
119+ --------------------------------------
120+ whatNow : STrans m () [] (\result => [])
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``:
126+.. code-block:: idris
128+ readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]
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:
134+.. code-block:: idris
136+ badGet : DataStore m => ST m () []
137+ badGet = do st <- connect
138+ secret <- readSecret st
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:
145+.. code-block:: idris
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 => []
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``:
160+.. code-block:: idris
162+ login : (store : Var) -> ST m () [store ::: Store LoggedOut :-> Store LoggedIn] -- Incorrect type!
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.
171+Instead, therefore, ``login`` will return whether logging in was successful,
172+via the following type;
174+.. code-block:: idris
176+ data LoginResult = OK | BadPassword
178+Then, we can *calculate* the result state (see :ref:`depstate`) from the
179+result. Add the following method to the ``DataStore`` interface:
181+.. code-block:: idris
183+ login : (store : Var) ->
184+ ST m LoginResult [store ::: Store LoggedOut :->
185+ (\res => Store (case res of
187+ BadPassword => LoggedOut))]
189+If ``login`` was successful, then the state after ``login`` is
190+``Store LoggedIn``. Otherwise, the state is ``Store LoggedOut``.
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.
196+.. code-block:: idris
198+ logout : (store : Var) -> ST m () [store ::: Store LoggedIn :-> Store LoggedOut]
200+This completes the interface, repeated in full for reference below:
202+.. code-block:: idris
204+ interface DataStore (m : Type -> Type) where
205+ Store : Access -> Type
207+ connect : ST m Var [add (Store LoggedOut)]
208+ disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]
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
215+ BadPassword => LoggedOut))]
216+ logout : (store : Var) -> ST m () [store ::: Store LoggedIn :-> Store LoggedOut]
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.
222+Writing a function with the data store
223+======================================
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:
230+.. code-block:: idris
232+ getData : (ConsoleIO m, DataStore m) => ST m () []
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.
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
246+We start by connecting to the store, creating a new resource ``st``, then
249+.. code-block:: idris
251+ getData : (ConsoleIO m, DataStore m) => ST m () []
252+ getData = do st <- connect
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
260+.. code-block:: idris
263+ constraint : ConsoleIO m
264+ constraint1 : DataStore m
267+ --------------------------------------
268+ whatNow : STrans m () [st ::: Store (case ok of
270+ BadPassword => LoggedOut)]
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``:
276+.. code-block:: idris
278+ getData : (ConsoleIO m, DataStore m) => ST m () []
279+ getData = do st <- connect
283+ BadPassword => ?whatNow_2
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``:
289+.. code-block:: idris
291+ --------------------------------------
292+ whatNow_1 : STrans m () [st ::: Store LoggedIn] (\result => [])
294+On the other hand, if it failed, the store is ``LoggedOut``:
296+.. code-block:: idris
298+ --------------------------------------
299+ whatNow_2 : STrans m () [st ::: Store LoggedOut] (\result => [])
301+In ``?whatNow_1``, since we've successfully logged in, we can now read
302+the secret and display it to the console:
304+.. code-block:: idris
306+ getData : (ConsoleIO m, DataStore m) => ST m () []
307+ getData = do st <- connect
310+ OK => do secret <- readSecret st
311+ putStrLn ("Secret is: " ++ show secret)
313+ BadPassword => ?whatNow_2
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:
318+.. code-block:: idris
320+ getData : (ConsoleIO m, DataStore m) => ST m () []
321+ getData = do st <- connect
324+ OK => do secret <- readSecret st
325+ putStrLn ("Secret is: " ++ show secret)
328+ BadPassword => ?whatNow_2
330+Note that we *must* ``logout`` of ``st`` before calling ``disconnect``,
331+because ``disconnect`` requires that the store is in the ``LoggedOut``
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:
340+.. code-block:: idris
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]
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``.
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``:
357+.. code-block:: idris
359+ getData : (ConsoleIO m, DataStore m) => ST m () []
360+ getData = do st <- connect
362+ | BadPassword => do putStr "Failure\n"
364+ secret <- readSecret st
365+ putStr ("Secret is: " ++ show secret ++ "\n")
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``:
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
379+The final step in implementing a data store which correctly follows the
380+state transition diagram, therefore, is to provide an implementation
383+Implementing the interface
384+==========================
387+.. |login| image:: ../image/login.png