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