src/HOL/Library/State_Monad.thy
author haftmann
Fri Mar 14 08:52:51 2008 +0100 (2008-03-14)
changeset 26266 35ae83ca190a
parent 26260 23ce0d32de11
child 26588 d83271bfaba5
permissions -rw-r--r--
tuned
     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 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 definition
    60   mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
    61     (infixl ">>=" 60) where
    62   "f >>= g = split g \<circ> f"
    63 
    64 definition
    65   fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"
    66     (infixl ">>" 60) where
    67   "f >> g = g \<circ> f"
    68 
    69 definition
    70   run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    71   "run f = f"
    72 
    73 syntax (xsymbols)
    74   mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
    75     (infixl "\<guillemotright>=" 60)
    76   fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"
    77     (infixl "\<guillemotright>" 60)
    78 
    79 abbreviation (input)
    80   "return \<equiv> Pair"
    81 
    82 print_ast_translation {*
    83   [(@{const_syntax "run"}, fn (f::ts) => Syntax.mk_appl f ts)]
    84 *}
    85 
    86 text {*
    87   Given two transformations @{term f} and @{term g}, they
    88   may be directly composed using the @{term "op \<guillemotright>"} combinator,
    89   forming a forward composition: @{prop "(f \<guillemotright> g) s = f (g s)"}.
    90 
    91   After any yielding transformation, we bind the side result
    92   immediately using a lambda abstraction.  This 
    93   is the purpose of the @{term "op \<guillemotright>="} combinator:
    94   @{prop "(f \<guillemotright>= (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
    95 
    96   For queries, the existing @{term "Let"} is appropriate.
    97 
    98   Naturally, a computation may yield a side result by pairing
    99   it to the state from the left;  we introduce the
   100   suggestive abbreviation @{term return} for this purpose.
   101 
   102   The @{const run} ist just a marker.
   103 
   104   The most crucial distinction to Haskell is that we do
   105   not need to introduce distinguished type constructors
   106   for different kinds of state.  This has two consequences:
   107   \begin{itemize}
   108     \item The monad model does not state anything about
   109        the kind of state; the model for the state is
   110        completely orthogonal and may be
   111        specified completely independently.
   112     \item There is no distinguished type constructor
   113        encapsulating away the state transformation, i.e.~transformations
   114        may be applied directly without using any lifting
   115        or providing and dropping units (``open monad'').
   116     \item The type of states may change due to a transformation.
   117   \end{itemize}
   118 *}
   119 
   120 
   121 subsection {* Obsolete runs *}
   122 
   123 text {*
   124   @{term run} is just a doodle and should not occur nested:
   125 *}
   126 
   127 lemma run_simp [simp]:
   128   "\<And>f. run (run f) = run f"
   129   "\<And>f g. run f \<guillemotright>= g = f \<guillemotright>= g"
   130   "\<And>f g. run f \<guillemotright> g = f \<guillemotright> g"
   131   "\<And>f g. f \<guillemotright>= (\<lambda>x. run g) = f \<guillemotright>= (\<lambda>x. g)"
   132   "\<And>f g. f \<guillemotright> run g = f \<guillemotright> g"
   133   "\<And>f. f = run f \<longleftrightarrow> True"
   134   "\<And>f. run f = f \<longleftrightarrow> True"
   135   unfolding run_def by rule+
   136 
   137 subsection {* Monad laws *}
   138 
   139 text {*
   140   The common monadic laws hold and may also be used
   141   as normalization rules for monadic expressions:
   142 *}
   143 
   144 lemma
   145   return_mbind [simp]: "return x \<guillemotright>= f = f x"
   146   unfolding mbind_def by (simp add: expand_fun_eq)
   147 
   148 lemma
   149   mbind_return [simp]: "x \<guillemotright>= return = x"
   150   unfolding mbind_def by (simp add: expand_fun_eq split_Pair)
   151 
   152 lemma
   153   id_fcomp [simp]: "id \<guillemotright> f = f"
   154   unfolding fcomp_def by simp
   155 
   156 lemma
   157   fcomp_id [simp]: "f \<guillemotright> id = f"
   158   unfolding fcomp_def by simp
   159 
   160 lemma
   161   mbind_mbind [simp]: "(f \<guillemotright>= g) \<guillemotright>= h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h)"
   162   unfolding mbind_def by (simp add: split_def expand_fun_eq)
   163 
   164 lemma
   165   mbind_fcomp [simp]: "(f \<guillemotright>= g) \<guillemotright> h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright> h)"
   166   unfolding mbind_def fcomp_def by (simp add: split_def expand_fun_eq)
   167 
   168 lemma
   169   fcomp_mbind [simp]: "(f \<guillemotright> g) \<guillemotright>= h = f \<guillemotright> (g \<guillemotright>= h)"
   170   unfolding mbind_def fcomp_def by (simp add: split_def expand_fun_eq)
   171 
   172 lemma
   173   fcomp_fcomp [simp]: "(f \<guillemotright> g) \<guillemotright> h = f \<guillemotright> (g \<guillemotright> h)"
   174   unfolding fcomp_def o_assoc ..
   175 
   176 lemmas monad_simp = run_simp return_mbind mbind_return id_fcomp fcomp_id
   177   mbind_mbind mbind_fcomp fcomp_mbind fcomp_fcomp
   178 
   179 text {*
   180   Evaluation of monadic expressions by force:
   181 *}
   182 
   183 lemmas monad_collapse = monad_simp o_apply o_assoc split_Pair split_comp
   184   mbind_def fcomp_def run_def
   185 
   186 subsection {* ML abstract operations *}
   187 
   188 ML {*
   189 structure StateMonad =
   190 struct
   191 
   192 fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
   193 fun liftT' sT = sT --> sT;
   194 
   195 fun return T sT x = Const (@{const_name return}, T --> liftT T sT) $ x;
   196 
   197 fun mbind T1 T2 sT f g = Const (@{const_name mbind},
   198   liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
   199 
   200 fun run T sT f = Const (@{const_name run}, liftT' (liftT T sT)) $ f;
   201 
   202 end;
   203 *}
   204 
   205 
   206 subsection {* Syntax *}
   207 
   208 text {*
   209   We provide a convenient do-notation for monadic expressions
   210   well-known from Haskell.  @{const Let} is printed
   211   specially in do-expressions.
   212 *}
   213 
   214 nonterminals do_expr
   215 
   216 syntax
   217   "_do" :: "do_expr \<Rightarrow> 'a"
   218     ("do _ done" [12] 12)
   219   "_mbind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   220     ("_ <- _;// _" [1000, 13, 12] 12)
   221   "_fcomp" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   222     ("_;// _" [13, 12] 12)
   223   "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   224     ("let _ = _;// _" [1000, 13, 12] 12)
   225   "_nil" :: "'a \<Rightarrow> do_expr"
   226     ("_" [12] 12)
   227 
   228 syntax (xsymbols)
   229   "_mbind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   230     ("_ \<leftarrow> _;// _" [1000, 13, 12] 12)
   231 
   232 translations
   233   "_do f" => "CONST run f"
   234   "_mbind x f g" => "f \<guillemotright>= (\<lambda>x. g)"
   235   "_fcomp f g" => "f \<guillemotright> g"
   236   "_let x t f" => "CONST Let t (\<lambda>x. f)"
   237   "_nil f" => "f"
   238 
   239 print_translation {*
   240 let
   241   fun dest_abs_eta (Abs (abs as (_, ty, _))) =
   242         let
   243           val (v, t) = Syntax.variant_abs abs;
   244         in ((v, ty), t) end
   245     | dest_abs_eta t =
   246         let
   247           val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);
   248         in ((v, dummyT), t) end
   249   fun unfold_monad (Const (@{const_syntax mbind}, _) $ f $ g) =
   250         let
   251           val ((v, ty), g') = dest_abs_eta g;
   252         in Const ("_mbind", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
   253     | unfold_monad (Const (@{const_syntax fcomp}, _) $ f $ g) =
   254         Const ("_fcomp", dummyT) $ f $ unfold_monad g
   255     | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
   256         let
   257           val ((v, ty), g') = dest_abs_eta g;
   258         in Const ("_let", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
   259     | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
   260         Const ("return", dummyT) $ f
   261     | unfold_monad f = f;
   262   fun tr' (f::ts) =
   263     list_comb (Const ("_do", dummyT) $ unfold_monad f, ts)
   264 in [(@{const_syntax "run"}, tr')] end;
   265 *}
   266 
   267 
   268 subsection {* Combinators *}
   269 
   270 definition
   271   lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> 'b \<times> 'c" where
   272   "lift f x = return (f x)"
   273 
   274 primrec
   275   list :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
   276   "list f [] = id"
   277 | "list f (x#xs) = (do f x; list f xs done)"
   278 
   279 primrec
   280   list_yield :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<times> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'c list \<times> 'b" where
   281   "list_yield f [] = return []"
   282 | "list_yield f (x#xs) = (do y \<leftarrow> f x; ys \<leftarrow> list_yield f xs; return (y#ys) done)"
   283 
   284 definition
   285   collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
   286   "collapse f = (do g \<leftarrow> f; g done)"
   287 
   288 text {* combinator properties *}
   289 
   290 lemma list_append [simp]:
   291   "list f (xs @ ys) = list f xs \<guillemotright> list f ys"
   292   by (induct xs) (simp_all del: id_apply)
   293 
   294 lemma list_cong [fundef_cong, recdef_cong]:
   295   "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk>
   296     \<Longrightarrow> list f xs = list g ys"
   297 proof (induct xs arbitrary: ys)
   298   case Nil then show ?case by simp
   299 next
   300   case (Cons x xs)
   301   from Cons have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto
   302   then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto
   303   with Cons have "list f xs = list g xs" by auto
   304   with Cons have "list f (x # xs) = list g (x # xs)" by auto
   305   with Cons show "list f (x # xs) = list g ys" by auto
   306 qed
   307 
   308 lemma list_yield_cong [fundef_cong, recdef_cong]:
   309   "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk>
   310     \<Longrightarrow> list_yield f xs = list_yield g ys"
   311 proof (induct xs arbitrary: ys)
   312   case Nil then show ?case by simp
   313 next
   314   case (Cons x xs)
   315   from Cons have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto
   316   then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto
   317   with Cons have "list_yield f xs = list_yield g xs" by auto
   318   with Cons have "list_yield f (x # xs) = list_yield g (x # xs)" by auto
   319   with Cons show "list_yield f (x # xs) = list_yield g ys" by auto
   320 qed
   321 
   322 text {*
   323   For an example, see HOL/ex/Random.thy.
   324 *}
   325 
   326 end