@@ -0,0 +1,605 @@
1+**********************************
2+Introducing ST: Working with State
3+**********************************
4+
5+The ``Control.ST`` library provides facilities for creating, reading, writing
6+and destroying state in Idris functions, and tracking changes of state in
7+a function's type. It is based around the concept of *resources*, which are,
8+essentially, mutable variables, and a dependent type, ``STrans`` which tracks
9+how those resources change when a function runs:
10+
11+.. code-block:: idris
12+
13+ STrans : (m : Type -> Type) ->
14+ (resultType : Type) ->
15+ (in_res : Resources) ->
16+ (out_res : resultType -> Resources) ->
17+ Type
18+
19+A value of type ``STrans m resultType in_res out_res_fn`` represents a sequence
20+of actions which can manipulate state. The arguments are:
21+
22+* ``m``, which is an underlying *context* in which the actions will be executed.
23+ Usually, this will be a generic type with a ``Monad`` implementation, but
24+ it isn't necessarily so. In particular, there is no need to understand monads
25+ to be able to use ``ST`` effectively!
26+* ``resultType``, which is the type of the value the sequence will produce
27+* ``in_res``, which is a list of *resources* available *before* executing the actions.
28+* ``out_res``, which is a list of resources available *after* executing the actions,
29+ and may differ depending on the result of the actions.
30+
31+We can use ``STrans`` to describe *state transition systems* in a function's
32+type. We'll come to the definition of ``Resources`` shortly, but for the moment
33+you can consider it an abstract representation of the "state of the world".
34+By giving the input resources (``in_res``) and the output resources
35+(``out_res``) we are describing the *preconditions* under which a function
36+is allowed to execute, and *postconditions* which describe how a function
37+affects the overall state of the world.
38+
39+We'll begin in this section by looking at some small examples of ``STrans``
40+functions, and see how to execute them. We'll also introduce ``ST``,
41+a type-level function which allows us to describe the state transitions of
42+a stateful function concisely.
43+
44+.. topic:: Type checking the examples
45+
46+ For the examples in this section, and throughout this tutorial,
47+ you'll need to ``import Control.ST`` and add the ``contrib`` package by
48+ passing the ``-p contrib`` flag to ``idris``.
49+
50+
51+Introductory examples: manipulating ``State``
52+=============================================
53+
54+An ``STrans`` function explains, in its type, how it affects a collection of
55+``Resources``. A resource has a *label* (of type ``Var``), which we use to
56+refer to the resource throughout the function, and we write the state of a
57+resource, in the ``Resources`` list, in the form ``label ::: type``.
58+
59+For example, the following function
60+has a resource ``x`` available on input, of type ``State Integer``, and that
61+resource is still a ``State Integer`` on output:
62+
63+.. code-block:: idris
64+
65+ increment : (x : Var) -> STrans m () [x ::: State Integer]
66+ (const [x ::: State Integer])
67+ increment x = do num <- read x
68+ write x (num + 1)
69+
70+.. sidebar:: Verbosity of the type of ``increment``
71+
72+ The type of ``increment`` may seem somewhat verbose, in that the
73+ *input* and *output* resources are repeated, even though they are the
74+ same. We'll introduce a much more concise way of writing this type at the
75+ end of this section (:ref:`sttype`), when we describe the ``ST`` type
76+ itself.
77+
78+This function reads the value stored at the resource ``x`` with ``read``,
79+increments it then writes the result back into the resource ``x`` with
80+``write``. We'll see the types of ``read`` and ``write`` shortly
81+(see :ref:`stransprimops`). We can also create and delete resources:
82+
83+.. code-block:: idris
84+
85+ makeAndIncrement : Integer -> STrans m Integer [] (const [])
86+ makeAndIncrement init = do var <- new init
87+ increment var
88+ x <- read var
89+ delete var
90+ pure x
91+
92+The type of ``makeAndIncrement`` states that it has *no* resources available on
93+entry (``[]``) or exit (``const []``). It creates a new ``State`` resource with
94+``new`` (which takes an initial value for the resource), increments the value,
95+reads it back, then deletes it using ``delete``, returning the final value
96+of the resource. Again, we'll see the types of ``new`` and ``delete``
97+shortly.
98+
99+The ``m`` argument to ``STrans`` (of type ``Type -> Type``) is the *context* in
100+which the function can be run. Here, the type level variable indicates that we
101+can run it in *any* context. We can run it in the identity context with
102+``runPure``. For example, try entering the above definitions in a file
103+``Intro.idr`` then running the following at the REPL:
104+
105+.. code::
106+
107+ *Intro> runPure (makeAndIncrement 93)
108+ 94 : Integer
109+
110+It's a good idea to take an interactive, type-driven approach to implementing
111+``STrans`` programs. For example, after creating the resource with ``new init``,
112+you can leave a *hole* for the rest of the program to see how creating the
113+resource has affected the type:
114+
115+.. code-block:: idris
116+
117+ makeAndIncrement : Integer -> STrans m Integer [] (const [])
118+ makeAndIncrement init = do var <- new init
119+ ?whatNext
120+
121+If you check the type of ``?whatNext``, you'll see that there is now
122+a resource available, ``var``, and that by the end of the function there
123+should be no resource available:
124+
125+.. code-block:: idris
126+
127+ init : Integer
128+ m : Type -> Type
129+ var : Var
130+ --------------------------------------
131+ whatNext : STrans m Integer [var ::: State Integer] (\value => [])
132+
133+These small examples work in any computation context ``m``. However, usually,
134+we are working in a more restricted context. For example, we might want to
135+write programs which only work in a context that supports interactive
136+programs. For this, we'll need to see how to *lift* operations from the
137+underlying context.
138+
139+Lifting: Using the computation context
140+======================================
141+
142+Let's say that, instead of passing an initial integer to ``makeAndIncrement``,
143+we want to read it in from the console. Then, instead of working in a generic
144+context ``m``, we can work in the specific context ``IO``:
145+
146+.. code-block:: idris
147+
148+ ioMakeAndIncrement : STrans IO () [] (const [])
149+
150+This gives us access to ``IO`` operations, via the ``lift`` function. We
151+can define ``ioMakeAndIncrement`` as follows:
152+
153+.. code-block:: idris
154+
155+ ioMakeAndIncrement : STrans IO () [] (const [])
156+ ioMakeAndIncrement
157+ = do lift $ putStr "Enter a number: "
158+ init <- lift $ getLine
159+ var <- new (cast init)
160+ lift $ putStrLn ("var = " ++ show !(read var))
161+ increment var
162+ lift $ putStrLn ("var = " ++ show !(read var))
163+ delete var
164+
165+The ``lift`` function allows us to use funtions from the underlying
166+computation context (``IO`` here) directly. Again, we'll see the exact type
167+of ``lift`` shortly.
168+
169+In general, though, it's bad practice to use a *specific* context like
170+``IO``. Firstly, it requires us to sprinkle ``lift`` liberally throughout
171+our code, which hinders readability. Secondly, and more importantly, it will
172+limit the safety of our functions, as we'll see in the next section
173+(:ref:`smstypes`).
174+
175+So, instead, we define *interfaces* to restrict the computation context.
176+For example, ``Control.ST`` defines a ``ConsoleIO`` interface which
177+provides the necessary methods for performing basic console interaction:
178+
179+.. code-block:: idris
180+
181+ interface ConsoleIO (m : Type -> Type) where
182+ putStr : String -> STrans m () res (const res)
183+ getStr : STrans m String res (const res)
184+
185+That is, we can write to and read from the console with any available
186+resources ``res``, and neither will affect the available resources.
187+This has the following implementation for ``IO``:
188+
189+.. code-block:: idris
190+
191+ ConsoleIO IO where
192+ putStr str = lift (Interactive.putStr str)
193+ getStr = lift Interactive.getLine
194+
195+Now, we can define ``ioMakeAndIncrement`` as follows:
196+
197+.. code-block:: idris
198+
199+ ioMakeAndIncrement : ConsoleIO io => STrans io () [] (const [])
200+ ioMakeAndIncrement
201+ = do putStr "Enter a number: "
202+ init <- getStr
203+ var <- new (cast init)
204+ putStrLn ("var = " ++ show !(read var))
205+ increment var
206+ putStrLn ("var = " ++ show !(read var))
207+ delete var
208+
209+Instead of working in ``IO`` specifically, this works in a generic context
210+``io``, provided that there is an implementation of ``ConsoleIO`` for that
211+context. This has several advantages over the first version:
212+
213+* All of the calls to ``lift`` are in the implementation of the interface,
214+ rather than ``ioMakeAndIncrement``
215+* We can provide alternative implementations of ``ConsoleIO``, perhaps
216+ supporting exceptions or logging in addition to basic I/O.
217+* As we'll see in the next section (:ref:`smstypes`), it will allow us to
218+ define safe APIs for manipulating specific resources more precisely.
219+
220+Earlier, we used ``runPure`` to run ``makeAndIncrement`` in the identity
221+context. Here, we use ``run``, which allows us to execute an ``STrans`` program
222+in any context (as long as it has an implementation of ``Applicative``) and we
223+can execute ``ioMakeAndIncrement`` at the REPL as follows:
224+
225+.. code::
226+
227+ *Intro> :exec run ioMakeAndIncrement
228+ Enter a number: 93
229+ var = 93
230+ var = 94
231+
232+Manipulating ``State`` with dependent types
233+===========================================
234+
235+In our first example of ``State``, when we incremented the value its
236+*type* remained the same. However, when we're working with
237+*dependent* types, updating a state may also involve updating its type.
238+For example, if we're adding an element to a vector stored in a state,
239+its length will change:
240+
241+.. code-block:: idris
242+
243+ addElement : (vec : Var) -> (item : a) ->
244+ STrans m () [vec ::: State (Vect n a)]
245+ (const [vec ::: State (Vect (S n) a)])
246+ addElement vec item = do xs <- read vec
247+ write vec (item :: xs)
248+
249+Note that you'll need to ``import Data.Vect`` to try this example.
250+
251+.. topic:: Updating a state directly with ``update``
252+
253+ Rather than using ``read`` and ``write`` separately, you can also
254+ use ``update`` which reads from a ``State``, applies a function to it,
255+ then writes the result. Using ``update`` you could write ``addElement``
256+ as follows:
257+
258+ .. code-block:: idris
259+
260+ addElement : (vec : Var) -> (item : a) ->
261+ STrans m () [vec ::: State (Vect n a)]
262+ (const [vec ::: State (Vect (S n) a)])
263+ addElement vec item = update vec (item ::)
264+
265+We don't always know *how* exactly the type will change in the course of a
266+sequence actions, however. For example, if we have a state containing a
267+vector of integers, we might read an input from the console and only add it
268+to the vector if the input is a valid integer. Somehow, we need a different
269+type for the output state depending on whether reading the integer was
270+successful, so neither of the following types is quite right:
271+
272+.. code-block:: idris
273+
274+ readAndAdd_OK : ConsoleIO io => (vec : Var) ->
275+ STrans m () -- Returns an empty tuple
276+ [vec ::: State (Vect n Integer)]
277+ (const [vec ::: State (Vect (S n) Integer)])
278+ readAndAdd_Fail : ConsoleIO io => (vec : Var) ->
279+ STrans m () -- Returns an empty tuple
280+ [vec ::: State (Vect n Integer)]
281+ (const [vec ::: State (Vect n Integer)])
282+
283+Remember, though, that the *output* resource types can be *computed* from
284+the result of a function. So far, we've used ``const`` to note that the
285+output resources are always the same, but here, instead, we can use a type
286+level function to *calculate* the output resources. We start by returning
287+a ``Bool`` instead of an empty tuple, which is ``True`` if reading the input
288+was successful, and leave a *hole* for the output resources:
289+
290+.. code-block:: idris
291+
292+ readAndAdd : ConsoleIO io => (vec : Var) ->
293+ STrans m Bool [vec ::: State (Vect n Integer)]
294+ ?output_res
295+
296+If you check the type of ``?output_res``, you'll see that Idris expects
297+a function of type ``Bool -> Resources``, meaning that the output resource
298+type can be different depending on the result of ``readAndAdd``:
299+
300+.. code-block:: idris
301+
302+ n : Nat
303+ m : Type -> Type
304+ io : Type -> Type
305+ constraint : ConsoleIO io
306+ vec : Var
307+ --------------------------------------
308+ output_res : Bool -> Resources
309+
310+So, the output resource is either a ``Vect n Integer`` if the input is
311+invalid (i.e. ``readAndAdd`` returns ``False``) or a ``Vect (S n) Integer``
312+if the input is valid. We can express this in the type as follows:
313+
314+.. code-block:: idris
315+
316+ readAndAdd : ConsoleIO io => (vec : Var) ->
317+ STrans io Bool [vec ::: State (Vect n Integer)]
318+ (\res => [vec ::: State (if res then Vect (S n) Integer
319+ else Vect n Integer)])
320+
321+Then, when we implement ``readAndAdd`` we need to return the appropriate
322+value for the output state. If we've added an item to the vector, we need to
323+return ``True``, otherwise we need to return ``False``:
324+
325+.. code-block:: idris
326+
327+ readAndAdd : ConsoleIO io => (vec : Var) ->
328+ STrans io Bool [vec ::: State (Vect n Integer)]
329+ (\res => [vec ::: State (if res then Vect (S n) Integer
330+ else Vect n Integer)])
331+ readAndAdd vec = do putStr "Enter a number: "
332+ num <- getStr
333+ if all isDigit (unpack num)
334+ then do
335+ update vec ((cast num) ::)
336+ pure True -- added an item, so return True
337+ else pure False -- didn't add, so return False
338+
339+There is a slight difficulty if we're developing interactively, which is
340+that if we leave a hole, the required output state isn't easily visible
341+until we know the value that's being returning. For example. in the following
342+incomplete definition of ``readAndAdd`` we've left a hole for the
343+successful case:
344+
345+.. code-block:: idris
346+
347+ readAndAdd vec = do putStr "Enter a number: "
348+ num <- getStr
349+ if all isDigit (unpack num)
350+ then ?whatNow
351+ else pure False
352+
353+We can look at the type of ``?whatNow``, but it is unforunately rather less
354+than informative:
355+
356+.. code-block:: idris
357+
358+ vec : Var
359+ n : Nat
360+ io : Type -> Type
361+ constraint : ConsoleIO io
362+ num : String
363+ --------------------------------------
364+ whatNow : STrans io Bool [vec ::: State (Vect (S n) Integer)]
365+ (\res =>
366+ [vec :::
367+ State (ifThenElse res
368+ (Delay (Vect (S n) Integer))
369+ (Delay (Vect n Integer)))])
370+
371+The problem is that we'll only know the required output state when we know
372+the value we're returning. To help with interactive development, ``Control.ST``
373+provides a function ``returning`` which allows us to specify the return
374+value up front, and to update the state accordingly. For example, we can
375+write an incomplete ``readAndAdd`` as follows:
376+
377+.. code-block:: idris
378+
379+ readAndAdd vec = do putStr "Enter a number: "
380+ num <- getStr
381+ if all isDigit (unpack num)
382+ then returning True ?whatNow
383+ else pure False
384+
385+This states that, in the successful branch, we'll be returning ``True``, and
386+``?whatNow`` should explain how to update the states appropriately so that
387+they are correct for a return value of ``True``. We can see this by checking
388+the type of ``?whatNow``, which is now a little more informative:
389+
390+.. code-block:: idris
391+
392+ vec : Var
393+ n : Nat
394+ io : Type -> Type
395+ constraint : ConsoleIO io
396+ num : String
397+ --------------------------------------
398+ whatnow : STrans io () [vec ::: State (Vect n Integer)]
399+ (\value => [vec ::: State (Vect (S n) Integer)])
400+
401+This type now shows, in the output resource list of ``STrans``,
402+that we can complete the definition by adding an item to ``vec``, which
403+we can do as follows:
404+
405+.. code-block:: idris
406+
407+ readAndAdd vec = do putStr "Enter a number: "
408+ num <- getStr
409+ if all isDigit (unpack num)
410+ then returning True (update vec ((cast num) ::))
411+ else returning False (pure ()) -- returning False, so no state update required
412+
413+.. _stransprimops:
414+
415+``STrans`` Primitive operations
416+===============================
417+
418+Now that we've written a few small examples of ``STrans`` functions, it's
419+a good time to look more closely at the types of the state manipulation
420+functions we've used. First, to read and write states, we've used
421+``read`` and ``write``:
422+
423+.. code-block:: idris
424+
425+ read : (lbl : Var) -> {auto prf : InState lbl (State ty) res} ->
426+ STrans m ty res (const res)
427+ write : (lbl : Var) -> {auto prf : InState lbl ty res} ->
428+ (val : ty') ->
429+ STrans m () res (const (updateRes res prf (State ty')))
430+
431+These types may look a little daunting at first, particularly due to the
432+implicit ``prf`` argument, which has the following type:
433+
434+.. code-block:: idris
435+
436+ prf : InState lbl (State ty) res}
437+
438+This relies on a predicate ``InState``. A value of type ``InState x ty res``
439+means that the reference ``x`` must have type ``ty`` in the list of
440+resources ``res``. So, in practice, all this type means is that we can
441+only read or write a resource if a reference to it exists in the list of
442+resources.
443+
444+Given a resource label ``res``, and a proof that ``res`` exists in a list
445+of resources, ``updateRes`` will update the type of that resource. So,
446+the type of ``write`` states that the type of the resource will be updated
447+to the type of the given value.
448+
449+The type of ``update`` is similar to that for ``read`` and ``write``, requiring
450+that the resource has the input type of the given function, and updating it to
451+have the output type of the function:
452+
453+.. code-block:: idris
454+
455+ update : (lbl : Var) -> {auto prf : InState lbl (State ty) res} ->
456+ (ty -> ty') ->
457+ STrans m () res (const (updateRes res prf (State ty')))
458+
459+The type of ``new`` states that it returns a ``Var``, and given an initial
460+value of type ``state``, the output resources contains a new resource
461+of type ``State state``:
462+
463+.. code-block:: idris
464+
465+ new : (val : state) ->
466+ STrans m Var res (\lbl => (lbl ::: State state) :: res)
467+
468+It's important that the new resource has type ``State state``, rather than
469+merely ``state``, because this will allow us to hide implementation details
470+of APIs. We'll see more about what this means in the next section,
471+:ref:`smstypes`.
472+
473+The type of ``delete`` states that the given label will be removed from
474+the list of resources, given an implicit proof that the label exists in
475+the input resources:
476+
477+.. code-block:: idris
478+
479+ delete : (lbl : Var) -> {auto prf : InState lbl (State st) res} ->
480+ STrans m () res (const (drop res prf))
481+
482+Here, ``drop`` is a type level function which updates the resource list,
483+removing the given resource ``lbl`` from the list.
484+
485+We've used ``lift`` to run functions in the underlying context. It has the
486+following type:
487+
488+.. code-block:: idris
489+
490+ lift : Monad m => m t -> STrans m t res (const res)
491+
492+Given a ``result`` value, ``pure`` is an ``STrans`` program which produces
493+that value, provided that the current list of resources is correct when
494+producing that value:
495+
496+.. code-block:: idris
497+
498+ pure : (result : ty) -> STrans m ty (out_fn result) out_fn
499+
500+We can use ``returning`` to break down returning a value from an
501+``STrans`` functions into two parts: providing the value itself, and updating
502+the resource list so that it is appropriate for returning that value:
503+
504+.. code-block:: idris
505+
506+ returning : (result : ty) ->
507+ STrans m () res (const (out_fn result)) ->
508+ STrans m ty res out_fn
509+
510+Finally, we've used ``run`` and ``runPure`` to execute ``STrans`` functions
511+in a specific context. ``run`` will execute a function in any context,
512+provided that there is an ``Applicative`` implementation for that context,
513+and ``runPure`` will execute a function in the identity context:
514+
515+.. code-block:: idris
516+
517+ run : Applicative m => STrans m a [] (const []) -> m a
518+ runPure : STrans Basics.id a [] (const []) -> a
519+
520+Note that in each case, the input and output resource list must be empty.
521+There's no way to provide an initial resource list, or extract the final
522+resources. This is deliberate: it ensures that *all* resource management is
523+carried out in the controlled ``STrans`` environment and, as we'll see, this
524+allows us to implement safe APIs with precise types explaining exactly how
525+resources are tracked throughout a program.
526+
527+These functions provide the core of the ``ST`` library; there are some
528+others which we'll encounter later, for more advanced situations, but the
529+functions we have seen so far already allow quite sophisticated state-aware
530+programming and reasoning in Idris.
531+
532+.. _sttype:
533+
534+`ST`: Representing state transitions directly
535+============================================
536+
537+We've seen a few examples of small ``STrans`` functions now, and
538+their types can become quite verbose given that we need to provide explicit
539+input and output resource lists. This is convenient for giving types for
540+the primitive operations, but for more general use it's much more convenient
541+to be able to express *transitions* on individual resources, rather than
542+given input and output resource lists in full. We can do this with
543+``ST``:
544+
545+.. code-block:: idris
546+
547+ ST : (m : Type -> Type) ->
548+ (resultType : Type) ->
549+ List (Action resultType) -> Type
550+
551+``ST`` is a type level function which computes an appropriate ``STrans``
552+type given a list of *actions*, which describe transitions on resources.
553+An ``Action`` in a function type can take one of the following forms:
554+
555+* ``lbl ::: ty`` expresses that the resource ``lbl`` begins and ends in
556+ the state ``ty``
557+* ``lbl ::: ty_in :-> ty_out`` expresses that the resource ``lbl`` begins
558+ in state ``ty_in`` and ends in state ``ty_out``
559+* ``lbl ::: ty_in :-> (\res -> ty_out)`` expresses that the resource ``lbl``
560+ begins in state ``ty_in`` and ends in a state ``ty_out``, where ``ty_out``
561+ is computed from the result of the function ``res``.
562+
563+So, we can write some of the function types we've seen so far as follows:
564+
565+.. code-block:: idris
566+
567+ increment : (x : Var) -> ST m () [x ::: State Integer]
568+
569+That is, ``increment`` begins and ends with ``x`` in state ``State Integer``.
570+
571+.. code-block:: idris
572+
573+ makeAndIncrement : Int -> ST m Int []
574+
575+That is, ``makeAndIncrement`` begins and ends with no resources.
576+
577+.. code-block:: idris
578+
579+ addElement : (vec : Var) -> (item : a) ->
580+ ST m () [vec ::: State (Vect n a) :-> State (Vect (S n) a)]
581+
582+That is, ``addElement`` changes ``vec`` from ``State (Vect n a)`` to
583+``State (Vect (S n) a)``.
584+
585+.. code-block:: idris
586+
587+ readAndAdd : ConsoleIO io => (vec : Var) ->
588+ ST io Bool
589+ [vec ::: State (Vect n Integer) :->
590+ \res => State (if res then Vect (S n) Integer
591+ else Vect n Integer)]
592+
593+By writing the types in this way, we express the minimum necessary to explain
594+how each function affects the overall resource state. If there is a resource
595+update depending on a result, as with ``readAndAdd``, then we need to describe
596+it in full. Otherwise, as with ``increment`` and ``makeAndIncrement``, we can
597+write the input and output resource lists without repetition.
598+
599+In the remainder of this tutorial, we will generally use ``ST`` except on
600+the rare occasions we need the full precision of ``STrans``. In the next
601+section, we'll see how to use the facilities provided by ``ST`` to write
602+a precise API for a system with security properties: a data store requiring
603+a login.
604+
605+