Dear all,
any opinions on making the type of monadic bind more general (see the
attached patch)?
For my motivation see the farther below.
I tested the change against IsaFoR (which makes heavy use of
Monad_Syntax). Unfortunately, running JinjaThreads (which also uses
Monad_Syntax) timed out on my machine (hopefully not due to the patch).
Could anybody with access to a more powerful machine check this please?
Motivation:
I'm currently writing a small combinator parser library in Isabelle/HOL,
where (for reasons of totality) I have two types of parsers (both are
typedefs carved out from the function space "'a list => string + ('b *
'a list)":
- standard parsers (with the invariant that the remaining input after
parsing is not longer than before), and
- "consuming" parsers (with the invariant that the remaining input
after parsing is strictly shorter than before).
Then it is possible to have (recursive) combinators like (where types
are simplified for readability)
many :: "'a cparser => ('a list) parser"
where totality of "many p" relies on the fact that "p" consumes at least
one token. (Of course, it is trivial to turn a consuming parser into a
standard one.) Now for bind: let "p", "f" be standard and "cp" and "cf"
be consuming. Then suitable combinations that yield consuming parsers are:
cp >>= cf, p >>= cf, and cp >>= f
But until now the type of "Monad_Syntax.bind" was "'a => ('b => 'c) =>
'c" which does not allow the last combination (since the result of "f"
is not consuming, but "cp >>= f" is).
Concerning readability it would be neat if I could overload "bind" for
all these cases.
Any comments?
cheers
chris
# HG changeset patch
# User Christian Sternagel
# Date 1376987651 -32400
# Tue Aug 20 17:34:11 2013 +0900
# Node ID 4808a6ae009b22369d71658c64369574d6adea83
# Parent 7e89edba3db64dad93dadac77a9e64d45ffcfe49
more general typing of monadic bind
diff --git a/src/HOL/Library/Monad_Syntax.thy b/src/HOL/Library/Monad_Syntax.thy
--- a/src/HOL/Library/Monad_Syntax.thy
+++ b/src/HOL/Library/Monad_Syntax.thy
@@ -15,7 +15,7 @@
*}
consts
- bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c" (infixr ">>=" 54)
+ bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd" (infixr ">>=" 54)
notation (xsymbols)
bind (infixr "\<guillemotright>=" 54)
@@ -24,7 +24,7 @@
bind (infixr "\<bind>" 54)
abbreviation (do_notation)
- bind_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c"
+ bind_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd"
where
"bind_do \<equiv> bind"
@@ -46,14 +46,14 @@
"_do_then" :: "'a \<Rightarrow> do_bind" ("_" [14] 13)
"_do_final" :: "'a \<Rightarrow> do_binds" ("_")
"_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds" ("_;//_" [13, 12] 12)
- "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr ">>" 54)
+ "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr ">>" 54)
syntax (xsymbols)
"_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ \<leftarrow>/ _)" 13)
- "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr "\<guillemotright>" 54)
+ "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr "\<guillemotright>" 54)
syntax (latex output)
- "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr "\<then>" 54)
+ "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr "\<then>" 54)
translations
"_do_block (_do_cons (_do_then t) (_do_final e))"
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
