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

[Florian Haftmann]

Hi Lukas,

thanks for the offer.  We have still time before the next release to
work that out.  Just give me a sign when you start to dig into this.

All the best,
Florian


Am 21.01.2017 um 18:33 schrieb Lukas Bulwahn:
> Hi Florian,
> 
> I have been quite busy the last few days and hence did find the time
> to answer you email quickly.
> 
>> 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:
> 
> Quickcheck Narrowing inherently uses Haskell's lazy evaluation to have
> a evaluation engine that implements narrowing without actually
> transforming the program that is evaluated.
> 
> The real ideas how to implement narrowing in Haskell come from the
> original authors of LazySmallCheck; the main contribution to make this
> possible in Isabelle is largely the engineering question how to
> combine the ideas from LazySmallCheck with the Isabelle code
> generator. As I was investigating this, I did some further extensions
> to allow existential quantifiers, but this is technically not that
> difficult to implement.
> 
> There is a bit of documentation describing the implementation in my thesis.
> At the moment, I am a little bit busy, but hopefully mid of February,
> I could assist looking into this.
> 
> Maintaining Quickcheck Narrowing has not been a major tasks in the
> last years there was no need to change anything as tricky as the point
> that we encounter now. Hence, I would expect that maintenance will
> continue to be low, once we resolved this issue.
> 
> Lukas
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Florian Haftmann]

Hi Andreas,

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 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 ; if I understand
>>  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
>>> >> <   } 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