src/HOL/Library/State_Monad.thy
author haftmann
Mon Nov 06 16:28:33 2006 +0100 (2006-11-06)
changeset 21192 5fe5cd5fede7
child 21283 b15355b9a59d
permissions -rw-r--r--
added state monad to HOL library
     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 "\<guillemotright>=" 60)
    72   "f \<guillemotright>= g = split g \<circ> f"
    73   fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"
    74     (infixl "\<guillemotright>" 60)
    75   "f \<guillemotright> g = g \<circ> f"
    76   run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    77   "run f = f"
    78 
    79 syntax (input)
    80   mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
    81     (infixl ">>=" 60)
    82   fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"
    83     (infixl ">>" 60)
    84 
    85 abbreviation (input)
    86   "return \<equiv> Pair"
    87 
    88 text {*
    89   Given two transformations @{term f} and @{term g}, they
    90   may be directly composed using the @{term "op \<guillemotright>"} combinator,
    91   forming a forward composition: @{prop "(f \<guillemotright> g) s = f (g s)"}.
    92 
    93   After any yielding transformation, we bind the side result
    94   immediately using a lambda abstraction.  This 
    95   is the purpose of the @{term "op \<guillemotright>="} combinator:
    96   @{prop "(f \<guillemotright>= (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
    97 
    98   For queries, the existing @{term "Let"} is appropriate.
    99 
   100   Naturally, a computation may yield a side result by pairing
   101   it to the state from the left;  we introduce the
   102   suggestive abbreviation @{term return} for this purpose.
   103 
   104   The @{const run} ist just a marker.
   105 
   106   The most crucial distinction to Haskell is that we do
   107   not need to introduce distinguished type constructors
   108   for different kinds of state.  This has two consequences:
   109   \begin{itemize}
   110     \item The monad model does not state anything about
   111        the kind of state; the model for the state is
   112        completely orthogonal and has (or may) be
   113        specified completely independent.
   114     \item There is no distinguished type constructor
   115        encapsulating away the state transformation, i.e.~transformations
   116        may be applied directly without using any lifting
   117        or providing and dropping units (``open monad'').
   118     \item The type of states may change due to a transformation.
   119   \end{itemize}
   120 *}
   121 
   122 
   123 subsection {* Obsolete runs *}
   124 
   125 text {*
   126   @{term run} is just a doodle and should not occur nested:
   127 *}
   128 
   129 lemma run_simp [simp]:
   130   "\<And>f. run (run f) = run f"
   131   "\<And>f g. run f \<guillemotright>= g = f \<guillemotright>= g"
   132   "\<And>f g. run f \<guillemotright> g = f \<guillemotright> g"
   133   "\<And>f g. f \<guillemotright>= (\<lambda>x. run g) = f \<guillemotright>= (\<lambda>x. g)"
   134   "\<And>f g. f \<guillemotright> run g = f \<guillemotright> g"
   135   "\<And>f. f = run f \<longleftrightarrow> True"
   136   "\<And>f. run f = f \<longleftrightarrow> True"
   137   unfolding run_def by rule+
   138 
   139 
   140 subsection {* Monad laws *}
   141 
   142 text {*
   143   The common monadic laws hold and may also be used
   144   as normalization rules for monadic expressions:
   145 *}
   146 
   147 lemma
   148   return_mbind [simp]: "return x \<guillemotright>= f = f x"
   149   unfolding mbind_def by (simp add: expand_fun_eq)
   150 
   151 lemma
   152   mbind_return [simp]: "x \<guillemotright>= return = x"
   153   unfolding mbind_def by (simp add: expand_fun_eq split_Pair)
   154 
   155 lemma
   156   mbind_mbind [simp]: "(f \<guillemotright>= g) \<guillemotright>= h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h)"
   157   unfolding mbind_def by (simp add: split_def expand_fun_eq)
   158 
   159 lemma
   160   mbind_fcomp [simp]: "(f \<guillemotright>= g) \<guillemotright> h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright> h)"
   161   unfolding mbind_def fcomp_def by (simp add: split_def expand_fun_eq)
   162 
   163 lemma
   164   fcomp_mbind [simp]: "(f \<guillemotright> g) \<guillemotright>= h = f \<guillemotright> (g \<guillemotright>= h)"
   165   unfolding mbind_def fcomp_def by (simp add: split_def expand_fun_eq)
   166 
   167 lemma
   168   fcomp_fcomp [simp]: "(f \<guillemotright> g) \<guillemotright> h = f \<guillemotright> (g \<guillemotright> h)"
   169   unfolding fcomp_def o_assoc ..
   170 
   171 lemmas monad_simp = run_simp return_mbind mbind_return
   172   mbind_mbind mbind_fcomp fcomp_mbind fcomp_fcomp
   173 
   174 text {*
   175   Evaluation of monadic expressions by force:
   176 *}
   177 
   178 lemmas monad_collapse = monad_simp o_apply o_assoc split_Pair split_comp
   179   mbind_def fcomp_def run_def
   180 
   181 subsection {* Syntax *}
   182 
   183 text {*
   184   We provide a convenient do-notation for monadic expressions
   185   well-known from Haskell.  @{const Let} is printed
   186   specially in do-expressions.
   187 *}
   188 
   189 nonterminals do_expr
   190 
   191 syntax
   192   "_do" :: "do_expr \<Rightarrow> 'a"
   193     ("do _ done" [12] 12)
   194   "_mbind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   195     ("_ <- _;// _" [1000, 13, 12] 12)
   196   "_fcomp" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   197     ("_;// _" [13, 12] 12)
   198   "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   199     ("let _ = _;// _" [1000, 13, 12] 12)
   200   "_nil" :: "'a \<Rightarrow> do_expr"
   201     ("_" [12] 12)
   202 
   203 syntax (xsymbols)
   204   "_mbind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   205     ("_ \<leftarrow> _;// _" [1000, 13, 12] 12)
   206 
   207 translations
   208   "_do f" => "State_Monad.run f"
   209   "_mbind x f g" => "f \<guillemotright>= (\<lambda>x. g)"
   210   "_fcomp f g" => "f \<guillemotright> g"
   211   "_let x t f" => "Let t (\<lambda>x. f)"
   212   "_nil f" => "f"
   213 
   214 print_translation {*
   215 let
   216   val syntax_name = Sign.const_syntax_name (the_context ());
   217   val name_mbind = syntax_name "State_Monad.mbind";
   218   val name_fcomp = syntax_name "State_Monad.fcomp";
   219   fun unfold_monad (t as Const (name, _) $ f $ g) =
   220         if name = name_mbind then let
   221             val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
   222           in Const ("_mbind", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
   223         else if name = name_fcomp then
   224           Const ("_fcomp", dummyT) $ f $ unfold_monad g
   225         else t
   226     | unfold_monad (Const ("Let", _) $ f $ g) =
   227         let
   228           val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
   229         in Const ("_let", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
   230     | unfold_monad (Const ("Pair", _) $ f) =
   231         Const ("return", dummyT) $ f
   232     | unfold_monad f = f;
   233   fun tr' (f::ts) =
   234     list_comb (Const ("_do", dummyT) $ unfold_monad f, ts)
   235 in [
   236   (syntax_name "State_Monad.run", tr')
   237 ] end;
   238 *}
   239 
   240 print_ast_translation {*[
   241   (Sign.const_syntax_name (the_context ()) "State_Monad.run", fn (f::ts) => Syntax.mk_appl f ts)
   242 ]*}
   243 
   244 text {*
   245   For an example, see HOL/ex/CodeRandom.thy (more examples coming soon).
   246 *}
   247 
   248 end