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

[Florian Haftmann]

Hi Andreas,

thanks for that quick reply.  This could be done in any case, sure.

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

-- 

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/20170114/5b2fba16/attachment.sig>