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