30 text \<open> |
30 text \<open> |
31 We classify functions operating on states into two categories: |
31 We classify functions operating on states into two categories: |
32 |
32 |
33 \begin{description} |
33 \begin{description} |
34 |
34 |
35 \item[transformations] with type signature @{text "\<sigma> \<Rightarrow> \<sigma>'"}, |
35 \item[transformations] with type signature \<open>\<sigma> \<Rightarrow> \<sigma>'\<close>, |
36 transforming a state. |
36 transforming a state. |
37 |
37 |
38 \item[``yielding'' transformations] with type signature @{text "\<sigma> |
38 \item[``yielding'' transformations] with type signature \<open>\<sigma> |
39 \<Rightarrow> \<alpha> \<times> \<sigma>'"}, ``yielding'' a side result while transforming a |
39 \<Rightarrow> \<alpha> \<times> \<sigma>'\<close>, ``yielding'' a side result while transforming a |
40 state. |
40 state. |
41 |
41 |
42 \item[queries] with type signature @{text "\<sigma> \<Rightarrow> \<alpha>"}, computing a |
42 \item[queries] with type signature \<open>\<sigma> \<Rightarrow> \<alpha>\<close>, computing a |
43 result dependent on a state. |
43 result dependent on a state. |
44 |
44 |
45 \end{description} |
45 \end{description} |
46 |
46 |
47 By convention we write @{text "\<sigma>"} for types representing states and |
47 By convention we write \<open>\<sigma>\<close> for types representing states and |
48 @{text "\<alpha>"}, @{text "\<beta>"}, @{text "\<gamma>"}, @{text "\<dots>"} for types |
48 \<open>\<alpha>\<close>, \<open>\<beta>\<close>, \<open>\<gamma>\<close>, \<open>\<dots>\<close> for types |
49 representing side results. Type changes due to transformations are |
49 representing side results. Type changes due to transformations are |
50 not excluded in our scenario. |
50 not excluded in our scenario. |
51 |
51 |
52 We aim to assert that values of any state type @{text "\<sigma>"} are used |
52 We aim to assert that values of any state type \<open>\<sigma>\<close> are used |
53 in a single-threaded way: after application of a transformation on a |
53 in a single-threaded way: after application of a transformation on a |
54 value of type @{text "\<sigma>"}, the former value should not be used |
54 value of type \<open>\<sigma>\<close>, the former value should not be used |
55 again. To achieve this, we use a set of monad combinators: |
55 again. To achieve this, we use a set of monad combinators: |
56 \<close> |
56 \<close> |
57 |
57 |
58 notation fcomp (infixl "\<circ>>" 60) |
58 notation fcomp (infixl "\<circ>>" 60) |
59 notation scomp (infixl "\<circ>\<rightarrow>" 60) |
59 notation scomp (infixl "\<circ>\<rightarrow>" 60) |