@@ -19,10 +19,10 @@ how those resources change when a function runs:
21A value of type ``STrans m resultType in_res out_res_fn`` represents a sequence
21A value of type ``STrans m resultType in_res out_res_fn`` represents a sequence
22−of actions which can manipulate state. The arguments are:
22+of actions which can manipulate state. The arguments are:
24* ``m``, which is an underlying *computation context* in which the actions will be executed.
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
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
26 it isn't necessarily so. In particular, there is no need to understand monads
27 to be able to use ``ST`` effectively!
27 to be able to use ``ST`` effectively!
28* ``resultType``, which is the type of the value the sequence will produce
28* ``resultType``, which is the type of the value the sequence will produce
@@ -76,10 +76,10 @@ resource is still a ``State Integer`` on output:
76 same. We'll introduce a much more concise way of writing this type at 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
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``,
80This function reads the value stored at the resource ``x`` with ``read``,
81increments it then writes the result back into the resource ``x`` with
81increments it then writes the result back into the resource ``x`` with
82−``write``. We'll see the types of ``read`` and ``write`` shortly
82+``write``. We'll see the types of ``read`` and ``write`` shortly
83(see :ref:`stransprimops`). We can also create and delete resources:
83(see :ref:`stransprimops`). We can also create and delete resources:
85.. code-block:: idris
85.. code-block:: idris
@@ -104,7 +104,7 @@ can 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
104``runPure``. For example, try entering the above definitions in a file
105``Intro.idr`` then running the following at the REPL:
105``Intro.idr`` then running the following at the REPL:
107−.. code::
107+.. code::
109 *Intro> runPure (makeAndIncrement 93)
109 *Intro> runPure (makeAndIncrement 93)
110 94 : Integer
110 94 : Integer
@@ -179,7 +179,7 @@ of ``lift`` shortly.
179 Conceptually, at least, you can think of it as having the following type:
179 Conceptually, at least, you can think of it as having the following type:
181 .. code-block:: idris
181 .. code-block:: idris
183 (!) : STrans m a state_in state_out -> a
183 (!) : STrans m a state_in state_out -> a
185 It is syntactic sugar for binding a variable immediately before the
185 It is syntactic sugar for binding a variable immediately before the
@@ -243,7 +243,7 @@ context. 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
243in any context (as long as it has an implementation of ``Applicative``) and we
244can execute ``ioMakeAndIncrement`` at the REPL as follows:
244can execute ``ioMakeAndIncrement`` at the REPL as follows:
246−.. code::
246+.. code::
248 *Intro> :exec run ioMakeAndIncrement
248 *Intro> :exec run ioMakeAndIncrement
249 Enter a number: 93
249 Enter a number: 93
@@ -269,7 +269,7 @@ its length will change:
269 addElement vec item = do xs <- read vec
269 addElement vec item = do xs <- read vec
270 write vec (item :: xs)
270 write vec (item :: xs)
272−Note that you'll need to ``import Data.Vect`` to try this example.
272+Note that you'll need to ``import Data.Vect`` to try this example.
274.. topic:: Updating a state directly with ``update``
274.. topic:: Updating a state directly with ``update``
@@ -344,7 +344,7 @@ if the input is valid. We can express this in the type as follows:
344Then, when we implement ``readAndAdd`` we need to return the appropriate
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
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``:
346return ``True``, otherwise we need to return ``False``:
348.. code-block:: idris
348.. code-block:: idris
350 readAndAdd : ConsoleIO io => (vec : Var) ->
350 readAndAdd : ConsoleIO io => (vec : Var) ->
@@ -435,7 +435,7 @@ we can do as follows:
436.. _stransprimops:
436.. _stransprimops:
438−``STrans`` Primitive operations
438+``STrans`` Primitive operations
439===============================
439===============================
441Now that we've written a few small examples of ``STrans`` functions, it's
441Now that we've written a few small examples of ``STrans`` functions, it's
@@ -485,7 +485,7 @@ of type ``State state``:
486.. code-block:: idris
486.. code-block:: idris
488− new : (val : state) ->
488+ new : (val : state) ->
489 STrans m Var res (\lbl => (lbl ::: State state) :: res)
489 STrans m Var res (\lbl => (lbl ::: State state) :: res)
491It's important that the new resource has type ``State state``, rather than
491It's important that the new resource has type ``State state``, rather than
@@ -526,7 +526,7 @@ the resource list so that it is appropriate for returning that value:
527.. code-block:: idris
527.. code-block:: idris
529− returning : (result : ty) ->
529+ returning : (result : ty) ->
530 STrans m () res (const (out_fn result)) ->
530 STrans m () res (const (out_fn result)) ->
531 STrans m ty res out_fn
531 STrans m ty res out_fn
@@ -555,7 +555,7 @@ programming and reasoning in Idris.
555.. _sttype:
555.. _sttype:
557`ST`: Representing state transitions directly
557`ST`: Representing state transitions directly
558−============================================
558+=============================================
560We've seen a few examples of small ``STrans`` functions now, and
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
561their types can become quite verbose given that we need to provide explicit
@@ -568,7 +568,7 @@ giving input and output resource lists in full. We can do this with
568.. code-block:: idris
568.. code-block:: idris
570 ST : (m : Type -> Type) ->
570 ST : (m : Type -> Type) ->
571− (resultType : Type) ->
571+ (resultType : Type) ->
572 List (Action resultType) -> Type
572 List (Action resultType) -> Type
574``ST`` is a type level function which computes an appropriate ``STrans``
574``ST`` is a type level function which computes an appropriate ``STrans``
@@ -593,7 +593,7 @@ So, we can write some of the function types we've seen so far as follows:
593That is, ``increment`` begins and ends with ``x`` in state ``State Integer``.
593That is, ``increment`` begins and ends with ``x`` in state ``State Integer``.
595.. code-block:: idris
595.. code-block:: idris
597 makeAndIncrement : Int -> ST m Int []
597 makeAndIncrement : Int -> ST m Int []
599That is, ``makeAndIncrement`` begins and ends with no resources.
599That is, ``makeAndIncrement`` begins and ends with no resources.
@@ -652,5 +652,3 @@ the 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
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
653a precise API for a system with security properties: a data store requiring