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

[Florian Haftmann]

Hi Lukas,

I am currently stuck with a problem in Quickcheck/Narrowing.

After about 10 years it came to surface that code generation for Haskell
may produce irrefutable patterns due to pattern bindings in let clauses.
See <https://wiki.haskell.org/Lazy_pattern_match>; if I understand
<https://www.haskell.org/tutorial/patterns.html> correctly that
particular semantics allows fancy definitions like the following
fibonacci one-liner: »fib @ (1 : more_fib) = 1 : 1 : [ a + b | (a, b) <-
zip fib more_fib ]«.

However the partial correctness approach of the code generator assumes
that pattern match clauses may silently be dropped, which is made use of
to translate the HOL-ish »partial« undefined conveniently. This breaks
down in presence of irrefutable patterns (see the post on isabelle-users
by Rene Thiemann).

The correction is obvious: for Haskell, only local variables may be
bound by let clauses, but never patterns – these are solely bound by
case clauses, which are strict in Haskell (as in function equations).

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:

The same before and after:
	Typerep.hs

Then the difference occurs:
	Generated_Code.hs
	Before: Generated_Code.A.hs
	After: Generated_Code.B.hs

The same before and after:
	Narrowing_Engine.hs
	Main.hs

The diff ist straight-forward to read:

> 	93,102c93,106
> 	<   let {
> 	<     (Narrowing_cons (Narrowing_sum_of_products ps) cfs) = f d;
> 	<     (Narrowing_cons ta cas) = a (d - (1 :: Prelude.Int));
> 	<     shallow = (0 :: Prelude.Int) < d && non_empty ta;
> 	<     aa = (if shallow then map (\ cf (x : xs) -> cf xs (conv cas x)) cfs
> 	<            else []);
> 	<   } in Narrowing_cons
> 	<          (Narrowing_sum_of_products
> 	<            (if shallow then map (\ ab -> ta : ab) ps else []))
> 	<          aa;
> 	---
> 	>   (case f d of {
> 	>     Narrowing_cons (Narrowing_sum_of_products ps) cfs ->
> 	>       (case a (d - (1 :: Prelude.Int)) of {
> 	>         Narrowing_cons ta cas ->
> 	>           let {
> 	>             shallow = (0 :: Prelude.Int) < d && non_empty ta;
> 	>             aa = (if shallow then map (\ cf (x : xs) -> cf xs (conv cas x)) cfs
> 	>                    else []);
> 	>           } in Narrowing_cons
> 	>                  (Narrowing_sum_of_products
> 	>                    (if shallow then map (\ ab -> ta : ab) ps else []))
> 	>                  aa;
> 	>       });
> 	>   });
> 	112,115c116,122
> 	<   let {
> 	<     (Narrowing_cons (Narrowing_sum_of_products ssa) ca) = a d;
> 	<     (Narrowing_cons (Narrowing_sum_of_products ssb) cb) = b d;
> 	<   } in Narrowing_cons (Narrowing_sum_of_products (ssa ++ ssb)) (ca ++ cb);
> 	---
> 	>   (case a d of {
> 	>     Narrowing_cons (Narrowing_sum_of_products ssa) ca ->
> 	>       (case b d of {
> 	>         Narrowing_cons (Narrowing_sum_of_products ssb) cb ->
> 	>           Narrowing_cons (Narrowing_sum_of_products (ssa ++ ssb)) (ca ++ cb);
> 	>       });
> 	>   });

Unfortunately my knowledge is too restricted what could be done here to
restore the intended behaviour economically.

Hence I ask whether you have an idea what is going wrong here.

Thanks a lot!

	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Quickcheck_Narrowing_Examples.thy
Type: application/x-extension-thy
Size: 300 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20170114/573758b9/attachment.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Generated_Code.A.hs
Type: text/x-haskell
Size: 6377 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20170114/573758b9/attachment.hs>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Generated_Code.B.hs
Type: text/x-haskell
Size: 6528 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20170114/573758b9/attachment-0001.hs>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Main.hs
Type: text/x-haskell
Size: 243 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20170114/573758b9/attachment-0002.hs>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Narrowing_Engine.hs
Type: text/x-haskell
Size: 4725 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20170114/573758b9/attachment-0003.hs>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Typerep.hs
Type: text/x-haskell
Size: 69 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20170114/573758b9/attachment-0004.hs>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20170114/573758b9/attachment.asc>