[isabelle-dev] Monad_Syntax

[Christian Sternagel]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: bind.patch
Type: text/x-patch
Size: 1695 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130820/384b4d94/attachment.bin>