author bulwahn Fri Apr 08 16:31:14 2011 +0200 (2011-04-08) changeset 42316 12635bb655fd parent 41229 d797baa3d57c child 54703 499f92dc6e45 permissions -rw-r--r--
deactivating other compilations in quickcheck_exhaustive momentarily that only interesting for my benchmarks and experiments
1 (*  Title:      HOL/Library/State_Monad.thy
2     Author:     Florian Haftmann, TU Muenchen
3 *)
8 imports Main Monad_Syntax
9 begin
11 subsection {* Motivation *}
13 text {*
14   The logic HOL has no notion of constructor classes, so it is not
15   possible to model monads the Haskell way in full genericity in
16   Isabelle/HOL.
18   However, this theory provides substantial support for a very common
20   monads}, since a state is transformed single-threadedly).
22   To enter from the Haskell world,
24   a good motivating start.  Here we just sketch briefly how those
25   monads enter the game of Isabelle/HOL.
26 *}
28 subsection {* State transformations and combinators *}
30 text {*
31   We classify functions operating on states into two categories:
33   \begin{description}
35     \item[transformations] with type signature @{text "\<sigma> \<Rightarrow> \<sigma>'"},
36       transforming a state.
38     \item[yielding'' transformations] with type signature @{text "\<sigma>
39       \<Rightarrow> \<alpha> \<times> \<sigma>'"}, yielding'' a side result while transforming a
40       state.
42     \item[queries] with type signature @{text "\<sigma> \<Rightarrow> \<alpha>"}, computing a
43       result dependent on a state.
45   \end{description}
47   By convention we write @{text "\<sigma>"} for types representing states and
48   @{text "\<alpha>"}, @{text "\<beta>"}, @{text "\<gamma>"}, @{text "\<dots>"} for types
49   representing side results.  Type changes due to transformations are
50   not excluded in our scenario.
52   We aim to assert that values of any state type @{text "\<sigma>"} are used
53   in a single-threaded way: after application of a transformation on a
54   value of type @{text "\<sigma>"}, the former value should not be used
55   again.  To achieve this, we use a set of monad combinators:
56 *}
58 notation fcomp (infixl "\<circ>>" 60)
59 notation scomp (infixl "\<circ>\<rightarrow>" 60)
61 text {*
62   Given two transformations @{term f} and @{term g}, they may be
63   directly composed using the @{term "op \<circ>>"} combinator, forming a
64   forward composition: @{prop "(f \<circ>> g) s = f (g s)"}.
66   After any yielding transformation, we bind the side result
67   immediately using a lambda abstraction.  This is the purpose of the
68   @{term "op \<circ>\<rightarrow>"} combinator: @{prop "(f \<circ>\<rightarrow> (\<lambda>x. g)) s = (let (x, s')
69   = f s in g s')"}.
71   For queries, the existing @{term "Let"} is appropriate.
73   Naturally, a computation may yield a side result by pairing it to
74   the state from the left; we introduce the suggestive abbreviation
75   @{term return} for this purpose.
77   The most crucial distinction to Haskell is that we do not need to
78   introduce distinguished type constructors for different kinds of
79   state.  This has two consequences:
81   \begin{itemize}
83     \item The monad model does not state anything about the kind of
84        state; the model for the state is completely orthogonal and may
85        be specified completely independently.
87     \item There is no distinguished type constructor encapsulating
88        away the state transformation, i.e.~transformations may be
89        applied directly without using any lifting or providing and
90        dropping units (open monad'').
92     \item The type of states may change due to a transformation.
94   \end{itemize}
95 *}
98 subsection {* Monad laws *}
100 text {*
101   The common monadic laws hold and may also be used as normalization
102   rules for monadic expressions:
103 *}
105 lemmas monad_simp = Pair_scomp scomp_Pair id_fcomp fcomp_id
106   scomp_scomp scomp_fcomp fcomp_scomp fcomp_assoc
108 text {*
109   Evaluation of monadic expressions by force:
110 *}
112 lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta
115 subsection {* Do-syntax *}
117 nonterminal sdo_binds and sdo_bind
119 syntax
120   "_sdo_block" :: "sdo_binds \<Rightarrow> 'a" ("exec {//(2  _)//}"  62)
121   "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ <-/ _)" 13)
122   "_sdo_let" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(2let _ =/ _)" [1000, 13] 13)
123   "_sdo_then" :: "'a \<Rightarrow> sdo_bind" ("_"  13)
124   "_sdo_final" :: "'a \<Rightarrow> sdo_binds" ("_")
125   "_sdo_cons" :: "[sdo_bind, sdo_binds] \<Rightarrow> sdo_binds" ("_;//_" [13, 12] 12)
127 syntax (xsymbols)
128   "_sdo_bind"  :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ \<leftarrow>/ _)" 13)
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))"
134     => "CONST fcomp t e"
135   "_sdo_final (_sdo_block (_sdo_cons (_sdo_then t) (_sdo_final e)))"
136     <= "_sdo_final (CONST fcomp t e)"
137   "_sdo_block (_sdo_cons (_sdo_then t) e)"
138     <= "CONST fcomp t (_sdo_block e)"
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"
147 text {*
148   For an example, see @{text "HOL/Proofs/Extraction/Higman.thy"}.
149 *}
151 end