author chaieb Mon Feb 09 17:21:46 2009 +0000 (2009-02-09) changeset 29847 af32126ee729 parent 29799 7c7f759c438e child 30738 0842e906300c permissions -rw-r--r--
     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 Plain "~~/src/HOL/List"

     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 "o>" 60)

    59 notation (xsymbols) fcomp (infixl "o>" 60)

    60 notation scomp (infixl "o->" 60)

    61 notation (xsymbols) scomp (infixl "o\<rightarrow>" 60)

    62

    63 abbreviation (input)

    64   "return \<equiv> Pair"

    65

    66 text {*

    67   Given two transformations @{term f} and @{term g}, they

    68   may be directly composed using the @{term "op o>"} combinator,

    69   forming a forward composition: @{prop "(f o> g) s = f (g s)"}.

    70

    71   After any yielding transformation, we bind the side result

    72   immediately using a lambda abstraction.  This

    73   is the purpose of the @{term "op o\<rightarrow>"} combinator:

    74   @{prop "(f o\<rightarrow> (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.

    75

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

    77

    78   Naturally, a computation may yield a side result by pairing

    79   it to the state from the left;  we introduce the

    80   suggestive abbreviation @{term return} for this purpose.

    81

    82   The most crucial distinction to Haskell is that we do

    83   not need to introduce distinguished type constructors

    84   for different kinds of state.  This has two consequences:

    85   \begin{itemize}

    86     \item The monad model does not state anything about

    87        the kind of state; the model for the state is

    88        completely orthogonal and may be

    89        specified completely independently.

    90     \item There is no distinguished type constructor

    91        encapsulating away the state transformation, i.e.~transformations

    92        may be applied directly without using any lifting

    93        or providing and dropping units (open monad'').

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

    95   \end{itemize}

    96 *}

    97

    98

    99 subsection {* Monad laws *}

   100

   101 text {*

   102   The common monadic laws hold and may also be used

   103   as normalization rules for monadic expressions:

   104 *}

   105

   106 lemmas monad_simp = Pair_scomp scomp_Pair id_fcomp fcomp_id

   107   scomp_scomp scomp_fcomp fcomp_scomp fcomp_assoc

   108

   109 text {*

   110   Evaluation of monadic expressions by force:

   111 *}

   112

   113 lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta

   114

   115

   116 subsection {* Syntax *}

   117

   118 text {*

   119   We provide a convenient do-notation for monadic expressions

   120   well-known from Haskell.  @{const Let} is printed

   121   specially in do-expressions.

   122 *}

   123

   124 nonterminals do_expr

   125

   126 syntax

   127   "_do" :: "do_expr \<Rightarrow> 'a"

   128     ("do _ done" [12] 12)

   129   "_scomp" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"

   130     ("_ <- _;// _" [1000, 13, 12] 12)

   131   "_fcomp" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"

   132     ("_;// _" [13, 12] 12)

   133   "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"

   134     ("let _ = _;// _" [1000, 13, 12] 12)

   135   "_done" :: "'a \<Rightarrow> do_expr"

   136     ("_" [12] 12)

   137

   138 syntax (xsymbols)

   139   "_scomp" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"

   140     ("_ \<leftarrow> _;// _" [1000, 13, 12] 12)

   141

   142 translations

   143   "_do f" => "f"

   144   "_scomp x f g" => "f o\<rightarrow> (\<lambda>x. g)"

   145   "_fcomp f g" => "f o> g"

   146   "_let x t f" => "CONST Let t (\<lambda>x. f)"

   147   "_done f" => "f"

   148

   149 print_translation {*

   150 let

   151   fun dest_abs_eta (Abs (abs as (_, ty, _))) =

   152         let

   153           val (v, t) = Syntax.variant_abs abs;

   154         in (Free (v, ty), t) end

   155     | dest_abs_eta t =

   156         let

   157           val (v, t) = Syntax.variant_abs ("", dummyT, t $Bound 0);   158 in (Free (v, dummyT), t) end;   159 fun unfold_monad (Const (@{const_syntax scomp}, _)$ f $g) =   160 let   161 val (v, g') = dest_abs_eta g;   162 in Const ("_scomp", dummyT)$ v $f$ unfold_monad g' end

   163     | unfold_monad (Const (@{const_syntax fcomp}, _) $f$ g) =

   164         Const ("_fcomp", dummyT) $f$ unfold_monad g

   165     | unfold_monad (Const (@{const_syntax Let}, _) $f$ g) =

   166         let

   167           val (v, g') = dest_abs_eta g;

   168         in Const ("_let", dummyT) $v$ f $unfold_monad g' end   169 | unfold_monad (Const (@{const_syntax Pair}, _)$ f) =

   170         Const ("return", dummyT) $f   171 | unfold_monad f = f;   172 fun contains_scomp (Const (@{const_syntax scomp}, _)$ _ $_) = true   173 | contains_scomp (Const (@{const_syntax fcomp}, _)$ _ $t) =   174 contains_scomp t   175 | contains_scomp (Const (@{const_syntax Let}, _)$ _ $Abs (_, _, t)) =   176 contains_scomp t;   177 fun scomp_monad_tr' (f::g::ts) = list_comb   178 (Const ("_do", dummyT)$ unfold_monad (Const (@{const_syntax scomp}, dummyT) $f$ g), ts);

   179   fun fcomp_monad_tr' (f::g::ts) = if contains_scomp g then list_comb

   180       (Const ("_do", dummyT) $unfold_monad (Const (@{const_syntax fcomp}, dummyT)$ f $g), ts)   181 else raise Match;   182 fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) = if contains_scomp g' then list_comb   183 (Const ("_do", dummyT)$ unfold_monad (Const (@{const_syntax Let}, dummyT) $f$ g), ts)

   184     else raise Match;

   185 in [

   186   (@{const_syntax scomp}, scomp_monad_tr'),

   187   (@{const_syntax fcomp}, fcomp_monad_tr'),

   188   (@{const_syntax Let}, Let_monad_tr')

   189 ] end;

   190 *}

   191

   192 text {*

   193   For an example, see HOL/ex/Random.thy.

   194 *}

   195

   196 end