c.sternagel at gmail.com
Tue Aug 20 10:49:59 CEST 2013
any opinions on making the type of monadic bind more general (see the
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?
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 *
- 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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 1695 bytes
Desc: not available
More information about the isabelle-dev