author haftmann Wed, 12 Mar 2008 08:47:36 +0100 changeset 26260 23ce0d32de11 parent 26141 e1b3a6953cdc child 26266 35ae83ca190a permissions -rw-r--r--
tuned

ID:         $Id$
Author:     Florian Haftmann, TU Muenchen
*)

imports List
begin

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.

However, this theory provides substantial support for
a very common class of monads: \emph{state monads}

To enter from the Haskell world,
makes a good motivating start.  Here we just sketch briefly
how those monads enter the game of Isabelle/HOL.
*}

subsection {* State transformations and combinators *}

(*<*)
typedecl \<alpha>
typedecl \<beta>
typedecl \<gamma>
typedecl \<sigma>
typedecl \<sigma>'
(*>*)

text {*
We classify functions operating on states into two categories:

\begin{description}
\item[transformations]
with type signature @{typ "\<sigma> \<Rightarrow> \<sigma>'"},
transforming a state.
\item[yielding'' transformations]
with type signature @{typ "\<sigma> \<Rightarrow> \<alpha> \<times> \<sigma>'"},
yielding'' a side result while transforming a state.
\item[queries]
with type signature @{typ "\<sigma> \<Rightarrow> \<alpha>"},
computing a result dependent on a state.
\end{description}

By convention we write @{typ "\<sigma>"} for types representing states
and @{typ "\<alpha>"}, @{typ "\<beta>"}, @{typ "\<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 @{typ "\<sigma>"}
are used in a single-threaded way: after application
of a transformation on a value of type @{typ "\<sigma>"}, the
former value should not be used again.  To achieve this,
we use a set of monad combinators:
*}

definition
mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
(infixl ">>=" 60) where
"f >>= g = split g \<circ> f"

definition
fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"
(infixl ">>" 60) where
"f >> g = g \<circ> f"

definition
run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
"run f = f"

syntax (xsymbols)
mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
(infixl "\<guillemotright>=" 60)
fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"
(infixl "\<guillemotright>" 60)

abbreviation (input)
"return \<equiv> Pair"

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

text {*
Given two transformations @{term f} and @{term g}, they
may be directly composed using the @{term "op \<guillemotright>"} combinator,
forming a forward composition: @{prop "(f \<guillemotright> 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 \<guillemotright>="} combinator:
@{prop "(f \<guillemotright>= (\<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.

The @{const run} ist just a marker.

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 type of states may change due to a transformation.
\end{itemize}
*}

subsection {* Obsolete runs *}

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

lemma run_simp [simp]:
"\<And>f. run (run f) = run f"
"\<And>f g. run f \<guillemotright>= g = f \<guillemotright>= g"
"\<And>f g. run f \<guillemotright> g = f \<guillemotright> g"
"\<And>f g. f \<guillemotright>= (\<lambda>x. run g) = f \<guillemotright>= (\<lambda>x. g)"
"\<And>f g. f \<guillemotright> run g = f \<guillemotright> g"
"\<And>f. f = run f \<longleftrightarrow> True"
"\<And>f. run f = f \<longleftrightarrow> True"
unfolding run_def by rule+

subsection {* Monad laws *}

text {*
The common monadic laws hold and may also be used
as normalization rules for monadic expressions:
*}

lemma
return_mbind [simp]: "return x \<guillemotright>= f = f x"
unfolding mbind_def by (simp add: expand_fun_eq)

lemma
mbind_return [simp]: "x \<guillemotright>= return = x"
unfolding mbind_def by (simp add: expand_fun_eq split_Pair)

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

lemma
fcomp_id [simp]: "f \<guillemotright> id = f"
unfolding fcomp_def by simp

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

lemma
mbind_fcomp [simp]: "(f \<guillemotright>= g) \<guillemotright> h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright> h)"
unfolding mbind_def fcomp_def by (simp add: split_def expand_fun_eq)

lemma
fcomp_mbind [simp]: "(f \<guillemotright> g) \<guillemotright>= h = f \<guillemotright> (g \<guillemotright>= h)"
unfolding mbind_def fcomp_def by (simp add: split_def expand_fun_eq)

lemma
fcomp_fcomp [simp]: "(f \<guillemotright> g) \<guillemotright> h = f \<guillemotright> (g \<guillemotright> h)"
unfolding fcomp_def o_assoc ..

lemmas monad_simp = run_simp return_mbind mbind_return id_fcomp fcomp_id
mbind_mbind mbind_fcomp fcomp_mbind fcomp_fcomp

text {*
Evaluation of monadic expressions by force:
*}

lemmas monad_collapse = monad_simp o_apply o_assoc split_Pair split_comp
mbind_def fcomp_def run_def

subsection {* ML abstract operations *}

ML {*
struct

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

fun return T sT x = Const (@{const_name return}, T --> liftT T sT) $x; fun mbind T1 T2 sT f g = Const (@{const_name mbind}, liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT)$ f $g; fun run T sT f = Const (@{const_name run}, liftT' (liftT T sT))$ f;

end;
*}

subsection {* Syntax *}

text {*
We provide a convenient do-notation for monadic expressions
well-known from Haskell.  @{const Let} is printed
specially in do-expressions.
*}

nonterminals do_expr

syntax
"_do" :: "do_expr \<Rightarrow> 'a"
("do _ done" [12] 12)
"_mbind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
("_ <- _;// _" [1000, 13, 12] 12)
"_fcomp" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
("_;// _" [13, 12] 12)
"_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
("let _ = _;// _" [1000, 13, 12] 12)
"_nil" :: "'a \<Rightarrow> do_expr"
("_" [12] 12)

syntax (xsymbols)
"_mbind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
("_ \<leftarrow> _;// _" [1000, 13, 12] 12)

translations
"_do f" => "CONST run f"
"_mbind x f g" => "f \<guillemotright>= (\<lambda>x. g)"
"_fcomp f g" => "f \<guillemotright> g"
"_let x t f" => "CONST Let t (\<lambda>x. f)"
"_nil f" => "f"

print_translation {*
let
fun dest_abs_eta (Abs (abs as (_, ty, _))) =
let
val (v, t) = Syntax.variant_abs abs;
in ((v, ty), t) end
| dest_abs_eta t =
let
val (v, t) = Syntax.variant_abs ("", dummyT, t $Bound 0); in ((v, dummyT), t) end fun unfold_monad (Const (@{const_syntax mbind}, _)$ f $g) = let val ((v, ty), g') = dest_abs_eta g; in Const ("_mbind", dummyT)$ Free (v, ty) $f$ unfold_monad g' end
| unfold_monad (Const (@{const_syntax fcomp}, _) $f$ g) =
Const ("_fcomp", dummyT) $f$ unfold_monad g
| unfold_monad (Const (@{const_syntax Let}, _) $f$ g) =
let
val ((v, ty), g') = dest_abs_eta g;
in Const ("_let", dummyT) $Free (v, ty)$ f $unfold_monad g' end | unfold_monad (Const (@{const_syntax Pair}, _)$ f) =
Const ("return", dummyT) $f | unfold_monad f = f; fun tr' (f::ts) = list_comb (Const ("_do", dummyT)$ unfold_monad f, ts)
in [(@{const_syntax "run"}, tr')] end;
*}

subsection {* Combinators *}

definition
lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> 'b \<times> 'c" where
"lift f x = return (f x)"

primrec
list :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
"list f [] = id"
| "list f (x#xs) = (do f x; list f xs done)"

primrec
list_yield :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<times> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'c list \<times> 'b" where
"list_yield f [] = return []"
| "list_yield f (x#xs) = (do y \<leftarrow> f x; ys \<leftarrow> list_yield f xs; return (y#ys) done)"

definition
collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
"collapse f = (do g \<leftarrow> f; g done)"

text {* combinator properties *}

lemma list_append [simp]:
"list f (xs @ ys) = list f xs \<guillemotright> list f ys"
by (induct xs) (simp_all del: id_apply)

lemma list_cong [fundef_cong, recdef_cong]:
"\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk>
\<Longrightarrow> list f xs = list g ys"
proof (induct xs arbitrary: ys)
case Nil then show ?case by simp
next
case (Cons x xs)
from Cons have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto
then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto
with Cons have "list f xs = list g xs" by auto
with Cons have "list f (x # xs) = list g (x # xs)" by auto
with Cons show "list f (x # xs) = list g ys" by auto
qed

lemma list_yield_cong [fundef_cong, recdef_cong]:
"\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk>
\<Longrightarrow> list_yield f xs = list_yield g ys"
proof (induct xs arbitrary: ys)
case Nil then show ?case by simp
next
case (Cons x xs)
from Cons have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto
then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto
with Cons have "list_yield f xs = list_yield g xs" by auto
with Cons have "list_yield f (x # xs) = list_yield g (x # xs)" by auto
with Cons show "list_yield f (x # xs) = list_yield g ys" by auto
qed

text {*
For an example, see HOL/ex/Random.thy.
*}

end