author  haftmann 
Wed, 12 Mar 2008 08:47:36 +0100  
changeset 26260  23ce0d32de11 
parent 26141  e1b3a6953cdc 
child 26266  35ae83ca190a 
permissions  rwrr 
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 

25595  9 
imports List 
21192  10 
begin 
11 

12 
subsection {* Motivation *} 

13 

14 
text {* 

15 
The logic HOL has no notion of constructor classes, so 

16 
it is not possible to model monads the Haskell way 

17 
in full genericity in Isabelle/HOL. 

18 

19 
However, this theory provides substantial support for 

20 
a very common class of monads: \emph{state monads} 

21 
(or \emph{singlethreaded monads}, since a state 

22 
is transformed singlethreaded). 

23 

24 
To enter from the Haskell world, 

25 
\url{http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm} 

26 
makes a good motivating start. Here we just sketch briefly 

27 
how those monads enter the game of Isabelle/HOL. 

28 
*} 

29 

30 
subsection {* State transformations and combinators *} 

31 

32 
(*<*) 

33 
typedecl \<alpha> 

34 
typedecl \<beta> 

35 
typedecl \<gamma> 

36 
typedecl \<sigma> 

37 
typedecl \<sigma>' 

38 
(*>*) 

39 

40 
text {* 

41 
We classify functions operating on states into two categories: 

42 

43 
\begin{description} 

44 
\item[transformations] 

45 
with type signature @{typ "\<sigma> \<Rightarrow> \<sigma>'"}, 

46 
transforming a state. 

47 
\item[``yielding'' transformations] 

48 
with type signature @{typ "\<sigma> \<Rightarrow> \<alpha> \<times> \<sigma>'"}, 

49 
``yielding'' a side result while transforming a state. 

50 
\item[queries] 

51 
with type signature @{typ "\<sigma> \<Rightarrow> \<alpha>"}, 

52 
computing a result dependent on a state. 

53 
\end{description} 

54 

55 
By convention we write @{typ "\<sigma>"} for types representing states 

56 
and @{typ "\<alpha>"}, @{typ "\<beta>"}, @{typ "\<gamma>"}, @{text "\<dots>"} 

57 
for types representing side results. Type changes due 

58 
to transformations are not excluded in our scenario. 

59 

60 
We aim to assert that values of any state type @{typ "\<sigma>"} 

61 
are used in a singlethreaded way: after application 

62 
of a transformation on a value of type @{typ "\<sigma>"}, the 

63 
former value should not be used again. To achieve this, 

64 
we use a set of monad combinators: 

65 
*} 

66 

67 
definition 

68 
mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21283
diff
changeset

69 
(infixl ">>=" 60) where 
21283  70 
"f >>= g = split g \<circ> f" 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21283
diff
changeset

71 

eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21283
diff
changeset

72 
definition 
21192  73 
fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21283
diff
changeset

74 
(infixl ">>" 60) where 
21283  75 
"f >> g = g \<circ> f" 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21283
diff
changeset

76 

eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21283
diff
changeset

77 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21283
diff
changeset

78 
run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where 
21192  79 
"run f = f" 
80 

21283  81 
syntax (xsymbols) 
21192  82 
mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" 
21283  83 
(infixl "\<guillemotright>=" 60) 
21192  84 
fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" 
21283  85 
(infixl "\<guillemotright>" 60) 
21192  86 

87 
abbreviation (input) 

88 
"return \<equiv> Pair" 

89 

22377  90 
print_ast_translation {* 
91 
[(@{const_syntax "run"}, fn (f::ts) => Syntax.mk_appl f ts)] 

92 
*} 

21835  93 

