3**********************************
4Introducing ST: Working with State
5**********************************
7The ``Control.ST`` library provides facilities for creating, reading, writing
8and destroying state in Idris functions, and tracking changes of state in
9a function's type. It is based around the concept of *resources*, which are,
10essentially, mutable variables, and a dependent type, ``STrans`` which tracks
11how those resources change when a function runs:
15 STrans : (m : Type -> Type) ->
16 (resultType : Type) ->
17 (in_res : Resources) ->
18 (out_res : resultType -> Resources) ->
21A value of type ``STrans m resultType in_res out_res_fn`` represents a sequence
22of actions which can manipulate state. The arguments are:
24* ``m``, which is an underlying *computation context* in which the actions will be executed.
25 Usually, this will be a generic type with a ``Monad`` implementation, but
26 it isn't necessarily so. In particular, there is no need to understand monads
27 to be able to use ``ST`` effectively!
28* ``resultType``, which is the type of the value the sequence will produce
29* ``in_res``, which is a list of *resources* available *before* executing the actions.
30* ``out_res``, which is a list of resources available *after* executing the actions,
31 and may differ depending on the result of the actions.
33We can use ``STrans`` to describe *state transition systems* in a function's
34type. We'll come to the definition of ``Resources`` shortly, but for the moment
35you can consider it an abstract representation of the "state of the world".
36By giving the input resources (``in_res``) and the output resources
37(``out_res``) we are describing the *preconditions* under which a function
38is allowed to execute, and *postconditions* which describe how a function
39affects the overall state of the world.
41We'll begin in this section by looking at some small examples of ``STrans``
42functions, and see how to execute them. We'll also introduce ``ST``,
43a type-level function which allows us to describe the state transitions of
44a stateful function concisely.
46.. topic:: Type checking the examples
48 For the examples in this section, and throughout this tutorial,
49 you'll need to ``import Control.ST`` and add the ``contrib`` package by
50 passing the ``-p contrib`` flag to ``idris``.
53Introductory examples: manipulating ``State``
54=============================================
56An ``STrans`` function explains, in its type, how it affects a collection of
57``Resources``. A resource has a *label* (of type ``Var``), which we use to
58refer to the resource throughout the function, and we write the state of a
59resource, in the ``Resources`` list, in the form ``label ::: type``.
61For example, the following function
62has a resource ``x`` available on input, of type ``State Integer``, and that
63resource is still a ``State Integer`` on output:
67 increment : (x : Var) -> STrans m () [x ::: State Integer]
68 (const [x ::: State Integer])
69 increment x = do num <- read x
72.. sidebar:: Verbosity of the type of ``increment``
74 The type of ``increment`` may seem somewhat verbose, in that the
75 *input* and *output* resources are repeated, even though they are the
76 same. We'll introduce a much more concise way of writing this type at the
77 end of this section (:ref:`sttype`), when we describe the ``ST`` type
80This function reads the value stored at the resource ``x`` with ``read``,
81increments it then writes the result back into the resource ``x`` with
82``write``. We'll see the types of ``read`` and ``write`` shortly
83(see :ref:`stransprimops`). We can also create and delete resources:
87 makeAndIncrement : Integer -> STrans m Integer [] (const [])
88 makeAndIncrement init = do var <- new init
94The type of ``makeAndIncrement`` states that it has *no* resources available on
95entry (``[]``) or exit (``const []``). It creates a new ``State`` resource with
96``new`` (which takes an initial value for the resource), increments the value,
97reads it back, then deletes it using ``delete``, returning the final value
98of the resource. Again, we'll see the types of ``new`` and ``delete``
101The ``m`` argument to ``STrans`` (of type ``Type -> Type``) is the *computation context* in
102which the function can be run. Here, the type level variable indicates that we
103can run it in *any* context. We can run it in the identity context with
104``runPure``. For example, try entering the above definitions in a file
105``Intro.idr`` then running the following at the REPL:
109 *Intro> runPure (makeAndIncrement 93)
112It's a good idea to take an interactive, type-driven approach to implementing
113``STrans`` programs. For example, after creating the resource with ``new init``,
114you can leave a *hole* for the rest of the program to see how creating the
115resource has affected the type:
119 makeAndIncrement : Integer -> STrans m Integer [] (const [])
120 makeAndIncrement init = do var <- new init
123If you check the type of ``?whatNext``, you'll see that there is now
124a resource available, ``var``, and that by the end of the function there
125should be no resource available:
132 --------------------------------------
133 whatNext : STrans m Integer [var ::: State Integer] (\value => [])
135These small examples work in any computation context ``m``. However, usually,
136we are working in a more restricted context. For example, we might want to
137write programs which only work in a context that supports interactive
138programs. For this, we'll need to see how to *lift* operations from the
141Lifting: Using the computation context
142======================================
144Let's say that, instead of passing an initial integer to ``makeAndIncrement``,
145we want to read it in from the console. Then, instead of working in a generic
146context ``m``, we can work in the specific context ``IO``:
150 ioMakeAndIncrement : STrans IO () [] (const [])
152This gives us access to ``IO`` operations, via the ``lift`` function. We
153can define ``ioMakeAndIncrement`` as follows:
157 ioMakeAndIncrement : STrans IO () [] (const [])
159 = do lift $ putStr "Enter a number: "
160 init <- lift $ getLine
161 var <- new (cast init)
162 lift $ putStrLn ("var = " ++ show !(read var))
164 lift $ putStrLn ("var = " ++ show !(read var))
167The ``lift`` function allows us to use funtions from the underlying
168computation context (``IO`` here) directly. Again, we'll see the exact type
173 In ``ioMakeAndIncrement`` we've used ``!(read var)`` to read from the
174 resource. You can read about this ``!``-notation in the main Idris tutorial
175 (see :ref:`monadsdo`). In short, it allows us to use an ``STrans``
176 function inline, rather than having to bind the result to a variable
179 Conceptually, at least, you can think of it as having the following type:
181 .. code-block:: idris
183 (!) : STrans m a state_in state_out -> a
185 It is syntactic sugar for binding a variable immediately before the
186 current action in a ``do`` block, then using that variable in place of
187 the ``!``-expression.
190In general, though, it's bad practice to use a *specific* context like
191``IO``. Firstly, it requires us to sprinkle ``lift`` liberally throughout
192our code, which hinders readability. Secondly, and more importantly, it will
193limit the safety of our functions, as we'll see in the next section
196So, instead, we define *interfaces* to restrict the computation context.
197For example, ``Control.ST`` defines a ``ConsoleIO`` interface which
198provides the necessary methods for performing basic console interaction:
202 interface ConsoleIO (m : Type -> Type) where
203 putStr : String -> STrans m () res (const res)
204 getStr : STrans m String res (const res)
206That is, we can write to and read from the console with any available
207resources ``res``, and neither will affect the available resources.
208This has the following implementation for ``IO``:
213 putStr str = lift (Interactive.putStr str)
214 getStr = lift Interactive.getLine
216Now, we can define ``ioMakeAndIncrement`` as follows:
220 ioMakeAndIncrement : ConsoleIO io => STrans io () [] (const [])
222 = do putStr "Enter a number: "
224 var <- new (cast init)
225 putStrLn ("var = " ++ show !(read var))
227 putStrLn ("var = " ++ show !(read var))
230Instead of working in ``IO`` specifically, this works in a generic context
231``io``, provided that there is an implementation of ``ConsoleIO`` for that
232context. This has several advantages over the first version:
234* All of the calls to ``lift`` are in the implementation of the interface,
235 rather than ``ioMakeAndIncrement``
236* We can provide alternative implementations of ``ConsoleIO``, perhaps
237 supporting exceptions or logging in addition to basic I/O.
238* As we'll see in the next section (:ref:`smstypes`), it will allow us to
239 define safe APIs for manipulating specific resources more precisely.
241Earlier, we used ``runPure`` to run ``makeAndIncrement`` in the identity
242context. Here, we use ``run``, which allows us to execute an ``STrans`` program
243in any context (as long as it has an implementation of ``Applicative``) and we
244can execute ``ioMakeAndIncrement`` at the REPL as follows:
248 *Intro> :exec run ioMakeAndIncrement
255Manipulating ``State`` with dependent types
256===========================================
258In our first example of ``State``, when we incremented the value its
259*type* remained the same. However, when we're working with
260*dependent* types, updating a state may also involve updating its type.
261For example, if we're adding an element to a vector stored in a state,
262its length will change:
266 addElement : (vec : Var) -> (item : a) ->
267 STrans m () [vec ::: State (Vect n a)]
268 (const [vec ::: State (Vect (S n) a)])
269 addElement vec item = do xs <- read vec
270 write vec (item :: xs)
272Note that you'll need to ``import Data.Vect`` to try this example.
274.. topic:: Updating a state directly with ``update``
276 Rather than using ``read`` and ``write`` separately, you can also
277 use ``update`` which reads from a ``State``, applies a function to it,
278 then writes the result. Using ``update`` you could write ``addElement``
281 .. code-block:: idris
283 addElement : (vec : Var) -> (item : a) ->
284 STrans m () [vec ::: State (Vect n a)]
285 (const [vec ::: State (Vect (S n) a)])
286 addElement vec item = update vec (item ::)
288We don't always know *how* exactly the type will change in the course of a
289sequence actions, however. For example, if we have a state containing a
290vector of integers, we might read an input from the console and only add it
291to the vector if the input is a valid integer. Somehow, we need a different
292type for the output state depending on whether reading the integer was
293successful, so neither of the following types is quite right:
297 readAndAdd_OK : ConsoleIO io => (vec : Var) ->
298 STrans m () -- Returns an empty tuple
299 [vec ::: State (Vect n Integer)]
300 (const [vec ::: State (Vect (S n) Integer)])
301 readAndAdd_Fail : ConsoleIO io => (vec : Var) ->
302 STrans m () -- Returns an empty tuple
303 [vec ::: State (Vect n Integer)]
304 (const [vec ::: State (Vect n Integer)])
306Remember, though, that the *output* resource types can be *computed* from
307the result of a function. So far, we've used ``const`` to note that the
308output resources are always the same, but here, instead, we can use a type
309level function to *calculate* the output resources. We start by returning
310a ``Bool`` instead of an empty tuple, which is ``True`` if reading the input
311was successful, and leave a *hole* for the output resources:
315 readAndAdd : ConsoleIO io => (vec : Var) ->
316 STrans m Bool [vec ::: State (Vect n Integer)]
319If you check the type of ``?output_res``, you'll see that Idris expects
320a function of type ``Bool -> Resources``, meaning that the output resource
321type can be different depending on the result of ``readAndAdd``:
328 constraint : ConsoleIO io
330 --------------------------------------
331 output_res : Bool -> Resources
333So, the output resource is either a ``Vect n Integer`` if the input is
334invalid (i.e. ``readAndAdd`` returns ``False``) or a ``Vect (S n) Integer``
335if the input is valid. We can express this in the type as follows:
339 readAndAdd : ConsoleIO io => (vec : Var) ->
340 STrans io Bool [vec ::: State (Vect n Integer)]
341 (\res => [vec ::: State (if res then Vect (S n) Integer
342 else Vect n Integer)])
344Then, when we implement ``readAndAdd`` we need to return the appropriate
345value for the output state. If we've added an item to the vector, we need to
346return ``True``, otherwise we need to return ``False``:
350 readAndAdd : ConsoleIO io => (vec : Var) ->
351 STrans io Bool [vec ::: State (Vect n Integer)]
352 (\res => [vec ::: State (if res then Vect (S n) Integer
353 else Vect n Integer)])
354 readAndAdd vec = do putStr "Enter a number: "
356 if all isDigit (unpack num)
358 update vec ((cast num) ::)
359 pure True -- added an item, so return True
360 else pure False -- didn't add, so return False
362There is a slight difficulty if we're developing interactively, which is
363that if we leave a hole, the required output state isn't easily visible
364until we know the value that's being returned. For example. in the following
365incomplete definition of ``readAndAdd`` we've left a hole for the
370 readAndAdd vec = do putStr "Enter a number: "
372 if all isDigit (unpack num)
376We can look at the type of ``?whatNow``, but it is unfortunately rather less
384 constraint : ConsoleIO io
386 --------------------------------------
387 whatNow : STrans io Bool [vec ::: State (Vect (S n) Integer)]
390 State (ifThenElse res
391 (Delay (Vect (S n) Integer))
392 (Delay (Vect n Integer)))])
394The problem is that we'll only know the required output state when we know
395the value we're returning. To help with interactive development, ``Control.ST``
396provides a function ``returning`` which allows us to specify the return
397value up front, and to update the state accordingly. For example, we can
398write an incomplete ``readAndAdd`` as follows:
402 readAndAdd vec = do putStr "Enter a number: "
404 if all isDigit (unpack num)
405 then returning True ?whatNow
408This states that, in the successful branch, we'll be returning ``True``, and
409``?whatNow`` should explain how to update the states appropriately so that
410they are correct for a return value of ``True``. We can see this by checking
411the type of ``?whatNow``, which is now a little more informative:
418 constraint : ConsoleIO io
420 --------------------------------------
421 whatnow : STrans io () [vec ::: State (Vect n Integer)]
422 (\value => [vec ::: State (Vect (S n) Integer)])
424This type now shows, in the output resource list of ``STrans``,
425that we can complete the definition by adding an item to ``vec``, which
430 readAndAdd vec = do putStr "Enter a number: "
432 if all isDigit (unpack num)
433 then returning True (update vec ((cast num) ::))
434 else returning False (pure ()) -- returning False, so no state update required
438``STrans`` Primitive operations
439===============================
441Now that we've written a few small examples of ``STrans`` functions, it's
442a good time to look more closely at the types of the state manipulation
443functions we've used. First, to read and write states, we've used
444``read`` and ``write``:
448 read : (lbl : Var) -> {auto prf : InState lbl (State ty) res} ->
449 STrans m ty res (const res)
450 write : (lbl : Var) -> {auto prf : InState lbl ty res} ->
452 STrans m () res (const (updateRes res prf (State ty')))
454These types may look a little daunting at first, particularly due to the
455implicit ``prf`` argument, which has the following type:
459 prf : InState lbl (State ty) res}
461This relies on a predicate ``InState``. A value of type ``InState x ty res``
462means that the reference ``x`` must have type ``ty`` in the list of
463resources ``res``. So, in practice, all this type means is that we can
464only read or write a resource if a reference to it exists in the list of
467Given a resource label ``res``, and a proof that ``res`` exists in a list
468of resources, ``updateRes`` will update the type of that resource. So,
469the type of ``write`` states that the type of the resource will be updated
470to the type of the given value.
472The type of ``update`` is similar to that for ``read`` and ``write``, requiring
473that the resource has the input type of the given function, and updating it to
474have the output type of the function:
478 update : (lbl : Var) -> {auto prf : InState lbl (State ty) res} ->
480 STrans m () res (const (updateRes res prf (State ty')))
482The type of ``new`` states that it returns a ``Var``, and given an initial
483value of type ``state``, the output resources contains a new resource
484of type ``State state``:
488 new : (val : state) ->
489 STrans m Var res (\lbl => (lbl ::: State state) :: res)
491It's important that the new resource has type ``State state``, rather than
492merely ``state``, because this will allow us to hide implementation details
493of APIs. We'll see more about what this means in the next section,
496The type of ``delete`` states that the given label will be removed from
497the list of resources, given an implicit proof that the label exists in
502 delete : (lbl : Var) -> {auto prf : InState lbl (State st) res} ->
503 STrans m () res (const (drop res prf))
505Here, ``drop`` is a type level function which updates the resource list,
506removing the given resource ``lbl`` from the list.
508We've used ``lift`` to run functions in the underlying context. It has the
513 lift : Monad m => m t -> STrans m t res (const res)
515Given a ``result`` value, ``pure`` is an ``STrans`` program which produces
516that value, provided that the current list of resources is correct when
521 pure : (result : ty) -> STrans m ty (out_fn result) out_fn
523We can use ``returning`` to break down returning a value from an
524``STrans`` functions into two parts: providing the value itself, and updating
525the resource list so that it is appropriate for returning that value:
529 returning : (result : ty) ->
530 STrans m () res (const (out_fn result)) ->
531 STrans m ty res out_fn
533Finally, we've used ``run`` and ``runPure`` to execute ``STrans`` functions
534in a specific context. ``run`` will execute a function in any context,
535provided that there is an ``Applicative`` implementation for that context,
536and ``runPure`` will execute a function in the identity context:
540 run : Applicative m => STrans m a [] (const []) -> m a
541 runPure : STrans Basics.id a [] (const []) -> a
543Note that in each case, the input and output resource list must be empty.
544There's no way to provide an initial resource list, or extract the final
545resources. This is deliberate: it ensures that *all* resource management is
546carried out in the controlled ``STrans`` environment and, as we'll see, this
547allows us to implement safe APIs with precise types explaining exactly how
548resources are tracked throughout a program.
550These functions provide the core of the ``ST`` library; there are some
551others which we'll encounter later, for more advanced situations, but the
552functions we have seen so far already allow quite sophisticated state-aware
553programming and reasoning in Idris.
557`ST`: Representing state transitions directly
558============================================
560We've seen a few examples of small ``STrans`` functions now, and
561their types can become quite verbose given that we need to provide explicit
562input and output resource lists. This is convenient for giving types for
563the primitive operations, but for more general use it's much more convenient
564to be able to express *transitions* on individual resources, rather than
565giving input and output resource lists in full. We can do this with
570 ST : (m : Type -> Type) ->
571 (resultType : Type) ->
572 List (Action resultType) -> Type
574``ST`` is a type level function which computes an appropriate ``STrans``
575type given a list of *actions*, which describe transitions on resources.
576An ``Action`` in a function type can take one of the following forms (plus
577some others which we'll see later in the tutorial):
579* ``lbl ::: ty`` expresses that the resource ``lbl`` begins and ends in
581* ``lbl ::: ty_in :-> ty_out`` expresses that the resource ``lbl`` begins
582 in state ``ty_in`` and ends in state ``ty_out``
583* ``lbl ::: ty_in :-> (\res -> ty_out)`` expresses that the resource ``lbl``
584 begins in state ``ty_in`` and ends in a state ``ty_out``, where ``ty_out``
585 is computed from the result of the function ``res``.
587So, we can write some of the function types we've seen so far as follows:
591 increment : (x : Var) -> ST m () [x ::: State Integer]
593That is, ``increment`` begins and ends with ``x`` in state ``State Integer``.
597 makeAndIncrement : Int -> ST m Int []
599That is, ``makeAndIncrement`` begins and ends with no resources.
603 addElement : (vec : Var) -> (item : a) ->
604 ST m () [vec ::: State (Vect n a) :-> State (Vect (S n) a)]
606That is, ``addElement`` changes ``vec`` from ``State (Vect n a)`` to
607``State (Vect (S n) a)``.
611 readAndAdd : ConsoleIO io => (vec : Var) ->
613 [vec ::: State (Vect n Integer) :->
614 \res => State (if res then Vect (S n) Integer
615 else Vect n Integer)]
617By writing the types in this way, we express the minimum necessary to explain
618how each function affects the overall resource state. If there is a resource
619update depending on a result, as with ``readAndAdd``, then we need to describe
620it in full. Otherwise, as with ``increment`` and ``makeAndIncrement``, we can
621write the input and output resource lists without repetition.
623An ``Action`` can also describe *adding* and *removing* states:
625* ``add ty``, assuming the operation returns a ``Var``, adds a new resource
627* ``remove lbl ty`` expresses that the operation removes the resource named
628 ``lbl``, beginning in state ``ty`` from the resource list.
630So, for example, we can write:
634 newState : ST m Var [add (State Int)]
635 removeState : (lbl : Var) -> ST m () [remove lbl (State Int)]
637The first of these, ``newState``, returns a new resource label, and adds that
638resource to the list with type ``State Int``. The second, ``removeState``,
639given a label ``lbl``, removes the resource from the list. These types are
640equivalent to the following:
644 newState : STrans m Var [] (\lbl => [lbl ::: State Int])
645 removeState : (lbl : Var) -> STrans m () [lbl ::: State Int] (const [])
647These are the primitive methods of constructing an ``Action``. Later, we will
648encounter some other ways using type level functions to help with readability.
650In the remainder of this tutorial, we will generally use ``ST`` except on
651the rare occasions we need the full precision of ``STrans``. In the next
652section, we'll see how to use the facilities provided by ``ST`` to write
653a precise API for a system with security properties: a data store requiring
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list