src/HOL/Library/State_Monad.thy
author haftmann
Wed Apr 09 08:10:11 2008 +0200 (2008-04-09)
changeset 26588 d83271bfaba5
parent 26266 35ae83ca190a
child 27368 9f90ac19e32b
permissions -rw-r--r--
removed syntax from monad combinators; renamed mbind to scomp
     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 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