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