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

[Florian Haftmann]

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 ; 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;
> >  

Re: [isabelle-dev] A note on composition in src/Pure/library.ML

[Lawrence Paulson]

I’m not sure what to conclude from this. It’s about non-functional behaviour, 
so not quite something people ought to rely upon.

I’m guessing one could make the change and nothing would happen. I’m still not 
convinced that the case for a change has been made however.

For what it’s worth, there are no such operators in HOL Light.

Larry

> On 22 Jan 2017, at 08:18, Florian Haftmann 
>  wrote:
> 
> Surprisingly (?), there is no error here. The reason is obvious when
> inspecting src/Pure/library.ML:
> 
> ML ‹
> fun (f oo g) x y = f (g x y);
> fun (f ooo g) x y z = f (g x y z);
> fun (f  g) x y z w = f (g x y z w);
> ›
> 
> The composition operators always wait for all arguments to be applied!
> Alternative definitions would be
> 
> ML ‹
> fun (f oo g) x = f o g x;
> fun (f ooo g) x  = f oo g x;
> fun (f  g) x = f ooo g x;
> ›
>   
> ML_val ‹
> fun foo k = error (string_of_int (k + 1));
>   
> val bar = I oo foo;
>   
> val _ = bar 41;
> ›
> 
> Yielding the expected error.
> 
> I am not sure whether this is a striking argument to change such
> long-standing definitions dating back to c755dfd02509 in 1998. But it is
> at least worth noting that these are not apt for partial application.
> 

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