Quelle  Open_State_Syntax.thy

(*  Title:      HOL/Library/Open_State_Syntax.thy
    Author:     Florian Haftmann, TU Muenchen
*)

section ‹Combinator syntax for generic, open state monads (single-threaded monads)›

theory Open_State_Syntax
imports Main
begin

context
  includes state_combinator_syntax
begin

subsection ‹Motivation›

text ‹
 The logic HOL has no notion of constructor classes, so it is not
 possible to model monads the Haskell way in full genericity in
 Isabelle/HOL.
 
 However, this theory provides substantial support for a very common
 class of monads: \emph{state monads} (or \emph{single-threaded
 monads}, since a state is transformed single-threadedly).

 To enter from the Haskell world,
 🪙‹https://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm› makes
 a good motivating start. Here we just sketch briefly how those
 monads enter the game of Isabelle/HOL.
 ›

subsection ‹State transformations and combinators›

text ‹
 We classify functions operating on states into two categories:

 \begin{description}

 \item[transformations] with type signature ‹σ ==> σ'›,
 transforming a state.

 \item[``yielding'' transformations] with type signature ‹σ
 ==> α × σ'›, ``yielding'' a side result while transforming a
 state.

 \item[queries] with type signature ‹σ ==> α›, computing a
 result dependent on a state.

 \end{description}

 By convention we write ‹σ› for types representing states and
 ‹α›, ‹β›, ‹γ›, ‹…› for types
 representing side results. Type changes due to transformations are
 not excluded in our scenario.

 We aim to assert that values of any state type ‹σ› are used
 in a single-threaded way: after application of a transformation on a
 value of type ‹σ›, the former value should not be used
 again. To achieve this, we use a set of monad combinators:
 ›

text ‹
 Given two transformations term‹f› and term‹g›, they may be
 directly composed using the term‹(∘>)› combinator, forming a
 forward composition: prop‹(f ∘> g) s = f (g s)›.

 After any yielding transformation, we bind the side result
 immediately using a lambda abstraction. This is the purpose of the
 term‹(∘→)› combinator: prop‹(f ∘→ (λx. g)) s = (let (x, s')
 = f s in g s')›.

 For queries, the existing term‹Let› is appropriate.

 Naturally, a computation may yield a side result by pairing it to
 the state from the left; we introduce the suggestive abbreviation
 term‹return› for this purpose.

 The most crucial distinction to Haskell is that we do not need to
 introduce distinguished type constructors for different kinds of
 state. This has two consequences:

 \begin{itemize}

 \item The monad model does not state anything about the kind of
 state; the model for the state is completely orthogonal and may
 be specified completely independently.

 \item There is no distinguished type constructor encapsulating
 away the state transformation, i.e.~transformations may be
 applied directly without using any lifting or providing and
 dropping units (``open monad'').

 \item The type of states may change due to a transformation.

 \end{itemize}
 ›


subsection ‹Monad laws›

text ‹
 The common monadic laws hold and may also be used as normalization
 rules for monadic expressions:
 ›

lemmas monad_simp = Pair_scomp scomp_Pair id_fcomp fcomp_id
  scomp_scomp scomp_fcomp fcomp_scomp fcomp_assoc

text ‹
 Evaluation of monadic expressions by force:
 ›

lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta

end


subsection ‹Do-syntax›

nonterminal sdo_binds and sdo_bind

syntax
  "_sdo_block" :: "sdo_binds ==> 'a"
    (‹(‹open_block notation=‹mixfix exec block››exec {//(2 _)//})› [12] 62)
  "_sdo_bind"  :: "[pttrn, 'a] ==> sdo_bind"
    (‹(‹indent=2 notation=‹infix exec bind››_ ←/ _)› 13)
  "_sdo_let" :: "[pttrn, 'a] ==> sdo_bind"
    (‹(‹indent=2 notation=‹infix exec let››let _ =/ _)› [1000, 13] 13)
  "_sdo_then" :: "'a ==> sdo_bind"  (‹_› [14] 13)
  "_sdo_final" :: "'a ==> sdo_binds"  (‹_›)
  "_sdo_cons" :: "[sdo_bind, sdo_binds] ==> sdo_binds"
    (‹(‹open_block notation=‹infix exec next››_;//_)› [13, 12] 12)

syntax (ASCII)
  "_sdo_bind" :: "[pttrn, 'a] ==> sdo_bind"
    (‹(‹indent=2 notation=‹infix exec bind››_ <-/ _)› 13)

syntax_consts
  "_sdo_let" == Let

translations
  "_sdo_block (_sdo_cons (_sdo_bind p t) (_sdo_final e))"
    == "CONST scomp t (λp. e)"
  "_sdo_block (_sdo_cons (_sdo_then t) (_sdo_final e))"
    => "CONST fcomp t e"
  "_sdo_final (_sdo_block (_sdo_cons (_sdo_then t) (_sdo_final e)))"
    <= "_sdo_final (CONST fcomp t e)"
  "_sdo_block (_sdo_cons (_sdo_then t) e)"
    <= "CONST fcomp t (_sdo_block e)"
  "_sdo_block (_sdo_cons (_sdo_let p t) bs)"
    == "let p = t in _sdo_block bs"
  "_sdo_block (_sdo_cons b (_sdo_cons c cs))"
    == "_sdo_block (_sdo_cons b (_sdo_final (_sdo_block (_sdo_cons c cs))))"
  "_sdo_cons (_sdo_let p t) (_sdo_final s)"
    == "_sdo_final (let p = t in s)"
  "_sdo_block (_sdo_final e)" => "e"

text ‹
 For an example, see 🍋‹~~/src/HOL/Proofs/Extraction/Higman_Extraction.thy›.
 ›

end