src/HOL/Library/State_Monad.thy
author Andreas Lochbihler
Fri Sep 20 10:09:16 2013 +0200 (2013-09-20)
changeset 53745 788730ab7da4
parent 41229 d797baa3d57c
child 54703 499f92dc6e45
permissions -rw-r--r--
prefer Code.abort over code_abort
haftmann@21192
     1
(*  Title:      HOL/Library/State_Monad.thy
haftmann@21192
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@21192
     3
*)
haftmann@21192
     4
haftmann@40359
     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@40359
    14
  The logic HOL has no notion of constructor classes, so it is not
haftmann@40359
    15
  possible to model monads the Haskell way in full genericity in
haftmann@40359
    16
  Isabelle/HOL.
haftmann@21192
    17
  
haftmann@40359
    18
  However, this theory provides substantial support for a very common
haftmann@40359
    19
  class of monads: \emph{state monads} (or \emph{single-threaded
haftmann@40359
    20
  monads}, since a state is transformed single-threadedly).
haftmann@21192
    21
haftmann@21192
    22
  To enter from the Haskell world,
haftmann@40359
    23
  \url{http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm} makes
haftmann@40359
    24
  a good motivating start.  Here we just sketch briefly how those
haftmann@40359
    25
  monads enter the game of Isabelle/HOL.
haftmann@21192
    26
*}
haftmann@21192
    27
haftmann@21192
    28
subsection {* State transformations and combinators *}
haftmann@21192
    29
haftmann@21192
    30
text {*
haftmann@21192
    31
  We classify functions operating on states into two categories:
haftmann@21192
    32
haftmann@21192
    33
  \begin{description}
haftmann@40359
    34
haftmann@40359
    35
    \item[transformations] with type signature @{text "\<sigma> \<Rightarrow> \<sigma>'"},
haftmann@21192
    36
      transforming a state.
haftmann@40359
    37
haftmann@40359
    38
    \item[``yielding'' transformations] with type signature @{text "\<sigma>
haftmann@40359
    39
      \<Rightarrow> \<alpha> \<times> \<sigma>'"}, ``yielding'' a side result while transforming a
haftmann@40359
    40
      state.
haftmann@40359
    41
haftmann@40359
    42
    \item[queries] with type signature @{text "\<sigma> \<Rightarrow> \<alpha>"}, computing a
haftmann@40359
    43
      result dependent on a state.
haftmann@40359
    44
haftmann@21192
    45
  \end{description}
haftmann@21192
    46
haftmann@40359
    47
  By convention we write @{text "\<sigma>"} for types representing states and
haftmann@40359
    48
  @{text "\<alpha>"}, @{text "\<beta>"}, @{text "\<gamma>"}, @{text "\<dots>"} for types
haftmann@40359
    49
  representing side results.  Type changes due to transformations are
haftmann@40359
    50
  not excluded in our scenario.
haftmann@21192
    51
haftmann@40359
    52
  We aim to assert that values of any state type @{text "\<sigma>"} are used
haftmann@40359
    53
  in a single-threaded way: after application of a transformation on a
haftmann@40359
    54
  value of type @{text "\<sigma>"}, the former value should not be used
haftmann@40359
    55
  again.  To achieve this, 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@21192
    61
text {*
haftmann@40359
    62
  Given two transformations @{term f} and @{term g}, they may be
haftmann@40359
    63
  directly composed using the @{term "op \<circ>>"} combinator, forming a
haftmann@40359
    64
  forward composition: @{prop "(f \<circ>> g) s = f (g s)"}.
haftmann@21192
    65
haftmann@21192
    66
  After any yielding transformation, we bind the side result
haftmann@40359
    67
  immediately using a lambda abstraction.  This is the purpose of the
haftmann@40359
    68
  @{term "op \<circ>\<rightarrow>"} combinator: @{prop "(f \<circ>\<rightarrow> (\<lambda>x. g)) s = (let (x, s')
haftmann@40359
    69
  = f s in g s')"}.
haftmann@21192
    70
haftmann@21192
    71
  For queries, the existing @{term "Let"} is appropriate.
haftmann@21192
    72
haftmann@40359
    73
  Naturally, a computation may yield a side result by pairing it to
haftmann@40359
    74
  the state from the left; we introduce the suggestive abbreviation
haftmann@40359
    75
  @{term return} for this purpose.
haftmann@21192
    76
haftmann@40359
    77
  The most crucial distinction to Haskell is that we do not need to
haftmann@40359
    78
  introduce distinguished type constructors for different kinds of
haftmann@40359
    79
  state.  This has two consequences:
haftmann@40359
    80
haftmann@21192
    81
  \begin{itemize}
haftmann@40359
    82
haftmann@40359
    83
    \item The monad model does not state anything about the kind of
haftmann@40359
    84
       state; the model for the state is completely orthogonal and may
haftmann@40359
    85
       be specified completely independently.
haftmann@40359
    86
haftmann@40359
    87
    \item There is no distinguished type constructor encapsulating
haftmann@40359
    88
       away the state transformation, i.e.~transformations may be
haftmann@40359
    89
       applied directly without using any lifting or providing and
haftmann@40359
    90
       dropping units (``open monad'').
haftmann@40359
    91
haftmann@21192
    92
    \item The type of states may change due to a transformation.
haftmann@40359
    93
haftmann@21192
    94
  \end{itemize}
haftmann@21192
    95
*}
haftmann@21192
    96
haftmann@21192
    97
haftmann@21192
    98
subsection {* Monad laws *}
haftmann@21192
    99
haftmann@21192
   100
text {*
haftmann@40359
   101
  The common monadic laws hold and may also be used as normalization
haftmann@40359
   102
  rules for monadic expressions:
haftmann@21192
   103
*}
haftmann@21192
   104
haftmann@28145
   105
lemmas monad_simp = Pair_scomp scomp_Pair id_fcomp fcomp_id
haftmann@28145
   106
  scomp_scomp scomp_fcomp fcomp_scomp fcomp_assoc
haftmann@21192
   107
haftmann@21192
   108
text {*
haftmann@21192
   109
  Evaluation of monadic expressions by force:
haftmann@21192
   110
*}
haftmann@21192
   111
haftmann@28145
   112
lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta
haftmann@26260
   113
haftmann@37817
   114
haftmann@37817
   115
subsection {* Do-syntax *}
haftmann@37817
   116
wenzelm@41229
   117
nonterminal sdo_binds and 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@40361
   148
  For an example, see @{text "HOL/Proofs/Extraction/Higman.thy"}.
haftmann@21192
   149
*}
haftmann@21192
   150
wenzelm@22664
   151
end