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