src/HOL/Library/State_Monad.thy
author haftmann
Fri Aug 27 19:34:23 2010 +0200 (2010-08-27 ago)
changeset 38857 97775f3e8722
parent 38345 8b8fc27c1872
child 40359 84388bba911d
permissions -rw-r--r--
renamed class/constant eq to equal; tuned some instantiations
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@37932
     8
imports Main Monad_Syntax
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@37751
    58
notation fcomp (infixl "\<circ>>" 60)
haftmann@37817
    59
notation scomp (infixl "\<circ>\<rightarrow>" 60)
wenzelm@21404
    60
haftmann@26588
    61
abbreviation (input)
haftmann@26588
    62
  "return \<equiv> Pair"
wenzelm@21404
    63
haftmann@21192
    64
text {*
haftmann@21192
    65
  Given two transformations @{term f} and @{term g}, they
haftmann@37751
    66
  may be directly composed using the @{term "op \<circ>>"} combinator,
haftmann@37751
    67
  forming a forward composition: @{prop "(f \<circ>> g) s = f (g s)"}.
haftmann@21192
    68
haftmann@21192
    69
  After any yielding transformation, we bind the side result
haftmann@21192
    70
  immediately using a lambda abstraction.  This 
haftmann@37751
    71
  is the purpose of the @{term "op \<circ>\<rightarrow>"} combinator:
haftmann@37751
    72
  @{prop "(f \<circ>\<rightarrow> (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
haftmann@21192
    73
haftmann@21192
    74
  For queries, the existing @{term "Let"} is appropriate.
haftmann@21192
    75
haftmann@21192
    76
  Naturally, a computation may yield a side result by pairing
haftmann@21192
    77
  it to the state from the left;  we introduce the
haftmann@21192
    78
  suggestive abbreviation @{term return} for this purpose.
haftmann@21192
    79
haftmann@21192
    80
  The most crucial distinction to Haskell is that we do
haftmann@21192
    81
  not need to introduce distinguished type constructors
haftmann@21192
    82
  for different kinds of state.  This has two consequences:
haftmann@21192
    83
  \begin{itemize}
haftmann@21192
    84
    \item The monad model does not state anything about
haftmann@21192
    85
       the kind of state; the model for the state is
haftmann@26260
    86
       completely orthogonal and may be
haftmann@26260
    87
       specified completely independently.
haftmann@21192
    88
    \item There is no distinguished type constructor
haftmann@21192
    89
       encapsulating away the state transformation, i.e.~transformations
haftmann@21192
    90
       may be applied directly without using any lifting
haftmann@21192
    91
       or providing and dropping units (``open monad'').
haftmann@21192
    92
    \item The type of states may change due to a transformation.
haftmann@21192
    93
  \end{itemize}
haftmann@21192
    94
*}
haftmann@21192
    95
haftmann@21192
    96
haftmann@21192
    97
subsection {* Monad laws *}
haftmann@21192
    98
haftmann@21192
    99
text {*
haftmann@21192
   100
  The common monadic laws hold and may also be used
haftmann@21192
   101
  as normalization rules for monadic expressions:
haftmann@21192
   102
*}
haftmann@21192
   103
haftmann@28145
   104
lemmas monad_simp = Pair_scomp scomp_Pair id_fcomp fcomp_id
haftmann@28145
   105
  scomp_scomp scomp_fcomp fcomp_scomp fcomp_assoc
haftmann@21192
   106
haftmann@21192
   107
text {*
haftmann@21192
   108
  Evaluation of monadic expressions by force:
haftmann@21192
   109
*}
haftmann@21192
   110
haftmann@28145
   111
lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta
haftmann@26260
   112
haftmann@37817
   113
haftmann@37817
   114
subsection {* Do-syntax *}
haftmann@37817
   115
haftmann@37932
   116
nonterminals
haftmann@37932
   117
  sdo_binds sdo_bind
haftmann@37932
   118
haftmann@37932
   119
syntax
haftmann@37932
   120
  "_sdo_block" :: "sdo_binds \<Rightarrow> 'a" ("exec {//(2  _)//}" [12] 62)
haftmann@37932
   121
  "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ <-/ _)" 13)
haftmann@37932
   122
  "_sdo_let" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(2let _ =/ _)" [1000, 13] 13)
haftmann@37932
   123
  "_sdo_then" :: "'a \<Rightarrow> sdo_bind" ("_" [14] 13)
haftmann@37932
   124
  "_sdo_final" :: "'a \<Rightarrow> sdo_binds" ("_")
haftmann@37932
   125
  "_sdo_cons" :: "[sdo_bind, sdo_binds] \<Rightarrow> sdo_binds" ("_;//_" [13, 12] 12)
haftmann@21192
   126
haftmann@37932
   127
syntax (xsymbols)
haftmann@37932
   128
  "_sdo_bind"  :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ \<leftarrow>/ _)" 13)
haftmann@37932
   129
haftmann@37932
   130
translations
haftmann@37932
   131
  "_sdo_block (_sdo_cons (_sdo_bind p t) (_sdo_final e))"
haftmann@37932
   132
    == "CONST scomp t (\<lambda>p. e)"
haftmann@37932
   133
  "_sdo_block (_sdo_cons (_sdo_then t) (_sdo_final e))"
haftmann@38345
   134
    => "CONST fcomp t e"
haftmann@38345
   135
  "_sdo_final (_sdo_block (_sdo_cons (_sdo_then t) (_sdo_final e)))"
haftmann@38345
   136
    <= "_sdo_final (CONST fcomp t e)"
haftmann@38345
   137
  "_sdo_block (_sdo_cons (_sdo_then t) e)"
haftmann@38345
   138
    <= "CONST fcomp t (_sdo_block e)"
haftmann@37932
   139
  "_sdo_block (_sdo_cons (_sdo_let p t) bs)"
haftmann@37932
   140
    == "let p = t in _sdo_block bs"
haftmann@37932
   141
  "_sdo_block (_sdo_cons b (_sdo_cons c cs))"
haftmann@37932
   142
    == "_sdo_block (_sdo_cons b (_sdo_final (_sdo_block (_sdo_cons c cs))))"
haftmann@37932
   143
  "_sdo_cons (_sdo_let p t) (_sdo_final s)"
haftmann@37932
   144
    == "_sdo_final (let p = t in s)"
haftmann@37932
   145
  "_sdo_block (_sdo_final e)" => "e"
haftmann@37817
   146
haftmann@21418
   147
text {*
haftmann@31033
   148
  For an example, see HOL/Extraction/Higman.thy.
haftmann@21192
   149
*}
haftmann@21192
   150
wenzelm@22664
   151
end