21192
|
1 |
(* Title: HOL/Library/State_Monad.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Florian Haftmann, TU Muenchen
|
|
4 |
*)
|
|
5 |
|
|
6 |
header {* Combinators syntax for generic, open state monads (single threaded monads) *}
|
|
7 |
|
|
8 |
theory State_Monad
|
|
9 |
imports Main
|
|
10 |
begin
|
|
11 |
|
|
12 |
section {* Generic, open state monads *}
|
|
13 |
|
|
14 |
subsection {* Motivation *}
|
|
15 |
|
|
16 |
text {*
|
|
17 |
The logic HOL has no notion of constructor classes, so
|
|
18 |
it is not possible to model monads the Haskell way
|
|
19 |
in full genericity in Isabelle/HOL.
|
|
20 |
|
|
21 |
However, this theory provides substantial support for
|
|
22 |
a very common class of monads: \emph{state monads}
|
|
23 |
(or \emph{single-threaded monads}, since a state
|
|
24 |
is transformed single-threaded).
|
|
25 |
|
|
26 |
To enter from the Haskell world,
|
|
27 |
\url{http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm}
|
|
28 |
makes a good motivating start. Here we just sketch briefly
|
|
29 |
how those monads enter the game of Isabelle/HOL.
|
|
30 |
*}
|
|
31 |
|
|
32 |
subsection {* State transformations and combinators *}
|
|
33 |
|
|
34 |
(*<*)
|
|
35 |
typedecl \<alpha>
|
|
36 |
typedecl \<beta>
|
|
37 |
typedecl \<gamma>
|
|
38 |
typedecl \<sigma>
|
|
39 |
typedecl \<sigma>'
|
|
40 |
(*>*)
|
|
41 |
|
|
42 |
text {*
|
|
43 |
We classify functions operating on states into two categories:
|
|
44 |
|
|
45 |
\begin{description}
|
|
46 |
\item[transformations]
|
|
47 |
with type signature @{typ "\<sigma> \<Rightarrow> \<sigma>'"},
|
|
48 |
transforming a state.
|
|
49 |
\item[``yielding'' transformations]
|
|
50 |
with type signature @{typ "\<sigma> \<Rightarrow> \<alpha> \<times> \<sigma>'"},
|
|
51 |
``yielding'' a side result while transforming a state.
|
|
52 |
\item[queries]
|
|
53 |
with type signature @{typ "\<sigma> \<Rightarrow> \<alpha>"},
|
|
54 |
computing a result dependent on a state.
|
|
55 |
\end{description}
|
|
56 |
|
|
57 |
By convention we write @{typ "\<sigma>"} for types representing states
|
|
58 |
and @{typ "\<alpha>"}, @{typ "\<beta>"}, @{typ "\<gamma>"}, @{text "\<dots>"}
|
|
59 |
for types representing side results. Type changes due
|
|
60 |
to transformations are not excluded in our scenario.
|
|
61 |
|
|
62 |
We aim to assert that values of any state type @{typ "\<sigma>"}
|
|
63 |
are used in a single-threaded way: after application
|
|
64 |
of a transformation on a value of type @{typ "\<sigma>"}, the
|
|
65 |
former value should not be used again. To achieve this,
|
|
66 |
we use a set of monad combinators:
|
|
67 |
*}
|
|
68 |
|
|
69 |
definition
|
|
70 |
mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
|
21283
|
71 |
(infixl ">>=" 60)
|
|
72 |
"f >>= g = split g \<circ> f"
|
21192
|
73 |
fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"
|
21283
|
74 |
(infixl ">>" 60)
|
|
75 |
"f >> g = g \<circ> f"
|
21192
|
76 |
run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
|
|
77 |
"run f = f"
|
|
78 |
|
21283
|
79 |
print_ast_translation {*[
|
|
80 |
(Sign.const_syntax_name (the_context ()) "State_Monad.run", fn (f::ts) => Syntax.mk_appl f ts)
|
|
81 |
]*}
|
|
82 |
|
|
83 |
syntax (xsymbols)
|
21192
|
84 |
mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
|
21283
|
85 |
(infixl "\<guillemotright>=" 60)
|
21192
|
86 |
fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"
|
21283
|
87 |
(infixl "\<guillemotright>" 60)
|
21192
|
88 |
|
|
89 |
abbreviation (input)
|
|
90 |
"return \<equiv> Pair"
|
|
91 |
|
|
92 |
text {*
|
|
93 |
Given two transformations @{term f} and @{term g}, they
|
|
94 |
may be directly composed using the @{term "op \<guillemotright>"} combinator,
|
|
95 |
forming a forward composition: @{prop "(f \<guillemotright> g) s = f (g s)"}.
|
|
96 |
|
|
97 |
After any yielding transformation, we bind the side result
|
|
98 |
immediately using a lambda abstraction. This
|
|
99 |
is the purpose of the @{term "op \<guillemotright>="} combinator:
|
|
100 |
@{prop "(f \<guillemotright>= (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
|
|
101 |
|
|
102 |
For queries, the existing @{term "Let"} is appropriate.
|
|
103 |
|
|
104 |
Naturally, a computation may yield a side result by pairing
|
|
105 |
it to the state from the left; we introduce the
|
|
106 |
suggestive abbreviation @{term return} for this purpose.
|
|
107 |
|
|
108 |
The @{const run} ist just a marker.
|
|
109 |
|
|
110 |
The most crucial distinction to Haskell is that we do
|
|
111 |
not need to introduce distinguished type constructors
|
|
112 |
for different kinds of state. This has two consequences:
|
|
113 |
\begin{itemize}
|
|
114 |
\item The monad model does not state anything about
|
|
115 |
the kind of state; the model for the state is
|
21283
|
116 |
completely orthogonal and has to (or may) be
|
21192
|
117 |
specified completely independent.
|
|
118 |
\item There is no distinguished type constructor
|
|
119 |
encapsulating away the state transformation, i.e.~transformations
|
|
120 |
may be applied directly without using any lifting
|
|
121 |
or providing and dropping units (``open monad'').
|
|
122 |
\item The type of states may change due to a transformation.
|
|
123 |
\end{itemize}
|
|
124 |
*}
|
|
125 |
|
|
126 |
|
|
127 |
subsection {* Obsolete runs *}
|
|
128 |
|
|
129 |
text {*
|
|
130 |
@{term run} is just a doodle and should not occur nested:
|
|
131 |
*}
|
|
132 |
|
|
133 |
lemma run_simp [simp]:
|
|
134 |
"\<And>f. run (run f) = run f"
|
|
135 |
"\<And>f g. run f \<guillemotright>= g = f \<guillemotright>= g"
|
|
136 |
"\<And>f g. run f \<guillemotright> g = f \<guillemotright> g"
|
|
137 |
"\<And>f g. f \<guillemotright>= (\<lambda>x. run g) = f \<guillemotright>= (\<lambda>x. g)"
|
|
138 |
"\<And>f g. f \<guillemotright> run g = f \<guillemotright> g"
|
|
139 |
"\<And>f. f = run f \<longleftrightarrow> True"
|
|
140 |
"\<And>f. run f = f \<longleftrightarrow> True"
|
|
141 |
unfolding run_def by rule+
|
|
142 |
|
|
143 |
|
|
144 |
subsection {* Monad laws *}
|
|
145 |
|
|
146 |
text {*
|
|
147 |
The common monadic laws hold and may also be used
|
|
148 |
as normalization rules for monadic expressions:
|
|
149 |
*}
|
|
150 |
|
|
151 |
lemma
|
|
152 |
return_mbind [simp]: "return x \<guillemotright>= f = f x"
|
|
153 |
unfolding mbind_def by (simp add: expand_fun_eq)
|
|
154 |
|
|
155 |
lemma
|
|
156 |
mbind_return [simp]: "x \<guillemotright>= return = x"
|
|
157 |
unfolding mbind_def by (simp add: expand_fun_eq split_Pair)
|
|
158 |
|
|
159 |
lemma
|
|
160 |
mbind_mbind [simp]: "(f \<guillemotright>= g) \<guillemotright>= h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h)"
|
|
161 |
unfolding mbind_def by (simp add: split_def expand_fun_eq)
|
|
162 |
|
|
163 |
lemma
|
|
164 |
mbind_fcomp [simp]: "(f \<guillemotright>= g) \<guillemotright> h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright> h)"
|
|
165 |
unfolding mbind_def fcomp_def by (simp add: split_def expand_fun_eq)
|
|
166 |
|
|
167 |
lemma
|
|
168 |
fcomp_mbind [simp]: "(f \<guillemotright> g) \<guillemotright>= h = f \<guillemotright> (g \<guillemotright>= h)"
|
|
169 |
unfolding mbind_def fcomp_def by (simp add: split_def expand_fun_eq)
|
|
170 |
|
|
171 |
lemma
|
|
172 |
fcomp_fcomp [simp]: "(f \<guillemotright> g) \<guillemotright> h = f \<guillemotright> (g \<guillemotright> h)"
|
|
173 |
unfolding fcomp_def o_assoc ..
|
|
174 |
|
|
175 |
lemmas monad_simp = run_simp return_mbind mbind_return
|
|
176 |
mbind_mbind mbind_fcomp fcomp_mbind fcomp_fcomp
|
|
177 |
|
|
178 |
text {*
|
|
179 |
Evaluation of monadic expressions by force:
|
|
180 |
*}
|
|
181 |
|
|
182 |
lemmas monad_collapse = monad_simp o_apply o_assoc split_Pair split_comp
|
|
183 |
mbind_def fcomp_def run_def
|
|
184 |
|
|
185 |
subsection {* Syntax *}
|
|
186 |
|
|
187 |
text {*
|
|
188 |
We provide a convenient do-notation for monadic expressions
|
|
189 |
well-known from Haskell. @{const Let} is printed
|
|
190 |
specially in do-expressions.
|
|
191 |
*}
|
|
192 |
|
|
193 |
nonterminals do_expr
|
|
194 |
|
|
195 |
syntax
|
|
196 |
"_do" :: "do_expr \<Rightarrow> 'a"
|
|
197 |
("do _ done" [12] 12)
|
|
198 |
"_mbind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
|
|
199 |
("_ <- _;// _" [1000, 13, 12] 12)
|
|
200 |
"_fcomp" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
|
|
201 |
("_;// _" [13, 12] 12)
|
|
202 |
"_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
|
|
203 |
("let _ = _;// _" [1000, 13, 12] 12)
|
|
204 |
"_nil" :: "'a \<Rightarrow> do_expr"
|
|
205 |
("_" [12] 12)
|
|
206 |
|
|
207 |
syntax (xsymbols)
|
|
208 |
"_mbind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
|
|
209 |
("_ \<leftarrow> _;// _" [1000, 13, 12] 12)
|
|
210 |
|
|
211 |
translations
|
|
212 |
"_do f" => "State_Monad.run f"
|
|
213 |
"_mbind x f g" => "f \<guillemotright>= (\<lambda>x. g)"
|
|
214 |
"_fcomp f g" => "f \<guillemotright> g"
|
|
215 |
"_let x t f" => "Let t (\<lambda>x. f)"
|
|
216 |
"_nil f" => "f"
|
|
217 |
|
|
218 |
print_translation {*
|
|
219 |
let
|
|
220 |
val syntax_name = Sign.const_syntax_name (the_context ());
|
|
221 |
val name_mbind = syntax_name "State_Monad.mbind";
|
|
222 |
val name_fcomp = syntax_name "State_Monad.fcomp";
|
|
223 |
fun unfold_monad (t as Const (name, _) $ f $ g) =
|
|
224 |
if name = name_mbind then let
|
|
225 |
val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
|
|
226 |
in Const ("_mbind", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
|
|
227 |
else if name = name_fcomp then
|
|
228 |
Const ("_fcomp", dummyT) $ f $ unfold_monad g
|
|
229 |
else t
|
|
230 |
| unfold_monad (Const ("Let", _) $ f $ g) =
|
|
231 |
let
|
21283
|
232 |
|
21192
|
233 |
val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
|
|
234 |
in Const ("_let", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
|
|
235 |
| unfold_monad (Const ("Pair", _) $ f) =
|
|
236 |
Const ("return", dummyT) $ f
|
|
237 |
| unfold_monad f = f;
|
|
238 |
fun tr' (f::ts) =
|
|
239 |
list_comb (Const ("_do", dummyT) $ unfold_monad f, ts)
|
|
240 |
in [
|
|
241 |
(syntax_name "State_Monad.run", tr')
|
|
242 |
] end;
|
|
243 |
*}
|
|
244 |
|
|
245 |
text {*
|
|
246 |
For an example, see HOL/ex/CodeRandom.thy (more examples coming soon).
|
|
247 |
*}
|
|
248 |
|
|
249 |
end |