[Haskell-cafe] Re: Optimizing 'sequence'

[Janis Voigtlaender]

Gracjan Polak wrote:
> How do I reason if >>= for parsers is lazy in its first argument?

Well, to quote from the abstract of the paper I already mentioned
(http://citeseer.ist.psu.edu/704350.html): "By testing before proving we
avoid wasting time trying to prove statements that are not valid."

I think the library described in the paper, available here:

http://www.cs.nott.ac.uk/~nad/software/#Chasing%20Bottoms

has what you need. For example, you can check for isBottom, combine this
with random test case generation, and thus should be able to quickly
get an informed hypothesis about whether or not your >>= is lazy. For
then proving that hypothesis, the paper (and probably other papers it
cites) also provides some techniques that might be of use to you.

Ciao, Janis.

-- 
Dr. Janis Voigtlaender
http://wwwtcs.inf.tu-dresden.de/~voigt/
mailto:voigt at tcs.inf.tu-dresden.de