src/HOL/Library/State_Monad.thy
author haftmann
Wed Mar 12 08:47:36 2008 +0100 (2008-03-12)
changeset 26260 23ce0d32de11
parent 26141 e1b3a6953cdc
child 26266 35ae83ca190a
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 (*<*)
    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 may be
   119        specified completely independently.
   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 {* ML abstract operations *}
   195 
   196 ML {*
   197 structure StateMonad =
   198 struct
   199 
   200 fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
   201 fun liftT' sT = sT --> sT;
   202 
   203 fun return T sT x = Const (@{const_name return}, T --> liftT T sT) $ x;
   204 
   205 fun mbind T1 T2 sT f g = Const (@{const_name mbind},
   206   liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
   207 
   208 fun run T sT f = Const (@{const_name run}, liftT' (liftT T sT)) $ f;
   209 
   210 end;
   211 *}
   212 
   213 
   214 subsection {* Syntax *}
   215 
   216 text {*
   217   We provide a convenient do-notation for monadic expressions
   218   well-known from Haskell.  @{const Let} is printed
   219   specially in do-expressions.
   220 *}
   221 
   222 nonterminals do_expr
   223 
   224 syntax
   225   "_do" :: "do_expr \<Rightarrow> 'a"
   226     ("do _ done" [12] 12)
   227   "_mbind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   228     ("_ <- _;// _" [1000, 13, 12] 12)
   229   "_fcomp" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   230     ("_;// _" [13, 12] 12)
   231   "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   232     ("let _ = _;// _" [1000, 13, 12] 12)
   233   "_nil" :: "'a \<Rightarrow> do_expr"
   234     ("_" [12] 12)
   235 
   236 syntax (xsymbols)
   237   "_mbind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   238     ("_ \<leftarrow> _;// _" [1000, 13, 12] 12)
   239 
   240 translations
   241   "_do f" => "CONST run f"
   242   "_mbind x f g" => "f \<guillemotright>= (\<lambda>x. g)"
   243   "_fcomp f g" => "f \<guillemotright> g"
   244   "_let x t f" => "CONST Let t (\<lambda>x. f)"
   245   "_nil f" => "f"
   246 
   247 print_translation {*
   248 let
   249   fun dest_abs_eta (Abs (abs as (_, ty, _))) =
   250         let
   251           val (v, t) = Syntax.variant_abs abs;
   252         in ((v, ty), t) end
   253     | dest_abs_eta t =
   254         let
   255           val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);
   256         in ((v, dummyT), t) end
   257   fun unfold_monad (Const (@{const_syntax mbind}, _) $ f $ g) =
   258         let
   259           val ((v, ty), g') = dest_abs_eta g;
   260         in Const ("_mbind", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
   261     | unfold_monad (Const (@{const_syntax fcomp}, _) $ f $ g) =
   262         Const ("_fcomp", dummyT) $ f $ unfold_monad g
   263     | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
   264         let
   265           val ((v, ty), g') = dest_abs_eta g;
   266         in Const ("_let", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
   267     | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
   268         Const ("return", dummyT) $ f
   269     | unfold_monad f = f;
   270   fun tr' (f::ts) =
   271     list_comb (Const ("_do", dummyT) $ unfold_monad f, ts)
   272 in [(@{const_syntax "run"}, tr')] end;
   273 *}
   274 
   275 
   276 subsection {* Combinators *}
   277 
   278 definition
   279   lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> 'b \<times> 'c" where
   280   "lift f x = return (f x)"
   281 
   282 primrec
   283   list :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
   284   "list f [] = id"
   285 | "list f (x#xs) = (do f x; list f xs done)"
   286 
   287 primrec
   288   list_yield :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<times> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'c list \<times> 'b" where
   289   "list_yield f [] = return []"
   290 | "list_yield f (x#xs) = (do y \<leftarrow> f x; ys \<leftarrow> list_yield f xs; return (y#ys) done)"
   291 
   292 definition
   293   collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
   294   "collapse f = (do g \<leftarrow> f; g done)"
   295 
   296 text {* combinator properties *}
   297 
   298 lemma list_append [simp]:
   299   "list f (xs @ ys) = list f xs \<guillemotright> list f ys"
   300   by (induct xs) (simp_all del: id_apply)
   301 
   302 lemma list_cong [fundef_cong, recdef_cong]:
   303   "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk>
   304     \<Longrightarrow> list f xs = list g ys"
   305 proof (induct xs arbitrary: ys)
   306   case Nil then show ?case by simp
   307 next
   308   case (Cons x xs)
   309   from Cons have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto
   310   then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto
   311   with Cons have "list f xs = list g xs" by auto
   312   with Cons have "list f (x # xs) = list g (x # xs)" by auto
   313   with Cons show "list f (x # xs) = list g ys" by auto
   314 qed
   315 
   316 lemma list_yield_cong [fundef_cong, recdef_cong]:
   317   "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk>
   318     \<Longrightarrow> list_yield f xs = list_yield g ys"
   319 proof (induct xs arbitrary: ys)
   320   case Nil then show ?case by simp
   321 next
   322   case (Cons x xs)
   323   from Cons have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto
   324   then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto
   325   with Cons have "list_yield f xs = list_yield g xs" by auto
   326   with Cons have "list_yield f (x # xs) = list_yield g (x # xs)" by auto
   327   with Cons show "list_yield f (x # xs) = list_yield g ys" by auto
   328 qed
   329 
   330 text {*
   331   For an example, see HOL/ex/Random.thy.
   332 *}
   333 
   334 end