[isabelle-dev] Irrefutable patterns in Haskell and Quickcheck/Narrowing
Andreas Lochbihler
andreas.lochbihler at inf.ethz.ch
Sat Jan 14 10:03:14 CET 2017
Hi Florian,
Lukas may be able to answer this question better, but here's a comment: You do not need
the lazy treatment of irrefutable patterns in Haskell as a primitive, because it is easy
to emulate using selectors. That is, if we have a single-constructor HOL datatype
dataype 'a T = C (s1: 'a) (s2: 'a T) (s3: 'a T list)
then we can introduce a copy of the case operator by
definition case_lazy_T where "case_lazy_T = case_T"
lemma [code]: "case_lazy_T f x = f (s1 x) (s2 x) (s3 x)"
Now, when you want to use the semantics of irrefutable patterns in let-bindings, use
case_lazy_T in the code equation. If you really want to force the evaluation, then use
case_T and compile it with the new scheme.
I have not tried this, but my guess is that if you do it this way for the three types
narrowing_type narrowing_term narrowing_cons of Quickcheck_Narrowing and adjust the code
equations for the constants in Quickcheck_Narrowing accordingly, then you get back the old
behaviour.
Hope this helps,
Andreas
On 14/01/17 09:33, Florian Haftmann wrote:
> 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
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
More information about the isabelle-dev
mailing list