author | blanchet |
Mon, 14 Dec 2009 12:14:12 +0100 | |
changeset 34120 | f9920a3ddf50 |
parent 31033 | c46d52fee219 |
child 35115 | 446c5063e4fd |
permissions | -rw-r--r-- |
21192 | 1 |
(* Title: HOL/Library/State_Monad.thy |
2 |
Author: Florian Haftmann, TU Muenchen |
|
3 |
*) |
|
4 |
||
27487 | 5 |
header {* Combinator syntax for generic, open state monads (single threaded monads) *} |
21192 | 6 |
|
7 |
theory State_Monad |
|
30738 | 8 |
imports Main |
21192 | 9 |
begin |
10 |
||
11 |
subsection {* Motivation *} |
|
12 |
||
13 |
text {* |
|
14 |
The logic HOL has no notion of constructor classes, so |
|
15 |
it is not possible to model monads the Haskell way |
|
16 |
in full genericity in Isabelle/HOL. |
|
17 |
||
18 |
However, this theory provides substantial support for |
|
19 |
a very common class of monads: \emph{state monads} |
|
20 |
(or \emph{single-threaded monads}, since a state |
|
21 |
is transformed single-threaded). |
|
22 |
||
23 |
To enter from the Haskell world, |
|
24 |
\url{http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm} |
|
25 |
makes a good motivating start. Here we just sketch briefly |
|
26 |
how those monads enter the game of Isabelle/HOL. |
|
27 |
*} |
|
28 |
||
29 |
subsection {* State transformations and combinators *} |
|
30 |
||
31 |
text {* |
|
32 |
We classify functions operating on states into two categories: |
|
33 |
||
34 |
\begin{description} |
|
35 |
\item[transformations] |
|
26266 | 36 |
with type signature @{text "\<sigma> \<Rightarrow> \<sigma>'"}, |
21192 | 37 |
transforming a state. |
38 |
\item[``yielding'' transformations] |
|
26266 | 39 |
with type signature @{text "\<sigma> \<Rightarrow> \<alpha> \<times> \<sigma>'"}, |
21192 | 40 |
``yielding'' a side result while transforming a state. |
41 |
\item[queries] |
|
26266 | 42 |
with type signature @{text "\<sigma> \<Rightarrow> \<alpha>"}, |
21192 | 43 |
computing a result dependent on a state. |
44 |
\end{description} |
|
45 |
||
26266 | 46 |
By convention we write @{text "\<sigma>"} for types representing states |
47 |
and @{text "\<alpha>"}, @{text "\<beta>"}, @{text "\<gamma>"}, @{text "\<dots>"} |
|
21192 | 48 |
for types representing side results. Type changes due |
49 |
to transformations are not excluded in our scenario. |
|
50 |
||
26266 | 51 |
We aim to assert that values of any state type @{text "\<sigma>"} |
21192 | 52 |
are used in a single-threaded way: after application |
26266 | 53 |
of a transformation on a value of type @{text "\<sigma>"}, the |
21192 | 54 |
former value should not be used again. To achieve this, |
55 |
we use a set of monad combinators: |
|
56 |
*} |
|
57 |
||
28145 | 58 |
notation fcomp (infixl "o>" 60) |
59 |
notation (xsymbols) fcomp (infixl "o>" 60) |
|
60 |
notation scomp (infixl "o->" 60) |
|
61 |
notation (xsymbols) scomp (infixl "o\<rightarrow>" 60) |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21283
diff
changeset
|
62 |
|
26588
d83271bfaba5
removed syntax from monad combinators; renamed mbind to scomp
haftmann
parents:
26266
diff
changeset
|
63 |
abbreviation (input) |
d83271bfaba5
removed syntax from monad combinators; renamed mbind to scomp
haftmann
parents:
26266
diff
changeset
|
64 |
"return \<equiv> Pair" |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21283
diff
changeset
|
65 |
|
21192 | 66 |
text {* |
67 |
Given two transformations @{term f} and @{term g}, they |
|
28145 | 68 |
may be directly composed using the @{term "op o>"} combinator, |
69 |
forming a forward composition: @{prop "(f o> g) s = f (g s)"}. |
|
21192 | 70 |
|
71 |
After any yielding transformation, we bind the side result |
|
72 |
immediately using a lambda abstraction. This |
|
28145 | 73 |
is the purpose of the @{term "op o\<rightarrow>"} combinator: |
74 |
@{prop "(f o\<rightarrow> (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}. |
|
21192 | 75 |
|
76 |
For queries, the existing @{term "Let"} is appropriate. |
|
77 |
||
78 |
Naturally, a computation may yield a side result by pairing |
|
79 |
it to the state from the left; we introduce the |
|
80 |
suggestive abbreviation @{term return} for this purpose. |
|
81 |
||
82 |
The most crucial distinction to Haskell is that we do |
|
83 |
not need to introduce distinguished type constructors |
|
84 |
for different kinds of state. This has two consequences: |
|
85 |
\begin{itemize} |
|
86 |
\item The monad model does not state anything about |
|
87 |
the kind of state; the model for the state is |
|
26260 | 88 |
completely orthogonal and may be |
89 |
specified completely independently. |
|
21192 | 90 |
\item There is no distinguished type constructor |
91 |
encapsulating away the state transformation, i.e.~transformations |
|
92 |
may be applied directly without using any lifting |
|
93 |
or providing and dropping units (``open monad''). |
|
94 |
\item The type of states may change due to a transformation. |
|
95 |
\end{itemize} |
|
96 |
*} |
|
97 |
||
98 |
||
99 |
subsection {* Monad laws *} |
|
100 |
||
101 |
text {* |
|
102 |
The common monadic laws hold and may also be used |
|
103 |
as normalization rules for monadic expressions: |
|
104 |
*} |
|
105 |
||
28145 | 106 |
lemmas monad_simp = Pair_scomp scomp_Pair id_fcomp fcomp_id |
107 |
scomp_scomp scomp_fcomp fcomp_scomp fcomp_assoc |
|
21192 | 108 |
|
109 |
text {* |
|
110 |
Evaluation of monadic expressions by force: |
|
111 |
*} |
|
112 |
||
28145 | 113 |
lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta |
26260 | 114 |
|
115 |
||
21192 | 116 |
subsection {* Syntax *} |
117 |
||
118 |
text {* |
|
119 |
We provide a convenient do-notation for monadic expressions |
|
120 |
well-known from Haskell. @{const Let} is printed |
|
121 |
specially in do-expressions. |
|
122 |
*} |
|
123 |
||
124 |
nonterminals do_expr |
|
125 |
||
126 |
syntax |
|
127 |
"_do" :: "do_expr \<Rightarrow> 'a" |
|
128 |
("do _ done" [12] 12) |
|
26588
d83271bfaba5
removed syntax from monad combinators; renamed mbind to scomp
haftmann
parents:
26266
diff
changeset
|
129 |
"_scomp" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr" |
21192 | 130 |
("_ <- _;// _" [1000, 13, 12] 12) |
131 |
"_fcomp" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr" |
|
132 |
("_;// _" [13, 12] 12) |
|
133 |
"_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr" |
|
134 |
("let _ = _;// _" [1000, 13, 12] 12) |
|
28145 | 135 |
"_done" :: "'a \<Rightarrow> do_expr" |
21192 | 136 |
("_" [12] 12) |
137 |
||
138 |
syntax (xsymbols) |
|
26588
d83271bfaba5
removed syntax from monad combinators; renamed mbind to scomp
haftmann
parents:
26266
diff
changeset
|
139 |
"_scomp" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr" |
21192 | 140 |
("_ \<leftarrow> _;// _" [1000, 13, 12] 12) |
141 |
||
142 |
translations |
|
28145 | 143 |
"_do f" => "f" |
144 |
"_scomp x f g" => "f o\<rightarrow> (\<lambda>x. g)" |
|
145 |
"_fcomp f g" => "f o> g" |
|
24195 | 146 |
"_let x t f" => "CONST Let t (\<lambda>x. f)" |
28145 | 147 |
"_done f" => "f" |
21192 | 148 |
|
149 |
print_translation {* |
|
150 |
let |
|
24253 | 151 |
fun dest_abs_eta (Abs (abs as (_, ty, _))) = |
152 |
let |
|
153 |
val (v, t) = Syntax.variant_abs abs; |
|
28145 | 154 |
in (Free (v, ty), t) end |
24253 | 155 |
| dest_abs_eta t = |
21192 | 156 |
let |
24253 | 157 |
val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0); |
28145 | 158 |
in (Free (v, dummyT), t) end; |
26588
d83271bfaba5
removed syntax from monad combinators; renamed mbind to scomp
haftmann
parents:
26266
diff
changeset
|
159 |
fun unfold_monad (Const (@{const_syntax scomp}, _) $ f $ g) = |
24253 | 160 |
let |
28145 | 161 |
val (v, g') = dest_abs_eta g; |
162 |
in Const ("_scomp", dummyT) $ v $ f $ unfold_monad g' end |
|
24195 | 163 |
| unfold_monad (Const (@{const_syntax fcomp}, _) $ f $ g) = |
164 |
Const ("_fcomp", dummyT) $ f $ unfold_monad g |
|
24253 | 165 |
| unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) = |
24195 | 166 |
let |
28145 | 167 |
val (v, g') = dest_abs_eta g; |
168 |
in Const ("_let", dummyT) $ v $ f $ unfold_monad g' end |
|
24195 | 169 |
| unfold_monad (Const (@{const_syntax Pair}, _) $ f) = |
21192 | 170 |
Const ("return", dummyT) $ f |
171 |
| unfold_monad f = f; |
|
28145 | 172 |
fun contains_scomp (Const (@{const_syntax scomp}, _) $ _ $ _) = true |
173 |
| contains_scomp (Const (@{const_syntax fcomp}, _) $ _ $ t) = |
|
174 |
contains_scomp t |
|
175 |
| contains_scomp (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) = |
|
176 |
contains_scomp t; |
|
177 |
fun scomp_monad_tr' (f::g::ts) = list_comb |
|
178 |
(Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax scomp}, dummyT) $ f $ g), ts); |
|
179 |
fun fcomp_monad_tr' (f::g::ts) = if contains_scomp g then list_comb |
|
180 |
(Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax fcomp}, dummyT) $ f $ g), ts) |
|
181 |
else raise Match; |
|
182 |
fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) = if contains_scomp g' then list_comb |
|
183 |
(Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts) |
|
184 |
else raise Match; |
|
185 |
in [ |
|
186 |
(@{const_syntax scomp}, scomp_monad_tr'), |
|
187 |
(@{const_syntax fcomp}, fcomp_monad_tr'), |
|
188 |
(@{const_syntax Let}, Let_monad_tr') |
|
189 |
] end; |
|
21192 | 190 |
*} |
191 |
||
21418 | 192 |
text {* |
31033 | 193 |
For an example, see HOL/Extraction/Higman.thy. |
21192 | 194 |
*} |
195 |
||
22664 | 196 |
end |