author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 63680  6e1e8b5abbfa 
child 66258  2b83dd24b301 
permissions  rwrr 
21192  1 
(* Title: HOL/Library/State_Monad.thy 
2 
Author: Florian Haftmann, TU Muenchen 

3 
*) 

4 

60500  5 
section \<open>Combinator syntax for generic, open state monads (singlethreaded monads)\<close> 
21192  6 

7 
theory State_Monad 

37932  8 
imports Main Monad_Syntax 
21192  9 
begin 
10 

60500  11 
subsection \<open>Motivation\<close> 
21192  12 

60500  13 
text \<open> 
40359
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

14 
The logic HOL has no notion of constructor classes, so it is not 
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

15 
possible to model monads the Haskell way in full genericity in 
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

16 
Isabelle/HOL. 
21192  17 

40359
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

18 
However, this theory provides substantial support for a very common 
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

19 
class of monads: \emph{state monads} (or \emph{singlethreaded 
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

20 
monads}, since a state is transformed singlethreadedly). 
21192  21 

22 
To enter from the Haskell world, 

63680  23 
\<^url>\<open>http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm\<close> makes 
40359
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

24 
a good motivating start. Here we just sketch briefly how those 
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

25 
monads enter the game of Isabelle/HOL. 
60500  26 
\<close> 
21192  27 

60500  28 
subsection \<open>State transformations and combinators\<close> 
21192  29 

60500  30 
text \<open> 
21192  31 
We classify functions operating on states into two categories: 
32 

33 
\begin{description} 

40359
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

34 

61585  35 
\item[transformations] with type signature \<open>\<sigma> \<Rightarrow> \<sigma>'\<close>, 
21192  36 
transforming a state. 
40359
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

37 

61585  38 
\item[``yielding'' transformations] with type signature \<open>\<sigma> 
39 
\<Rightarrow> \<alpha> \<times> \<sigma>'\<close>, ``yielding'' a side result while transforming a 

40359
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

40 
state. 
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

41 

61585  42 
\item[queries] with type signature \<open>\<sigma> \<Rightarrow> \<alpha>\<close>, computing a 
40359
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

43 
result dependent on a state. 
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

44 

21192  45 
\end{description} 
46 

61585  47 
By convention we write \<open>\<sigma>\<close> for types representing states and 
48 
\<open>\<alpha>\<close>, \<open>\<beta>\<close>, \<open>\<gamma>\<close>, \<open>\<dots>\<close> for types 

40359
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

49 
representing side results. Type changes due to transformations are 
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

50 
not excluded in our scenario. 
21192  51 

61585  52 
We aim to assert that values of any state type \<open>\<sigma>\<close> are used 
40359
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

53 
in a singlethreaded way: after application of a transformation on a 
61585  54 
value of type \<open>\<sigma>\<close>, the former value should not be used 
40359
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

55 
again. To achieve this, we use a set of monad combinators: 
60500  56 
\<close> 
21192  57 

37751  58 
notation fcomp (infixl "\<circ>>" 60) 
37817  59 
notation scomp (infixl "\<circ>\<rightarrow>" 60) 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21283
diff
changeset

60 

60500  61 
text \<open> 
40359
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

62 
Given two transformations @{term f} and @{term g}, they may be 
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

63 
directly composed using the @{term "op \<circ>>"} combinator, forming a 
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

64 
forward composition: @{prop "(f \<circ>> g) s = f (g s)"}. 
21192  65 

66 
After any yielding transformation, we bind the side result 

40359
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

67 
immediately using a lambda abstraction. This is the purpose of the 
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

