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@tcs.inf.tu-dresden.de