21192  94 
text {* 
95 
Given two transformations @{term f} and @{term g}, they 

96 
may be directly composed using the @{term "op \<guillemotright>"} combinator, 

97 
forming a forward composition: @{prop "(f \<guillemotright> g) s = f (g s)"}. 

98 

99 
After any yielding transformation, we bind the side result 

100 
immediately using a lambda abstraction. This 

101 
is the purpose of the @{term "op \<guillemotright>="} combinator: 

102 
@{prop "(f \<guillemotright>= (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}. 

103 

104 
For queries, the existing @{term "Let"} is appropriate. 

105 

106 
Naturally, a computation may yield a side result by pairing 

107 
it to the state from the left; we introduce the 

108 
suggestive abbreviation @{term return} for this purpose. 

109 

110 
The @{const run} ist just a marker. 

111 

112 
The most crucial distinction to Haskell is that we do 

113 
not need to introduce distinguished type constructors 

114 
for different kinds of state. This has two consequences: 

115 
\begin{itemize} 

116 
\item The monad model does not state anything about 

117 
the kind of state; the model for the state is 

26260  118 
completely orthogonal and may be 
119 
specified completely independently. 

21192  120 
\item There is no distinguished type constructor 
121 
encapsulating away the state transformation, i.e.~transformations 

122 
may be applied directly without using any lifting 

123 
or providing and dropping units (``open monad''). 

124 
\item The type of states may change due to a transformation. 

125 
\end{itemize} 

126 
*} 

127 

128 

129 
subsection {* Obsolete runs *} 

130 

131 
text {* 

132 
@{term run} is just a doodle and should not occur nested: 

133 
*} 

134 

135 
lemma run_simp [simp]: 

136 
"\<And>f. run (run f) = run f" 

137 
"\<And>f g. run f \<guillemotright>= g = f \<guillemotright>= g" 

138 
"\<And>f g. run f \<guillemotright> g = f \<guillemotright> g" 

139 
"\<And>f g. f \<guillemotright>= (\<lambda>x. run g) = f \<guillemotright>= (\<lambda>x. g)" 

140 
"\<And>f g. f \<guillemotright> run g = f \<guillemotright> g" 

141 
"\<And>f. f = run f \<longleftrightarrow> True" 

142 
"\<And>f. run f = f \<longleftrightarrow> True" 

143 
unfolding run_def by rule+ 

144 

145 
subsection {* Monad laws *} 

146 

147 
text {* 

148 
The common monadic laws hold and may also be used 

149 
as normalization rules for monadic expressions: 

150 
*} 

151 

152 
lemma 

153 
return_mbind [simp]: "return x \<guillemotright>= f = f x" 

154 
unfolding mbind_def by (simp add: expand_fun_eq) 

155 

156 
lemma 

157 
mbind_return [simp]: "x \<guillemotright>= return = x" 

158 
unfolding mbind_def by (simp add: expand_fun_eq split_Pair) 

159 

160 
lemma 

21418  161 
id_fcomp [simp]: "id \<guillemotright> f = f" 
162 
unfolding fcomp_def by simp 

163 

164 
lemma 

165 
fcomp_id [simp]: "f \<guillemotright> id = f" 

166 
unfolding fcomp_def by simp 

167 

168 
lemma 

21192  169 
mbind_mbind [simp]: "(f \<guillemotright>= g) \<guillemotright>= h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h)" 
170 
unfolding mbind_def by (simp add: split_def expand_fun_eq) 

171 

172 
lemma 

173 
mbind_fcomp [simp]: "(f \<guillemotright>= g) \<guillemotright> h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright> h)" 

174 
unfolding mbind_def fcomp_def by (simp add: split_def expand_fun_eq) 

175 

176 
lemma 

177 
fcomp_mbind [simp]: "(f \<guillemotright> g) \<guillemotright>= h = f \<guillemotright> (g \<guillemotright>= h)" 

178 
unfolding mbind_def fcomp_def by (simp add: split_def expand_fun_eq) 

179 

180 
lemma 

181 
fcomp_fcomp [simp]: "(f \<guillemotright> g) \<guillemotright> h = f \<guillemotright> (g \<guillemotright> h)" 

182 
unfolding fcomp_def o_assoc .. 

183 

21418  184 
lemmas monad_simp = run_simp return_mbind mbind_return id_fcomp fcomp_id 
21192  185 
mbind_mbind mbind_fcomp fcomp_mbind fcomp_fcomp 
186 

187 
text {* 

188 
Evaluation of monadic expressions by force: 

189 
*} 

190 

191 
lemmas monad_collapse = monad_simp o_apply o_assoc split_Pair split_comp 

192 
mbind_def fcomp_def run_def 

193 

26260  194 
subsection {* ML abstract operations *} 
195 

196 
ML {* 

197 
structure StateMonad = 

198 
struct 

199 

200 
fun liftT T sT = sT > HOLogic.mk_prodT (T, sT); 

201 
fun liftT' sT = sT > sT; 

202 

203 
fun return T sT x = Const (@{const_name return}, T > liftT T sT) $ x; 

204 

205 
fun mbind T1 T2 sT f g = Const (@{const_name mbind}, 

206 
liftT T1 sT > (T1 > liftT T2 sT) > liftT T2 sT) $ f $ g; 

207 

208 
fun run T sT f = Const (@{const_name run}, liftT' (liftT T sT)) $ f; 

209 

210 
end; 

211 
*} 

212 

213 

21192  214 
subsection {* Syntax *} 
215 

216 
text {* 

217 
We provide a convenient donotation for monadic expressions 

218 
wellknown from Haskell. @{const Let} is printed 

219 
specially in doexpressions. 

220 
*} 

221 

222 
nonterminals do_expr 

223 

224 
syntax 

225 
"_do" :: "do_expr \<Rightarrow> 'a" 

226 
("do _ done" [12] 12) 

227 
"_mbind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr" 

228 
("_ < _;// _" [1000, 13, 12] 12) 

229 
"_fcomp" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr" 

230 
("_;// _" [13, 12] 12) 

231 
"_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr" 

232 
("let _ = _;// _" [1000, 13, 12] 12) 

233 
"_nil" :: "'a \<Rightarrow> do_expr" 

234 
("_" [12] 12) 

235 

236 
syntax (xsymbols) 

237 
"_mbind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr" 

238 
("_ \<leftarrow> _;// _" [1000, 13, 12] 12) 

239 

240 
translations 

22664  241 
"_do f" => "CONST run f" 
21192  242 
"_mbind x f g" => "f \<guillemotright>= (\<lambda>x. g)" 
243 
"_fcomp f g" => "f \<guillemotright> g" 

24195  244 
"_let x t f" => "CONST Let t (\<lambda>x. f)" 
21192  245 
"_nil f" => "f" 
246 

247 
print_translation {* 

248 
let 

24253  249 
fun dest_abs_eta (Abs (abs as (_, ty, _))) = 
250 
let 

251 
val (v, t) = Syntax.variant_abs abs; 

252 
in ((v, ty), t) end 

253 
 dest_abs_eta t = 

21192  254 
let 
24253  255 
val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0); 
256 
in ((v, dummyT), t) end 

257 
fun unfold_monad (Const (@{const_syntax mbind}, _) $ f $ g) = 

258 
let 

259 
val ((v, ty), g') = dest_abs_eta g; 

260 
in Const ("_mbind", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end 

24195  261 
 unfold_monad (Const (@{const_syntax fcomp}, _) $ f $ g) = 
262 
Const ("_fcomp", dummyT) $ f $ unfold_monad g 

24253  263 
 unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) = 
24195  264 
let 
24253  265 
val ((v, ty), g') = dest_abs_eta g; 
266 
in Const ("_let", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end 

24195  267 
 unfold_monad (Const (@{const_syntax Pair}, _) $ f) = 
21192  268 
Const ("return", dummyT) $ f 
269 
 unfold_monad f = f; 

270 
fun tr' (f::ts) = 

271 
list_comb (Const ("_do", dummyT) $ unfold_monad f, ts) 

22377  272 
in [(@{const_syntax "run"}, tr')] end; 
21192  273 
*} 
274 

24195  275 

21418  276 
subsection {* Combinators *} 
277 

278 
definition 

21601
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21418
diff
changeset

279 
lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> 'b \<times> 'c" where 
21418  280 
"lift f x = return (f x)" 
281 

25765  282 
primrec 
21418  283 
list :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where 
284 
"list f [] = id" 

22492  285 
 "list f (x#xs) = (do f x; list f xs done)" 
21418  286 

25765  287 
primrec 
288 
list_yield :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<times> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'c list \<times> 'b" where 

21418  289 
"list_yield f [] = return []" 
22492  290 
 "list_yield f (x#xs) = (do y \<leftarrow> f x; ys \<leftarrow> list_yield f xs; return (y#ys) done)" 
26141  291 

292 
definition 

26260  293 
collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where 
26141  294 
"collapse f = (do g \<leftarrow> f; g done)" 
295 

21418  296 
text {* combinator properties *} 
297 

298 
lemma list_append [simp]: 

299 
"list f (xs @ ys) = list f xs \<guillemotright> list f ys" 

26141  300 
by (induct xs) (simp_all del: id_apply) 
21418  301 

302 
lemma list_cong [fundef_cong, recdef_cong]: 

303 
"\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk> 

304 
\<Longrightarrow> list f xs = list g ys" 

25765  305 
proof (induct xs arbitrary: ys) 
306 
case Nil then show ?case by simp 

21418  307 
next 
25765  308 
case (Cons x xs) 
309 
from Cons have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto 

21418  310 
then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto 
25765  311 
with Cons have "list f xs = list g xs" by auto 
312 
with Cons have "list f (x # xs) = list g (x # xs)" by auto 

313 
with Cons show "list f (x # xs) = list g ys" by auto 

21418  314 
qed 
315 

316 
lemma list_yield_cong [fundef_cong, recdef_cong]: 

317 
"\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk> 

318 
\<Longrightarrow> list_yield f xs = list_yield g ys" 

25765  319 
proof (induct xs arbitrary: ys) 
320 
case Nil then show ?case by simp 

21418  321 
next 
25765  322 
case (Cons x xs) 
323 
from Cons have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto 

21418  324 
then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto 
25765  325 
with Cons have "list_yield f xs = list_yield g xs" by auto 
326 
with Cons have "list_yield f (x # xs) = list_yield g (x # xs)" by auto 

327 
with Cons show "list_yield f (x # xs) = list_yield g ys" by auto 

21418  328 
qed 
329 

330 
text {* 

24195  331 
For an example, see HOL/ex/Random.thy. 
21192  332 
*} 
333 

22664  334 
end 