src/HOL/Library/State_Monad.thy
author wenzelm
Fri Apr 13 21:26:34 2007 +0200 (2007-04-13)
changeset 22664 e965391e2864
parent 22492 43545e640877
child 24195 7d1a16c77f7c
permissions -rw-r--r--
do translation: CONST;
     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 Main
    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" => "Let t (\<lambda>x. f)"
   225   "_nil f" => "f"
   226 
   227 print_translation {*
   228 let
   229   val name_mbind = @{const_syntax "mbind"};
   230   val name_fcomp = @{const_syntax "fcomp"};
   231   fun unfold_monad (t as Const (name, _) $ f $ g) =
   232         if name = name_mbind then let
   233             val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
   234           in Const ("_mbind", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
   235         else if name = name_fcomp then
   236           Const ("_fcomp", dummyT) $ f $ unfold_monad g
   237         else t
   238     | unfold_monad (Const ("Let", _) $ f $ g) =
   239         let
   240           
   241           val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
   242         in Const ("_let", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
   243     | unfold_monad (Const ("Pair", _) $ f) =
   244         Const ("return", dummyT) $ f
   245     | unfold_monad f = f;
   246   fun tr' (f::ts) =
   247     list_comb (Const ("_do", dummyT) $ unfold_monad f, ts)
   248 in [(@{const_syntax "run"}, tr')] end;
   249 *}
   250 
   251 subsection {* Combinators *}
   252 
   253 definition
   254   lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> 'b \<times> 'c" where
   255   "lift f x = return (f x)"
   256 
   257 fun
   258   list :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
   259   "list f [] = id"
   260 | "list f (x#xs) = (do f x; list f xs done)"
   261 lemmas [code] = list.simps
   262 
   263 fun list_yield :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<times> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'c list \<times> 'b" where
   264   "list_yield f [] = return []"
   265 | "list_yield f (x#xs) = (do y \<leftarrow> f x; ys \<leftarrow> list_yield f xs; return (y#ys) done)"
   266 lemmas [code] = list_yield.simps
   267   
   268 text {* combinator properties *}
   269 
   270 lemma list_append [simp]:
   271   "list f (xs @ ys) = list f xs \<guillemotright> list f ys"
   272   by (induct xs) (simp_all del: id_apply) (*FIXME*)
   273 
   274 lemma list_cong [fundef_cong, recdef_cong]:
   275   "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk>
   276     \<Longrightarrow> list f xs = list g ys"
   277 proof (induct f xs arbitrary: g ys rule: list.induct)
   278   case 1 then show ?case by simp
   279 next
   280   case (2 f x xs g)
   281   from 2 have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto
   282   then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto
   283   with 2 have "list f xs = list g xs" by auto
   284   with 2 have "list f (x # xs) = list g (x # xs)" by auto
   285   with 2 show "list f (x # xs) = list g ys" by auto
   286 qed
   287 
   288 lemma list_yield_cong [fundef_cong, recdef_cong]:
   289   "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk>
   290     \<Longrightarrow> list_yield f xs = list_yield g ys"
   291 proof (induct f xs arbitrary: g ys rule: list_yield.induct)
   292   case 1 then show ?case by simp
   293 next
   294   case (2 f x xs g)
   295   from 2 have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto
   296   then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto
   297   with 2 have "list_yield f xs = list_yield g xs" by auto
   298   with 2 have "list_yield f (x # xs) = list_yield g (x # xs)" by auto
   299   with 2 show "list_yield f (x # xs) = list_yield g ys" by auto
   300 qed
   301 
   302 text {*
   303   still waiting for extensions@{text "\<dots>"}
   304 *}
   305 
   306 text {*
   307   For an example, see HOL/ex/CodeRandom.thy (more examples coming soon).
   308 *}
   309 
   310 end