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