src/HOL/Library/Open_State_Syntax.thy
 author haftmann Wed Jul 18 20:51:21 2018 +0200 (11 months ago) changeset 68658 16cc1161ad7f parent 68224 1f7308050349 child 69593 3dda49e08b9d permissions -rw-r--r--
tuned equation
     1 (*  Title:      HOL/Library/Open_State_Syntax.thy

     2     Author:     Florian Haftmann, TU Muenchen

     3 *)

     4

     5 section \<open>Combinator syntax for generic, open state monads (single-threaded monads)\<close>

     6

     7 theory Open_State_Syntax

     8 imports Main

     9 begin

    10

    11 subsection \<open>Motivation\<close>

    12

    13 text \<open>

    14   The logic HOL has no notion of constructor classes, so it is not

    15   possible to model monads the Haskell way in full genericity in

    16   Isabelle/HOL.

    17

    18   However, this theory provides substantial support for a very common

    19   class of monads: \emph{state monads} (or \emph{single-threaded

    20   monads}, since a state is transformed single-threadedly).

    21

    22   To enter from the Haskell world,

    23   \<^url>\<open>https://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm\<close> makes

    24   a good motivating start.  Here we just sketch briefly how those

    25   monads enter the game of Isabelle/HOL.

    26 \<close>

    27

    28 subsection \<open>State transformations and combinators\<close>

    29

    30 text \<open>

    31   We classify functions operating on states into two categories:

    32

    33   \begin{description}

    34

    35     \item[transformations] with type signature \<open>\<sigma> \<Rightarrow> \<sigma>'\<close>,

    36       transforming a state.

    37

    38     \item[yielding'' transformations] with type signature \<open>\<sigma>

    39       \<Rightarrow> \<alpha> \<times> \<sigma>'\<close>, yielding'' a side result while transforming a

    40       state.

    41

    42     \item[queries] with type signature \<open>\<sigma> \<Rightarrow> \<alpha>\<close>, computing a

    43       result dependent on a state.

    44

    45   \end{description}

    46

    47   By convention we write \<open>\<sigma>\<close> for types representing states and

    48   \<open>\<alpha>\<close>, \<open>\<beta>\<close>, \<open>\<gamma>\<close>, \<open>\<dots>\<close> for types

    49   representing side results.  Type changes due to transformations are

    50   not excluded in our scenario.

    51

    52   We aim to assert that values of any state type \<open>\<sigma>\<close> are used

    53   in a single-threaded way: after application of a transformation on a

    54   value of type \<open>\<sigma>\<close>, the former value should not be used

    55   again.  To achieve this, we use a set of monad combinators:

    56 \<close>

    57

    58 notation fcomp (infixl "\<circ>>" 60)

    59 notation scomp (infixl "\<circ>\<rightarrow>" 60)

    60

    61 text \<open>

    62   Given two transformations @{term f} and @{term g}, they may be

    63   directly composed using the @{term "(\<circ>>)"} combinator, forming a

    64   forward composition: @{prop "(f \<circ>> g) s = f (g s)"}.

    65

    66   After any yielding transformation, we bind the side result

    67   immediately using a lambda abstraction.  This is the purpose of the

    68   @{term "(\<circ>\<rightarrow>)"} combinator: @{prop "(f \<circ>\<rightarrow> (\<lambda>x. g)) s = (let (x, s')

    69   = f s in g s')"}.

    70

    71   For queries, the existing @{term "Let"} is appropriate.

    72

    73   Naturally, a computation may yield a side result by pairing it to

    74   the state from the left; we introduce the suggestive abbreviation

    75   @{term return} for this purpose.

    76

    77   The most crucial distinction to Haskell is that we do not need to

    78   introduce distinguished type constructors for different kinds of

    79   state.  This has two consequences:

    80

    81   \begin{itemize}

    82

    83     \item The monad model does not state anything about the kind of

    84        state; the model for the state is completely orthogonal and may

    85        be specified completely independently.

    86

    87     \item There is no distinguished type constructor encapsulating

    88        away the state transformation, i.e.~transformations may be

    89        applied directly without using any lifting or providing and

    90        dropping units (open monad'').

    91

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

    93

    94   \end{itemize}

    95 \<close>

    96

    97

    98 subsection \<open>Monad laws\<close>

    99

   100 text \<open>

   101   The common monadic laws hold and may also be used as normalization

   102   rules for monadic expressions:

   103 \<close>

   104

   105 lemmas monad_simp = Pair_scomp scomp_Pair id_fcomp fcomp_id

   106   scomp_scomp scomp_fcomp fcomp_scomp fcomp_assoc

   107

   108 text \<open>

   109   Evaluation of monadic expressions by force:

   110 \<close>

   111

   112 lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta

   113

   114

   115 subsection \<open>Do-syntax\<close>

   116

   117 nonterminal sdo_binds and sdo_bind

   118

   119 syntax

   120   "_sdo_block" :: "sdo_binds \<Rightarrow> 'a" ("exec {//(2  _)//}" [12] 62)

   121   "_sdo_bind"  :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ \<leftarrow>/ _)" 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 (ASCII)

   128   "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ <-/ _)" 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 \<open>

   148   For an example, see \<^file>\<open>~~/src/HOL/Proofs/Extraction/Higman_Extraction.thy\<close>.

   149 \<close>

   150

   151 end