author haftmann Thu Jun 26 10:07:01 2008 +0200 (2008-06-26) changeset 27368 9f90ac19e32b parent 26588 d83271bfaba5 child 27487 c8a6ce181805 permissions -rw-r--r--
established Plain theory and image
     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

     9 imports Plain List

    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{single-threaded monads}, since a state

    22   is transformed single-threaded).

    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 text {*

    33   We classify functions operating on states into two categories:

    34

    35   \begin{description}

    36     \item[transformations]

    37       with type signature @{text "\<sigma> \<Rightarrow> \<sigma>'"},

    38       transforming a state.

    39     \item[yielding'' transformations]

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

    41       yielding'' a side result while transforming a state.

    42     \item[queries]

    43       with type signature @{text "\<sigma> \<Rightarrow> \<alpha>"},

    44       computing a result dependent on a state.

    45   \end{description}

    46

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

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

    49   for types representing side results.  Type changes due

    50   to transformations are not excluded in our scenario.

    51

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

    53   are used in a single-threaded way: after application

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

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

    56   we use a set of monad combinators:

    57 *}

    58

    59 notation fcomp (infixl ">>" 60)

    60 notation (xsymbols) fcomp (infixl "\<guillemotright>" 60)

    61 notation scomp (infixl ">>=" 60)

    62 notation (xsymbols) scomp (infixl "\<guillemotright>=" 60)

    63

    64 abbreviation (input)

    65   "return \<equiv> Pair"

    66

    67 definition

    68   run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where

    69   "run f = f"

    70

    71 print_ast_translation {*

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

    73 *}

    74

    75 text {*

    76   Given two transformations @{term f} and @{term g}, they

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

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

    79

    80   After any yielding transformation, we bind the side result

    81   immediately using a lambda abstraction.  This

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

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

    84

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

    86

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

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

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

    90

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

    92

    93   The most crucial distinction to Haskell is that we do

    94   not need to introduce distinguished type constructors

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

    96   \begin{itemize}

    97     \item The monad model does not state anything about

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

    99        completely orthogonal and may be

   100        specified completely independently.

   101     \item There is no distinguished type constructor

   102        encapsulating away the state transformation, i.e.~transformations

   103        may be applied directly without using any lifting

   104        or providing and dropping units (open monad'').

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

   106   \end{itemize}

   107 *}

   108

   109

   110 subsection {* Obsolete runs *}

   111

   112 text {*

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

   114 *}

   115

   116 lemma run_simp [simp]:

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

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

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

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

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

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

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

   124   unfolding run_def by rule+

   125

   126 subsection {* Monad laws *}

   127

   128 text {*

   129   The common monadic laws hold and may also be used

   130   as normalization rules for monadic expressions:

   131 *}

   132

   133 lemma

   134   return_scomp [simp]: "return x \<guillemotright>= f = f x"

   135   unfolding scomp_def by (simp add: expand_fun_eq)

   136

   137 lemma

   138   scomp_return [simp]: "x \<guillemotright>= return = x"

   139   unfolding scomp_def by (simp add: expand_fun_eq split_Pair)

   140

   141 lemma

   142   id_fcomp [simp]: "id \<guillemotright> f = f"

   143   unfolding fcomp_def by simp

   144

   145 lemma

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

   147   unfolding fcomp_def by simp

   148

   149 lemma

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

   151   unfolding scomp_def by (simp add: split_def expand_fun_eq)

   152

   153 lemma

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

   155   unfolding scomp_def fcomp_def by (simp add: split_def expand_fun_eq)

   156

   157 lemma

   158   fcomp_scomp [simp]: "(f \<guillemotright> g) \<guillemotright>= h = f \<guillemotright> (g \<guillemotright>= h)"

   159   unfolding scomp_def fcomp_def by (simp add: split_def expand_fun_eq)

   160

   161 lemma

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

   163   unfolding fcomp_def o_assoc ..

   164

   165 lemmas monad_simp = run_simp return_scomp scomp_return id_fcomp fcomp_id

   166   scomp_scomp scomp_fcomp fcomp_scomp fcomp_fcomp

   167

   168 text {*

   169   Evaluation of monadic expressions by force:

   170 *}

   171

   172 lemmas monad_collapse = monad_simp o_apply o_assoc split_Pair split_comp

   173   scomp_def fcomp_def run_def

   174

   175 subsection {* ML abstract operations *}

   176

   177 ML {*

   178 structure StateMonad =

   179 struct

   180

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

   182 fun liftT' sT = sT --> sT;

   183

   184 fun return T sT x = Const (@{const_name return}, T --> liftT T sT) $x;   185   186 fun scomp T1 T2 sT f g = Const (@{const_name scomp},   187 liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT)$ f $g;   188   189 fun run T sT f = Const (@{const_name run}, liftT' (liftT T sT))$ f;

   190

   191 end;

   192 *}

   193

   194

   195 subsection {* Syntax *}

   196

   197 text {*

   198   We provide a convenient do-notation for monadic expressions

   199   well-known from Haskell.  @{const Let} is printed

   200   specially in do-expressions.

   201 *}

   202

   203 nonterminals do_expr

   204

   205 syntax

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

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

   208   "_scomp" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"

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

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

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

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

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

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

   215     ("_" [12] 12)

   216

   217 syntax (xsymbols)

   218   "_scomp" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"

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

   220

   221 translations

   222   "_do f" => "CONST run f"

   223   "_scomp x f g" => "f \<guillemotright>= (\<lambda>x. g)"

   224   "_fcomp f g" => "f \<guillemotright> g"

   225   "_let x t f" => "CONST Let t (\<lambda>x. f)"

   226   "_nil f" => "f"

   227

   228 print_translation {*

   229 let

   230   fun dest_abs_eta (Abs (abs as (_, ty, _))) =

   231         let

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

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

   234     | dest_abs_eta t =

   235         let

   236           val (v, t) = Syntax.variant_abs ("", dummyT, t $Bound 0);   237 in ((v, dummyT), t) end   238 fun unfold_monad (Const (@{const_syntax scomp}, _)$ f $g) =   239 let   240 val ((v, ty), g') = dest_abs_eta g;   241 in Const ("_scomp", dummyT)$ Free (v, ty) $f$ unfold_monad g' end

   242     | unfold_monad (Const (@{const_syntax fcomp}, _) $f$ g) =

   243         Const ("_fcomp", dummyT) $f$ unfold_monad g

   244     | unfold_monad (Const (@{const_syntax Let}, _) $f$ g) =

   245         let

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

   247         in Const ("_let", dummyT) $Free (v, ty)$ f $unfold_monad g' end   248 | unfold_monad (Const (@{const_syntax Pair}, _)$ f) =

   249         Const ("return", dummyT) $f   250 | unfold_monad f = f;   251 fun tr' (f::ts) =   252 list_comb (Const ("_do", dummyT)$ unfold_monad f, ts)

   253 in [(@{const_syntax "run"}, tr')] end;

   254 *}

   255

   256

   257 subsection {* Combinators *}

   258

   259 definition

   260   lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> 'b \<times> 'c" where

   261   "lift f x = return (f x)"

   262

   263 primrec

   264   list :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where

   265   "list f [] = id"

   266 | "list f (x#xs) = (do f x; list f xs done)"

   267

   268 primrec

   269   list_yield :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<times> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'c list \<times> 'b" where

   270   "list_yield f [] = return []"

   271 | "list_yield f (x#xs) = (do y \<leftarrow> f x; ys \<leftarrow> list_yield f xs; return (y#ys) done)"

   272

   273 definition

   274   collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where

   275   "collapse f = (do g \<leftarrow> f; g done)"

   276

   277 text {* combinator properties *}

   278

   279 lemma list_append [simp]:

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

   281   by (induct xs) (simp_all del: id_apply)

   282

   283 lemma list_cong [fundef_cong, recdef_cong]:

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

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

   286 proof (induct xs arbitrary: ys)

   287   case Nil then show ?case by simp

   288 next

   289   case (Cons x xs)

   290   from Cons have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto

   291   then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto

   292   with Cons have "list f xs = list g xs" by auto

   293   with Cons have "list f (x # xs) = list g (x # xs)" by auto

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

   295 qed

   296

   297 lemma list_yield_cong [fundef_cong, recdef_cong]:

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

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

   300 proof (induct xs arbitrary: ys)

   301   case Nil then show ?case by simp

   302 next

   303   case (Cons x xs)

   304   from Cons have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto

   305   then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto

   306   with Cons have "list_yield f xs = list_yield g xs" by auto

   307   with Cons have "list_yield f (x # xs) = list_yield g (x # xs)" by auto

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

   309 qed

   310

   311 text {*

   312   For an example, see HOL/ex/Random.thy.

   313 *}

   314

   315 end