author wenzelm Fri Nov 17 02:20:03 2006 +0100 (2006-11-17) changeset 21404 eb85850d3eb7 parent 21283 b15355b9a59d child 21418 4bc2882f80af permissions -rw-r--r--
more robust syntax for definition/abbreviation/notation;
     1 (*  Title:      HOL/Library/State_Monad.thy

     2     ID:         $Id$

     3     Author:     Florian Haftmann, TU Muenchen

     4 *)

     5

     6 header {* Combinators syntax for generic, open state monads (single threaded monads) *}

     7

     8 theory State_Monad

     9 imports Main

    10 begin

    11

    12 section {* Generic, open state monads *}

    13

    14 subsection {* Motivation *}

    15

    16 text {*

    17   The logic HOL has no notion of constructor classes, so

    18   it is not possible to model monads the Haskell way

    19   in full genericity in Isabelle/HOL.

    20

    21   However, this theory provides substantial support for

    22   a very common class of monads: \emph{state monads}

    23   (or \emph{single-threaded monads}, since a state

    24   is transformed single-threaded).

    25

    26   To enter from the Haskell world,

    27   \url{http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm}

    28   makes a good motivating start.  Here we just sketch briefly

    29   how those monads enter the game of Isabelle/HOL.

    30 *}

    31

    32 subsection {* State transformations and combinators *}

    33

    34 (*<*)

    35 typedecl \<alpha>

    36 typedecl \<beta>

    37 typedecl \<gamma>

    38 typedecl \<sigma>

    39 typedecl \<sigma>'

    40 (*>*)

    41

    42 text {*

    43   We classify functions operating on states into two categories:

    44

    45   \begin{description}

    46     \item[transformations]

    47       with type signature @{typ "\<sigma> \<Rightarrow> \<sigma>'"},

    48       transforming a state.

    49     \item[yielding'' transformations]

    50       with type signature @{typ "\<sigma> \<Rightarrow> \<alpha> \<times> \<sigma>'"},

    51       yielding'' a side result while transforming a state.

    52     \item[queries]

    53       with type signature @{typ "\<sigma> \<Rightarrow> \<alpha>"},

    54       computing a result dependent on a state.

    55   \end{description}

    56

    57   By convention we write @{typ "\<sigma>"} for types representing states

    58   and @{typ "\<alpha>"}, @{typ "\<beta>"}, @{typ "\<gamma>"}, @{text "\<dots>"}

    59   for types representing side results.  Type changes due

    60   to transformations are not excluded in our scenario.

    61

    62   We aim to assert that values of any state type @{typ "\<sigma>"}

    63   are used in a single-threaded way: after application

    64   of a transformation on a value of type @{typ "\<sigma>"}, the

    65   former value should not be used again.  To achieve this,

    66   we use a set of monad combinators:

    67 *}

    68

    69 definition

    70   mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"

    71     (infixl ">>=" 60) where

    72   "f >>= g = split g \<circ> f"

    73

    74 definition

    75   fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"

    76     (infixl ">>" 60) where

    77   "f >> g = g \<circ> f"

    78

    79 definition

    80   run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where

    81   "run f = f"

    82

    83 print_ast_translation {*[

    84   (Sign.const_syntax_name (the_context ()) "State_Monad.run", fn (f::ts) => Syntax.mk_appl f ts)

    85 ]*}

    86

    87 syntax (xsymbols)

    88   mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"

    89     (infixl "\<guillemotright>=" 60)

    90   fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"

    91     (infixl "\<guillemotright>" 60)

    92

    93 abbreviation (input)

    94   "return \<equiv> Pair"

    95

    96 text {*

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

    98   may be directly composed using the @{term "op \<guillemotright>"} combinator,

    99   forming a forward composition: @{prop "(f \<guillemotright> g) s = f (g s)"}.

   100

   101   After any yielding transformation, we bind the side result

   102   immediately using a lambda abstraction.  This

   103   is the purpose of the @{term "op \<guillemotright>="} combinator:

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

   105

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

   107

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

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

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

   111

   112   The @{const run} ist just a marker.

   113

   114   The most crucial distinction to Haskell is that we do

   115   not need to introduce distinguished type constructors

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

   117   \begin{itemize}

   118     \item The monad model does not state anything about

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

   120        completely orthogonal and has to (or may) be

   121        specified completely independent.

   122     \item There is no distinguished type constructor

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

   124        may be applied directly without using any lifting

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

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

   127   \end{itemize}

   128 *}

   129

   130

   131 subsection {* Obsolete runs *}

   132

   133 text {*

   134   @{term run} is just a doodle and should not occur nested:

   135 *}

   136

   137 lemma run_simp [simp]:

   138   "\<And>f. run (run f) = run f"

   139   "\<And>f g. run f \<guillemotright>= g = f \<guillemotright>= g"

   140   "\<And>f g. run f \<guillemotright> g = f \<guillemotright> g"

   141   "\<And>f g. f \<guillemotright>= (\<lambda>x. run g) = f \<guillemotright>= (\<lambda>x. g)"

   142   "\<And>f g. f \<guillemotright> run g = f \<guillemotright> g"

   143   "\<And>f. f = run f \<longleftrightarrow> True"

   144   "\<And>f. run f = f \<longleftrightarrow> True"

   145   unfolding run_def by rule+

   146

   147

   148 subsection {* Monad laws *}

   149

   150 text {*

   151   The common monadic laws hold and may also be used

   152   as normalization rules for monadic expressions:

   153 *}

   154

   155 lemma

   156   return_mbind [simp]: "return x \<guillemotright>= f = f x"

   157   unfolding mbind_def by (simp add: expand_fun_eq)

   158

   159 lemma

   160   mbind_return [simp]: "x \<guillemotright>= return = x"

   161   unfolding mbind_def by (simp add: expand_fun_eq split_Pair)

   162

   163 lemma

   164   mbind_mbind [simp]: "(f \<guillemotright>= g) \<guillemotright>= h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h)"

   165   unfolding mbind_def by (simp add: split_def expand_fun_eq)

   166

   167 lemma

   168   mbind_fcomp [simp]: "(f \<guillemotright>= g) \<guillemotright> h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright> h)"

   169   unfolding mbind_def fcomp_def by (simp add: split_def expand_fun_eq)

   170

   171 lemma

   172   fcomp_mbind [simp]: "(f \<guillemotright> g) \<guillemotright>= h = f \<guillemotright> (g \<guillemotright>= h)"

   173   unfolding mbind_def fcomp_def by (simp add: split_def expand_fun_eq)

   174

   175 lemma

   176   fcomp_fcomp [simp]: "(f \<guillemotright> g) \<guillemotright> h = f \<guillemotright> (g \<guillemotright> h)"

   177   unfolding fcomp_def o_assoc ..

   178

   179 lemmas monad_simp = run_simp return_mbind mbind_return

   180   mbind_mbind mbind_fcomp fcomp_mbind fcomp_fcomp

   181

   182 text {*

   183   Evaluation of monadic expressions by force:

   184 *}

   185

   186 lemmas monad_collapse = monad_simp o_apply o_assoc split_Pair split_comp

   187   mbind_def fcomp_def run_def

   188

   189 subsection {* Syntax *}

   190

   191 text {*

   192   We provide a convenient do-notation for monadic expressions

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

   194   specially in do-expressions.

   195 *}

   196

   197 nonterminals do_expr

   198

   199 syntax

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

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

   202   "_mbind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"

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

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

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

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

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

   208   "_nil" :: "'a \<Rightarrow> do_expr"

   209     ("_" [12] 12)

   210

   211 syntax (xsymbols)

   212   "_mbind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"

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

   214

   215 translations

   216   "_do f" => "State_Monad.run f"

   217   "_mbind x f g" => "f \<guillemotright>= (\<lambda>x. g)"

   218   "_fcomp f g" => "f \<guillemotright> g"

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

   220   "_nil f" => "f"

   221

   222 print_translation {*

   223 let

   224   val syntax_name = Sign.const_syntax_name (the_context ());

   225   val name_mbind = syntax_name "State_Monad.mbind";

   226   val name_fcomp = syntax_name "State_Monad.fcomp";

   227   fun unfold_monad (t as Const (name, _) $f$ g) =

   228         if name = name_mbind then let

   229             val ([(v, ty)], g') = Term.strip_abs_eta 1 g;

   230           in Const ("_mbind", dummyT) $Free (v, ty)$ f $unfold_monad g' end   231 else if name = name_fcomp then   232 Const ("_fcomp", dummyT)$ f $unfold_monad g   233 else t   234 | unfold_monad (Const ("Let", _)$ f $g) =   235 let   236   237 val ([(v, ty)], g') = Term.strip_abs_eta 1 g;   238 in Const ("_let", dummyT)$ Free (v, ty) $f$ unfold_monad g' end

   239     | unfold_monad (Const ("Pair", _) $f) =   240 Const ("return", dummyT)$ f

   241     | unfold_monad f = f;

   242   fun tr' (f::ts) =

   243     list_comb (Const ("_do", dummyT) \$ unfold_monad f, ts)

   244 in [

   245   (syntax_name "State_Monad.run", tr')

   246 ] end;

   247 *}

   248

   249 text {*

   250   For an example, see HOL/ex/CodeRandom.thy (more examples coming soon).

   251 *}

   252

   253 end