src/HOL/Library/State_Monad.thy
author haftmann
Sat Sep 06 14:02:36 2008 +0200 (2008-09-06)
changeset 28145 af3923ed4786
parent 27487 c8a6ce181805
child 29799 7c7f759c438e
permissions -rw-r--r--
dropped "run" marker in monad syntax
     1 (*  Title:      HOL/Library/State_Monad.thy
     2     ID:         $Id$
     3     Author:     Florian Haftmann, TU Muenchen
     4 *)
     5 
     6 header {* Combinator syntax for generic, open state monads (single threaded monads) *}
     7 
     8 theory State_Monad
     9 imports Plain "~~/src/HOL/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 text {*
    33   We classify functions operating on states into two categories:
    34 
    35   \begin{description}
    36     \item[transformations]
    37       with type signature @{text "\<sigma> \<Rightarrow> \<sigma>'"},
    38       transforming a state.
    39     \item[``yielding'' transformations]
    40       with type signature @{text "\<sigma> \<Rightarrow> \<alpha> \<times> \<sigma>'"},
    41       ``yielding'' a side result while transforming a state.
    42     \item[queries]
    43       with type signature @{text "\<sigma> \<Rightarrow> \<alpha>"},
    44       computing a result dependent on a state.
    45   \end{description}
    46 
    47   By convention we write @{text "\<sigma>"} for types representing states
    48   and @{text "\<alpha>"}, @{text "\<beta>"}, @{text "\<gamma>"}, @{text "\<dots>"}
    49   for types representing side results.  Type changes due
    50   to transformations are not excluded in our scenario.
    51 
    52   We aim to assert that values of any state type @{text "\<sigma>"}
    53   are used in a single-threaded way: after application
    54   of a transformation on a value of type @{text "\<sigma>"}, the
    55   former value should not be used again.  To achieve this,
    56   we use a set of monad combinators:
    57 *}
    58 
    59 notation fcomp (infixl "o>" 60)
    60 notation (xsymbols) fcomp (infixl "o>" 60)
    61 notation scomp (infixl "o->" 60)
    62 notation (xsymbols) scomp (infixl "o\<rightarrow>" 60)
    63 
    64 abbreviation (input)
    65   "return \<equiv> Pair"
    66 
    67 text {*
    68   Given two transformations @{term f} and @{term g}, they
    69   may be directly composed using the @{term "op o>"} combinator,
    70   forming a forward composition: @{prop "(f o> g) s = f (g s)"}.
    71 
    72   After any yielding transformation, we bind the side result
    73   immediately using a lambda abstraction.  This 
    74   is the purpose of the @{term "op o\<rightarrow>"} combinator:
    75   @{prop "(f o\<rightarrow> (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
    76 
    77   For queries, the existing @{term "Let"} is appropriate.
    78 
    79   Naturally, a computation may yield a side result by pairing
    80   it to the state from the left;  we introduce the
    81   suggestive abbreviation @{term return} for this purpose.
    82 
    83   The most crucial distinction to Haskell is that we do
    84   not need to introduce distinguished type constructors
    85   for different kinds of state.  This has two consequences:
    86   \begin{itemize}
    87     \item The monad model does not state anything about
    88        the kind of state; the model for the state is
    89        completely orthogonal and may be
    90        specified completely independently.
    91     \item There is no distinguished type constructor
    92        encapsulating away the state transformation, i.e.~transformations
    93        may be applied directly without using any lifting
    94        or providing and dropping units (``open monad'').
    95     \item The type of states may change due to a transformation.
    96   \end{itemize}
    97 *}
    98 
    99 
   100 subsection {* Monad laws *}
   101 
   102 text {*
   103   The common monadic laws hold and may also be used
   104   as normalization rules for monadic expressions:
   105 *}
   106 
   107 lemmas monad_simp = Pair_scomp scomp_Pair id_fcomp fcomp_id
   108   scomp_scomp scomp_fcomp fcomp_scomp fcomp_assoc
   109 
   110 text {*
   111   Evaluation of monadic expressions by force:
   112 *}
   113 
   114 lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta
   115 
   116 
   117 subsection {* Syntax *}
   118 
   119 text {*
   120   We provide a convenient do-notation for monadic expressions
   121   well-known from Haskell.  @{const Let} is printed
   122   specially in do-expressions.
   123 *}
   124 
   125 nonterminals do_expr
   126 
   127 syntax
   128   "_do" :: "do_expr \<Rightarrow> 'a"
   129     ("do _ done" [12] 12)
   130   "_scomp" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   131     ("_ <- _;// _" [1000, 13, 12] 12)
   132   "_fcomp" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   133     ("_;// _" [13, 12] 12)
   134   "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   135     ("let _ = _;// _" [1000, 13, 12] 12)
   136   "_done" :: "'a \<Rightarrow> do_expr"
   137     ("_" [12] 12)
   138 
   139 syntax (xsymbols)
   140   "_scomp" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   141     ("_ \<leftarrow> _;// _" [1000, 13, 12] 12)
   142 
   143 translations
   144   "_do f" => "f"
   145   "_scomp x f g" => "f o\<rightarrow> (\<lambda>x. g)"
   146   "_fcomp f g" => "f o> g"
   147   "_let x t f" => "CONST Let t (\<lambda>x. f)"
   148   "_done f" => "f"
   149 
   150 print_translation {*
   151 let
   152   fun dest_abs_eta (Abs (abs as (_, ty, _))) =
   153         let
   154           val (v, t) = Syntax.variant_abs abs;
   155         in (Free (v, ty), t) end
   156     | dest_abs_eta t =
   157         let
   158           val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);
   159         in (Free (v, dummyT), t) end;
   160   fun unfold_monad (Const (@{const_syntax scomp}, _) $ f $ g) =
   161         let
   162           val (v, g') = dest_abs_eta g;
   163         in Const ("_scomp", dummyT) $ v $ f $ unfold_monad g' end
   164     | unfold_monad (Const (@{const_syntax fcomp}, _) $ f $ g) =
   165         Const ("_fcomp", dummyT) $ f $ unfold_monad g
   166     | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
   167         let
   168           val (v, g') = dest_abs_eta g;
   169         in Const ("_let", dummyT) $ v $ f $ unfold_monad g' end
   170     | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
   171         Const ("return", dummyT) $ f
   172     | unfold_monad f = f;
   173   fun contains_scomp (Const (@{const_syntax scomp}, _) $ _ $ _) = true
   174     | contains_scomp (Const (@{const_syntax fcomp}, _) $ _ $ t) =
   175         contains_scomp t
   176     | contains_scomp (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
   177         contains_scomp t;
   178   fun scomp_monad_tr' (f::g::ts) = list_comb
   179     (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax scomp}, dummyT) $ f $ g), ts);
   180   fun fcomp_monad_tr' (f::g::ts) = if contains_scomp g then list_comb
   181       (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax fcomp}, dummyT) $ f $ g), ts)
   182     else raise Match;
   183   fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) = if contains_scomp g' then list_comb
   184       (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
   185     else raise Match;
   186 in [
   187   (@{const_syntax scomp}, scomp_monad_tr'),
   188   (@{const_syntax fcomp}, fcomp_monad_tr'),
   189   (@{const_syntax Let}, Let_monad_tr')
   190 ] end;
   191 *}
   192 
   193 text {*
   194   For an example, see HOL/ex/Random.thy.
   195 *}
   196 
   197 end