68 
@{term "op \<circ>\<rightarrow>"} combinator: @{prop "(f \<circ>\<rightarrow> (\<lambda>x. g)) s = (let (x, s') 
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

69 
= f s in g s')"}. 
21192  70 

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

72 

40359
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

73 
Naturally, a computation may yield a side result by pairing it to 
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

74 
the state from the left; we introduce the suggestive abbreviation 
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

75 
@{term return} for this purpose. 
21192  76 

40359
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

77 
The most crucial distinction to Haskell is that we do not need to 
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

78 
introduce distinguished type constructors for different kinds of 
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

79 
state. This has two consequences: 
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

80 

21192  81 
\begin{itemize} 
40359
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

82 

84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

83 
\item The monad model does not state anything about the kind of 
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

84 
state; the model for the state is completely orthogonal and may 
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

85 
be specified completely independently. 
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

86 

84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

87 
\item There is no distinguished type constructor encapsulating 
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

88 
away the state transformation, i.e.~transformations may be 
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

89 
applied directly without using any lifting or providing and 
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

90 
dropping units (``open monad''). 
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

91 

21192  92 
\item The type of states may change due to a transformation. 
40359
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

93 

21192  94 
\end{itemize} 
60500  95 
\<close> 
21192  96 

97 

60500  98 
subsection \<open>Monad laws\<close> 
21192  99 

60500  100 
text \<open> 
40359
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

101 
The common monadic laws hold and may also be used as normalization 
84388bba911d
dropped return abbreviation for Pair  confusing if combined with monad syntax; tuned document
haftmann
parents:
38345
diff
changeset

102 
rules for monadic expressions: 
60500  103 
\<close> 
21192  104 

28145  105 
lemmas monad_simp = Pair_scomp scomp_Pair id_fcomp fcomp_id 
106 
scomp_scomp scomp_fcomp fcomp_scomp fcomp_assoc 

21192  107 

60500  108 
text \<open> 
21192  109 
Evaluation of monadic expressions by force: 
60500  110 
\<close> 
21192  111 

28145  112 
lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta 
26260  113 

37817  114 

60500  115 
subsection \<open>Dosyntax\<close> 
37817  116 

41229
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
40361
diff
changeset

117 
nonterminal sdo_binds and sdo_bind 
37932  118 

119 
syntax 

120 
"_sdo_block" :: "sdo_binds \<Rightarrow> 'a" ("exec {//(2 _)//}" [12] 62) 

61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61585
diff
changeset

121 
"_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ \<leftarrow>/ _)" 13) 
37932  122 
"_sdo_let" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(2let _ =/ _)" [1000, 13] 13) 
123 
"_sdo_then" :: "'a \<Rightarrow> sdo_bind" ("_" [14] 13) 

124 
"_sdo_final" :: "'a \<Rightarrow> sdo_binds" ("_") 

125 
"_sdo_cons" :: "[sdo_bind, sdo_binds] \<Rightarrow> sdo_binds" ("_;//_" [13, 12] 12) 

21192  126 

61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61585
diff
changeset

127 
syntax (ASCII) 
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61585
diff
changeset

128 
"_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ </ _)" 13) 
37932  129 

130 
translations 

131 
"_sdo_block (_sdo_cons (_sdo_bind p t) (_sdo_final e))" 

132 
== "CONST scomp t (\<lambda>p. e)" 

133 
"_sdo_block (_sdo_cons (_sdo_then t) (_sdo_final e))" 

38345
8b8fc27c1872
print fcomp combinator only monadic in connection with other monadic expressions
haftmann
parents:
37932
diff
changeset

134 
=> "CONST fcomp t e" 
8b8fc27c1872
print fcomp combinator only monadic in connection with other monadic expressions
haftmann
parents:
37932
diff
changeset

135 
"_sdo_final (_sdo_block (_sdo_cons (_sdo_then t) (_sdo_final e)))" 
8b8fc27c1872
print fcomp combinator only monadic in connection with other monadic expressions
haftmann
parents:
37932
diff
changeset

136 
<= "_sdo_final (CONST fcomp t e)" 
8b8fc27c1872
print fcomp combinator only monadic in connection with other monadic expressions
haftmann
parents:
37932
diff
changeset

137 
"_sdo_block (_sdo_cons (_sdo_then t) e)" 
8b8fc27c1872
print fcomp combinator only monadic in connection with other monadic expressions
haftmann
parents:
37932
diff
changeset

138 
<= "CONST fcomp t (_sdo_block e)" 
37932  139 
"_sdo_block (_sdo_cons (_sdo_let p t) bs)" 
140 
== "let p = t in _sdo_block bs" 

141 
"_sdo_block (_sdo_cons b (_sdo_cons c cs))" 

142 
== "_sdo_block (_sdo_cons b (_sdo_final (_sdo_block (_sdo_cons c cs))))" 

143 
"_sdo_cons (_sdo_let p t) (_sdo_final s)" 

144 
== "_sdo_final (let p = t in s)" 

145 
"_sdo_block (_sdo_final e)" => "e" 

37817  146 

60500  147 
text \<open> 
63680  148 
For an example, see \<^file>\<open>~~/src/HOL/Proofs/Extraction/Higman_Extraction.thy\<close>. 
60500  149 
\<close> 
21192  150 

22664  151 
end 