[isabelle-dev] Irrefutable patterns in Haskell and Quickcheck/Narrowing
Andreas Lochbihler
andreas.lochbihler at inf.ethz.ch
Mon Jan 23 09:39:26 CET 2017
Hi Florian,
On 21/01/17 16:56, Florian Haftmann wrote:
> unfortunately, a selector-based solution didn't either yield a
> terminating example.
>
> If you like you can inspect the attached code, maybe I did get something
> wrong.
>
I am afraid, I am busy with other stuff and won't have the time to dig into the details. I
hope that Lukas will be able to find out what is going wrong.
Andreas
> I will resonsider this in approx. one week; maybe we have to raise the
> question seriously how maintenance of quickcheck/narrowing can go on.
>
> Cheers,
> Florian
>
> Am 14.01.2017 um 10:03 schrieb Andreas Lochbihler:
>> 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
>>>
>>>
>> _______________________________________________
>> 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