[isabelle-dev] Irrefutable patterns in Haskell and Quickcheck/Narrowing

[Lukas Bulwahn]

Hi Florian,

I have been quite busy the last few days and hence did find the time
to answer you email quickly.

> This however breaks Quickcheck/Narrowing where the lazy nature of
> pattern bindings has been exploited, may be unconsciously. A minimal
> example is attached (Quickcheck_Narrowing_Examples.thy) but I also
> distilled the generated Haskell code:

Quickcheck Narrowing inherently uses Haskell's lazy evaluation to have
a evaluation engine that implements narrowing without actually
transforming the program that is evaluated.

The real ideas how to implement narrowing in Haskell come from the
original authors of LazySmallCheck; the main contribution to make this
possible in Isabelle is largely the engineering question how to
combine the ideas from LazySmallCheck with the Isabelle code
generator. As I was investigating this, I did some further extensions
to allow existential quantifiers, but this is technically not that
difficult to implement.

There is a bit of documentation describing the implementation in my thesis.
At the moment, I am a little bit busy, but hopefully mid of February,
I could assist looking into this.

Maintaining Quickcheck Narrowing has not been a major tasks in the
last years there was no need to change anything as tricky as the point
that we encounter now. Hence, I would expect that maintenance will
continue to be low, once we resolved this issue.

Lukas