--- a/src/HOL/Library/State_Monad.thy Thu Nov 04 13:42:36 2010 +0100
+++ b/src/HOL/Library/State_Monad.thy Thu Nov 04 13:42:36 2010 +0100
@@ -2,7 +2,7 @@
Author: Florian Haftmann, TU Muenchen
*)
-header {* Combinator syntax for generic, open state monads (single threaded monads) *}
+header {* Combinator syntax for generic, open state monads (single-threaded monads) *}
theory State_Monad
imports Main Monad_Syntax
@@ -11,19 +11,18 @@
subsection {* Motivation *}
text {*
- The logic HOL has no notion of constructor classes, so
- it is not possible to model monads the Haskell way
- in full genericity in Isabelle/HOL.
+ The logic HOL has no notion of constructor classes, so it is not
+ possible to model monads the Haskell way in full genericity in
+ Isabelle/HOL.
- However, this theory provides substantial support for
- a very common class of monads: \emph{state monads}
- (or \emph{single-threaded monads}, since a state
- is transformed single-threaded).
+ However, this theory provides substantial support for a very common
+ class of monads: \emph{state monads} (or \emph{single-threaded
+ monads}, since a state is transformed single-threadedly).
To enter from the Haskell world,
- \url{http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm}
- makes a good motivating start. Here we just sketch briefly
- how those monads enter the game of Isabelle/HOL.
+ \url{http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm} makes
+ a good motivating start. Here we just sketch briefly how those
+ monads enter the game of Isabelle/HOL.
*}
subsection {* State transformations and combinators *}
@@ -32,64 +31,66 @@
We classify functions operating on states into two categories:
\begin{description}
- \item[transformations]
- with type signature @{text "\<sigma> \<Rightarrow> \<sigma>'"},
+
+ \item[transformations] with type signature @{text "\<sigma> \<Rightarrow> \<sigma>'"},
transforming a state.
- \item[``yielding'' transformations]
- with type signature @{text "\<sigma> \<Rightarrow> \<alpha> \<times> \<sigma>'"},
- ``yielding'' a side result while transforming a state.
- \item[queries]
- with type signature @{text "\<sigma> \<Rightarrow> \<alpha>"},
- computing a result dependent on a state.
+
+ \item[``yielding'' transformations] with type signature @{text "\<sigma>
+ \<Rightarrow> \<alpha> \<times> \<sigma>'"}, ``yielding'' a side result while transforming a
+ state.
+
+ \item[queries] with type signature @{text "\<sigma> \<Rightarrow> \<alpha>"}, computing a
+ result dependent on a state.
+
\end{description}
- By convention we write @{text "\<sigma>"} for types representing states
- and @{text "\<alpha>"}, @{text "\<beta>"}, @{text "\<gamma>"}, @{text "\<dots>"}
- for types representing side results. Type changes due
- to transformations are not excluded in our scenario.
+ By convention we write @{text "\<sigma>"} for types representing states and
+ @{text "\<alpha>"}, @{text "\<beta>"}, @{text "\<gamma>"}, @{text "\<dots>"} for types
+ representing side results. Type changes due to transformations are
+ not excluded in our scenario.
- We aim to assert that values of any state type @{text "\<sigma>"}
- are used in a single-threaded way: after application
- of a transformation on a value of type @{text "\<sigma>"}, the
- former value should not be used again. To achieve this,
- we use a set of monad combinators:
+ We aim to assert that values of any state type @{text "\<sigma>"} are used
+ in a single-threaded way: after application of a transformation on a
+ value of type @{text "\<sigma>"}, the former value should not be used
+ again. To achieve this, we use a set of monad combinators:
*}
notation fcomp (infixl "\<circ>>" 60)
notation scomp (infixl "\<circ>\<rightarrow>" 60)
-abbreviation (input)
- "return \<equiv> Pair"
-
text {*
- Given two transformations @{term f} and @{term g}, they
- may be directly composed using the @{term "op \<circ>>"} combinator,
- forming a forward composition: @{prop "(f \<circ>> g) s = f (g s)"}.
+ Given two transformations @{term f} and @{term g}, they may be
+ directly composed using the @{term "op \<circ>>"} combinator, forming a
+ forward composition: @{prop "(f \<circ>> g) s = f (g s)"}.
After any yielding transformation, we bind the side result
- immediately using a lambda abstraction. This
- is the purpose of the @{term "op \<circ>\<rightarrow>"} combinator:
- @{prop "(f \<circ>\<rightarrow> (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
+ immediately using a lambda abstraction. This is the purpose of the
+ @{term "op \<circ>\<rightarrow>"} combinator: @{prop "(f \<circ>\<rightarrow> (\<lambda>x. g)) s = (let (x, s')
+ = f s in g s')"}.
For queries, the existing @{term "Let"} is appropriate.
- Naturally, a computation may yield a side result by pairing
- it to the state from the left; we introduce the
- suggestive abbreviation @{term return} for this purpose.
+ Naturally, a computation may yield a side result by pairing it to
+ the state from the left; we introduce the suggestive abbreviation
+ @{term return} for this purpose.
- The most crucial distinction to Haskell is that we do
- not need to introduce distinguished type constructors
- for different kinds of state. This has two consequences:
+ The most crucial distinction to Haskell is that we do not need to
+ introduce distinguished type constructors for different kinds of
+ state. This has two consequences:
+
\begin{itemize}
- \item The monad model does not state anything about
- the kind of state; the model for the state is
- completely orthogonal and may be
- specified completely independently.
- \item There is no distinguished type constructor
- encapsulating away the state transformation, i.e.~transformations
- may be applied directly without using any lifting
- or providing and dropping units (``open monad'').
+
+ \item The monad model does not state anything about the kind of
+ state; the model for the state is completely orthogonal and may
+ be specified completely independently.
+
+ \item There is no distinguished type constructor encapsulating
+ away the state transformation, i.e.~transformations may be
+ applied directly without using any lifting or providing and
+ dropping units (``open monad'').
+
\item The type of states may change due to a transformation.
+
\end{itemize}
*}
@@ -97,8 +98,8 @@
subsection {* Monad laws *}
text {*
- The common monadic laws hold and may also be used
- as normalization rules for monadic expressions:
+ The common monadic laws hold and may also be used as normalization
+ rules for monadic expressions:
*}
lemmas monad_simp = Pair_scomp scomp_Pair id_fcomp fcomp_id
@@ -145,7 +146,7 @@
"_sdo_block (_sdo_final e)" => "e"
text {*
- For an example, see HOL/Extraction/Higman.thy.
+ For an example, see @{text HOL/Proofs/Extraction/Higman.thy}.
*}
end