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