[isabelle-dev] Irrefutable patterns in Haskell and Quickcheck/Narrowing
Florian Haftmann
florian.haftmann at informatik.tu-muenchen.de
Mon Jan 23 18:30:05 CET 2017
Hi Andreas,
that should be fine. I am optimistic that we will manage somehow to
work that our during February.
Cheers,
Florian
Am 23.01.2017 um 09:39 schrieb Andreas Lochbihler:
> 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
>>>
>>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
--
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: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170123/4788acdf/attachment.sig>
More information about the isabelle-dev
mailing list