src/HOL/Library/State_Monad.thy
author wenzelm
Fri Nov 17 02:20:03 2006 +0100 (2006-11-17)
changeset 21404 eb85850d3eb7
parent 21283 b15355b9a59d
child 21418 4bc2882f80af
permissions -rw-r--r--
more robust syntax for definition/abbreviation/notation;
     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 section {* Generic, open state monads *}
    13 
    14 subsection {* Motivation *}
    15 
    16 text {*
    17   The logic HOL has no notion of constructor classes, so
    18   it is not possible to model monads the Haskell way
    19   in full genericity in Isabelle/HOL.
    20   
    21   However, this theory provides substantial support for
    22   a very common class of monads: \emph{state monads}
    23   (or \emph{single-threaded monads}, since a state
    24   is transformed single-threaded).
    25 
    26   To enter from the Haskell world,
    27   \url{http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm}
    28   makes a good motivating start.  Here we just sketch briefly
    29   how those monads enter the game of Isabelle/HOL.
    30 *}
    31 
    32 subsection {* State transformations and combinators *}
    33 
    34 (*<*)
    35 typedecl \<alpha>
    36 typedecl \<beta>
    37 typedecl \<gamma>
    38 typedecl \<sigma>
    39 typedecl \<sigma>'
    40 (*>*)
    41 
    42 text {*
    43   We classify functions operating on states into two categories:
    44 
    45   \begin{description}
    46     \item[transformations]
    47       with type signature @{typ "\<sigma> \<Rightarrow> \<sigma>'"},
    48       transforming a state.
    49     \item[``yielding'' transformations]
    50       with type signature @{typ "\<sigma> \<Rightarrow> \<alpha> \<times> \<sigma>'"},
    51       ``yielding'' a side result while transforming a state.
    52     \item[queries]
    53       with type signature @{typ "\<sigma> \<Rightarrow> \<alpha>"},
    54       computing a result dependent on a state.
    55   \end{description}
    56 
    57   By convention we write @{typ "\<sigma>"} for types representing states
    58   and @{typ "\<alpha>"}, @{typ "\<beta>"}, @{typ "\<gamma>"}, @{text "\<dots>"}
    59   for types representing side results.  Type changes due
    60   to transformations are not excluded in our scenario.
    61 
    62   We aim to assert that values of any state type @{typ "\<sigma>"}
    63   are used in a single-threaded way: after application
    64   of a transformation on a value of type @{typ "\<sigma>"}, the
    65   former value should not be used again.  To achieve this,
    66   we use a set of monad combinators:
    67 *}
    68 
    69 definition
    70   mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
    71     (infixl ">>=" 60) where
    72   "f >>= g = split g \<circ> f"
    73 
    74 definition
    75   fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"
    76     (infixl ">>" 60) where
    77   "f >> g = g \<circ> f"
    78 
    79 definition
    80   run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    81   "run f = f"
    82 
    83 print_ast_translation {*[
    84   (Sign.const_syntax_name (the_context ()) "State_Monad.run", fn (f::ts) => Syntax.mk_appl f ts)
    85 ]*}
    86 
    87 syntax (xsymbols)
    88   mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
    89     (infixl "\<guillemotright>=" 60)
    90   fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"
    91     (infixl "\<guillemotright>" 60)
    92 
    93 abbreviation (input)
    94   "return \<equiv> Pair"
    95 
    96 text {*
    97   Given two transformations @{term f} and @{term g}, they
    98   may be directly composed using the @{term "op \<guillemotright>"} combinator,
    99   forming a forward composition: @{prop "(f \<guillemotright> g) s = f (g s)"}.
   100 
   101   After any yielding transformation, we bind the side result
   102   immediately using a lambda abstraction.  This 
   103   is the purpose of the @{term "op \<guillemotright>="} combinator:
   104   @{prop "(f \<guillemotright>= (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
   105 
   106   For queries, the existing @{term "Let"} is appropriate.
   107 
   108   Naturally, a computation may yield a side result by pairing
   109   it to the state from the left;  we introduce the
   110   suggestive abbreviation @{term return} for this purpose.
   111 
   112   The @{const run} ist just a marker.
   113 
   114   The most crucial distinction to Haskell is that we do
   115   not need to introduce distinguished type constructors
   116   for different kinds of state.  This has two consequences:
   117   \begin{itemize}
   118     \item The monad model does not state anything about
   119        the kind of state; the model for the state is
   120        completely orthogonal and has to (or may) be
   121        specified completely independent.
   122     \item There is no distinguished type constructor
   123        encapsulating away the state transformation, i.e.~transformations
   124        may be applied directly without using any lifting
   125        or providing and dropping units (``open monad'').
   126     \item The type of states may change due to a transformation.
   127   \end{itemize}
   128 *}
   129 
   130 
   131 subsection {* Obsolete runs *}
   132 
   133 text {*
   134   @{term run} is just a doodle and should not occur nested:
   135 *}
   136 
   137 lemma run_simp [simp]:
   138   "\<And>f. run (run f) = run f"
   139   "\<And>f g. run f \<guillemotright>= g = f \<guillemotright>= g"
   140   "\<And>f g. run f \<guillemotright> g = f \<guillemotright> g"
   141   "\<And>f g. f \<guillemotright>= (\<lambda>x. run g) = f \<guillemotright>= (\<lambda>x. g)"
   142   "\<And>f g. f \<guillemotright> run g = f \<guillemotright> g"
   143   "\<And>f. f = run f \<longleftrightarrow> True"
   144   "\<And>f. run f = f \<longleftrightarrow> True"
   145   unfolding run_def by rule+
   146 
   147 
   148 subsection {* Monad laws *}
   149 
   150 text {*
   151   The common monadic laws hold and may also be used
   152   as normalization rules for monadic expressions:
   153 *}
   154 
   155 lemma
   156   return_mbind [simp]: "return x \<guillemotright>= f = f x"
   157   unfolding mbind_def by (simp add: expand_fun_eq)
   158 
   159 lemma
   160   mbind_return [simp]: "x \<guillemotright>= return = x"
   161   unfolding mbind_def by (simp add: expand_fun_eq split_Pair)
   162 
   163 lemma
   164   mbind_mbind [simp]: "(f \<guillemotright>= g) \<guillemotright>= h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h)"
   165   unfolding mbind_def by (simp add: split_def expand_fun_eq)
   166 
   167 lemma
   168   mbind_fcomp [simp]: "(f \<guillemotright>= g) \<guillemotright> h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright> h)"
   169   unfolding mbind_def fcomp_def by (simp add: split_def expand_fun_eq)
   170 
   171 lemma
   172   fcomp_mbind [simp]: "(f \<guillemotright> g) \<guillemotright>= h = f \<guillemotright> (g \<guillemotright>= h)"
   173   unfolding mbind_def fcomp_def by (simp add: split_def expand_fun_eq)
   174 
   175 lemma
   176   fcomp_fcomp [simp]: "(f \<guillemotright> g) \<guillemotright> h = f \<guillemotright> (g \<guillemotright> h)"
   177   unfolding fcomp_def o_assoc ..
   178 
   179 lemmas monad_simp = run_simp return_mbind mbind_return
   180   mbind_mbind mbind_fcomp fcomp_mbind fcomp_fcomp
   181 
   182 text {*
   183   Evaluation of monadic expressions by force:
   184 *}
   185 
   186 lemmas monad_collapse = monad_simp o_apply o_assoc split_Pair split_comp
   187   mbind_def fcomp_def run_def
   188 
   189 subsection {* Syntax *}
   190 
   191 text {*
   192   We provide a convenient do-notation for monadic expressions
   193   well-known from Haskell.  @{const Let} is printed
   194   specially in do-expressions.
   195 *}
   196 
   197 nonterminals do_expr
   198 
   199 syntax
   200   "_do" :: "do_expr \<Rightarrow> 'a"
   201     ("do _ done" [12] 12)
   202   "_mbind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   203     ("_ <- _;// _" [1000, 13, 12] 12)
   204   "_fcomp" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   205     ("_;// _" [13, 12] 12)
   206   "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   207     ("let _ = _;// _" [1000, 13, 12] 12)
   208   "_nil" :: "'a \<Rightarrow> do_expr"
   209     ("_" [12] 12)
   210 
   211 syntax (xsymbols)
   212   "_mbind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   213     ("_ \<leftarrow> _;// _" [1000, 13, 12] 12)
   214 
   215 translations
   216   "_do f" => "State_Monad.run f"
   217   "_mbind x f g" => "f \<guillemotright>= (\<lambda>x. g)"
   218   "_fcomp f g" => "f \<guillemotright> g"
   219   "_let x t f" => "Let t (\<lambda>x. f)"
   220   "_nil f" => "f"
   221 
   222 print_translation {*
   223 let
   224   val syntax_name = Sign.const_syntax_name (the_context ());
   225   val name_mbind = syntax_name "State_Monad.mbind";
   226   val name_fcomp = syntax_name "State_Monad.fcomp";
   227   fun unfold_monad (t as Const (name, _) $ f $ g) =
   228         if name = name_mbind then let
   229             val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
   230           in Const ("_mbind", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
   231         else if name = name_fcomp then
   232           Const ("_fcomp", dummyT) $ f $ unfold_monad g
   233         else t
   234     | unfold_monad (Const ("Let", _) $ f $ g) =
   235         let
   236           
   237           val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
   238         in Const ("_let", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
   239     | unfold_monad (Const ("Pair", _) $ f) =
   240         Const ("return", dummyT) $ f
   241     | unfold_monad f = f;
   242   fun tr' (f::ts) =
   243     list_comb (Const ("_do", dummyT) $ unfold_monad f, ts)
   244 in [
   245   (syntax_name "State_Monad.run", tr')
   246 ] end;
   247 *}
   248 
   249 text {*
   250   For an example, see HOL/ex/CodeRandom.thy (more examples coming soon).
   251 *}
   252 
   253 end