author haftmann Fri Aug 10 17:10:05 2007 +0200 (2007-08-10) changeset 24224 a5c95bbeb31d parent 24195 7d1a16c77f7c child 24253 3d7f74fd9fd9 permissions -rw-r--r--
syntax fix
     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 subsection {* Motivation *}

    13

    14 text {*

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

    16   it is not possible to model monads the Haskell way

    17   in full genericity in Isabelle/HOL.

    18

    19   However, this theory provides substantial support for

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

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

    22   is transformed single-threaded).

    23

    24   To enter from the Haskell world,

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

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

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

    28 *}

    29

    30 subsection {* State transformations and combinators *}

    31

    32 (*<*)

    33 typedecl \<alpha>

    34 typedecl \<beta>

    35 typedecl \<gamma>

    36 typedecl \<sigma>

    37 typedecl \<sigma>'

    38 (*>*)

    39

    40 text {*

    41   We classify functions operating on states into two categories:

    42

    43   \begin{description}

    44     \item[transformations]

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

    46       transforming a state.

    47     \item[yielding'' transformations]

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

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

    50     \item[queries]

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

    52       computing a result dependent on a state.

    53   \end{description}

    54

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

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

    57   for types representing side results.  Type changes due

    58   to transformations are not excluded in our scenario.

    59

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

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

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

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

    64   we use a set of monad combinators:

    65 *}

    66

    67 definition

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

    69     (infixl ">>=" 60) where

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

    71

    72 definition

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

    74     (infixl ">>" 60) where

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

    76

    77 definition

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

    79   "run f = f"

    80

    81 syntax (xsymbols)

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

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

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

    85     (infixl "\<guillemotright>" 60)

    86

    87 abbreviation (input)

    88   "return \<equiv> Pair"

    89

    90 print_ast_translation {*

    91   [(@{const_syntax "run"}, fn (f::ts) => Syntax.mk_appl f ts)]

    92 *}

    93

    94 text {*

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

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

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

    98

    99   After any yielding transformation, we bind the side result

   100   immediately using a lambda abstraction.  This

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

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

   103

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

   105

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

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

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

   109

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

   111

   112   The most crucial distinction to Haskell is that we do

   113   not need to introduce distinguished type constructors

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

   115   \begin{itemize}

   116     \item The monad model does not state anything about

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

   118        completely orthogonal and has to (or may) be

   119        specified completely independent.

   120     \item There is no distinguished type constructor

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

   122        may be applied directly without using any lifting

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

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

   125   \end{itemize}

   126 *}

   127

   128

   129 subsection {* Obsolete runs *}

   130

   131 text {*

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

   133 *}

   134

   135 lemma run_simp [simp]:

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

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

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

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

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

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

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

   143   unfolding run_def by rule+

   144

   145 subsection {* Monad laws *}

   146

   147 text {*

   148   The common monadic laws hold and may also be used

   149   as normalization rules for monadic expressions:

   150 *}

   151

   152 lemma

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

   154   unfolding mbind_def by (simp add: expand_fun_eq)

   155

   156 lemma

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

   158   unfolding mbind_def by (simp add: expand_fun_eq split_Pair)

   159

   160 lemma

   161   id_fcomp [simp]: "id \<guillemotright> f = f"

   162   unfolding fcomp_def by simp

   163

   164 lemma

   165   fcomp_id [simp]: "f \<guillemotright> id = f"

   166   unfolding fcomp_def by simp

   167

   168 lemma

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

   170   unfolding mbind_def by (simp add: split_def expand_fun_eq)

   171

   172 lemma

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

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

   175

   176 lemma

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

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

   179

   180 lemma

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

   182   unfolding fcomp_def o_assoc ..

   183

   184 lemmas monad_simp = run_simp return_mbind mbind_return id_fcomp fcomp_id

   185   mbind_mbind mbind_fcomp fcomp_mbind fcomp_fcomp

   186

   187 text {*

   188   Evaluation of monadic expressions by force:

   189 *}

   190

   191 lemmas monad_collapse = monad_simp o_apply o_assoc split_Pair split_comp

   192   mbind_def fcomp_def run_def

   193

   194 subsection {* Syntax *}

   195

   196 text {*

   197   We provide a convenient do-notation for monadic expressions

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

   199   specially in do-expressions.

   200 *}

   201

   202 nonterminals do_expr

   203

   204 syntax

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

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

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

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

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

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

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

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

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

   214     ("_" [12] 12)

   215

   216 syntax (xsymbols)

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

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

   219

   220 translations

   221   "_do f" => "CONST run f"

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

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

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

   225   "_nil f" => "f"

   226

   227 print_translation {*

   228 let

   229   fun unfold_monad (Const (@{const_syntax mbind}, _) $f$ Abs (abs as (_, ty, _))) =

   230         let

   231           val (v', g') = Syntax.variant_abs abs;

   232         in Const ("_mbind", dummyT) $Free (v', ty)$ f $unfold_monad g' end   233 | unfold_monad (Const (@{const_syntax fcomp}, _)$ f $g) =   234 Const ("_fcomp", dummyT)$ f $unfold_monad g   235 | unfold_monad (Const (@{const_syntax Let}, _)$ f $Abs (abs as (_, ty, _))) =   236 let   237 val (v', g') = Syntax.variant_abs abs;   238 in Const ("_mbind", dummyT)$ Free (v', ty) $f$ unfold_monad g' end

   239     | unfold_monad (Const (@{const_syntax 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 [(@{const_syntax "run"}, tr')] end;

   245 *}

   246

   247

   248 subsection {* Combinators *}

   249

   250 definition

   251   lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> 'b \<times> 'c" where

   252   "lift f x = return (f x)"

   253

   254 fun

   255   list :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where

   256   "list f [] = id"

   257 | "list f (x#xs) = (do f x; list f xs done)"

   258

   259 fun list_yield :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<times> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'c list \<times> 'b" where

   260   "list_yield f [] = return []"

   261 | "list_yield f (x#xs) = (do y \<leftarrow> f x; ys \<leftarrow> list_yield f xs; return (y#ys) done)"

   262

   263 text {* combinator properties *}

   264

   265 lemma list_append [simp]:

   266   "list f (xs @ ys) = list f xs \<guillemotright> list f ys"

   267   by (induct xs) (simp_all del: id_apply) (*FIXME*)

   268

   269 lemma list_cong [fundef_cong, recdef_cong]:

   270   "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk>

   271     \<Longrightarrow> list f xs = list g ys"

   272 proof (induct f xs arbitrary: g ys rule: list.induct)

   273   case 1 then show ?case by simp

   274 next

   275   case (2 f x xs g)

   276   from 2 have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto

   277   then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto

   278   with 2 have "list f xs = list g xs" by auto

   279   with 2 have "list f (x # xs) = list g (x # xs)" by auto

   280   with 2 show "list f (x # xs) = list g ys" by auto

   281 qed

   282

   283 lemma list_yield_cong [fundef_cong, recdef_cong]:

   284   "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk>

   285     \<Longrightarrow> list_yield f xs = list_yield g ys"

   286 proof (induct f xs arbitrary: g ys rule: list_yield.induct)

   287   case 1 then show ?case by simp

   288 next

   289   case (2 f x xs g)

   290   from 2 have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto

   291   then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto

   292   with 2 have "list_yield f xs = list_yield g xs" by auto

   293   with 2 have "list_yield f (x # xs) = list_yield g (x # xs)" by auto

   294   with 2 show "list_yield f (x # xs) = list_yield g ys" by auto

   295 qed

   296

   297 text {*

   298   still waiting for extensions@{text "\<dots>"}

   299 *}

   300

   301 text {*

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

   303 *}

   304

   305 end