[Agda] no-eta-equality

[Andrea Vezzosi]

No, doing that wouldn't be enough to see major improvements.

You have to change definitions that build elements of Foo into ones
that do so by copatterns.

On Tue, Sep 27, 2016 at 12:31 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> To my question on --no-eta-equality
>
>> > Now, if  "fst x , snd x" and "x"  are only going to be
>> > propositionally equal,  why does this reduce the memory size when >
>> > type-checking?
>
>
> On Mon, 2016-09-26 at 15:01 +0200, Andrea Vezzosi wrote:
>
>> As far as I'm aware the biggest benefit comes in combination with
>> copatterns, and it's because more things will be compared "by name"
>> rather than structurally, so there's less reduction and possibly less
>> expansion of terms going on.
>>
>
> I looked into
>          https://gist.github.com/puffnfresh/8960574
>
> to find out of what is a copattern:
>
>   {-# OPTIONS --copatterns #-}
>
>   record _×_ (A B : Set) : Set where
>     constructor _,_
>     field
>       fst : A
>       snd : B
>   open _×_
>
>   pair : {A B : Set} → A → B → A × B
>   fst (pair a b) = a                     -- (1)
>   snd (pair a b) = b                     -- (2)
>
> Probably, this implements the function `pair' on types by saying that it
> satisfies the equations (1) and (2).
> (?)
>
> Now, my program declares many records (a hierarchy of algebraic
> structures). For example (contrived):
>
>   record Foo (A : Set) : Set where
>                              constructor foo
>                              field f1  : A
>                                    nat : Nat
>   open Foo
>
> And in order to reduce the type checking cost, it has sense
> 1) to prefix the files with
>    {-# OPTIONS --copatterns #-},
>
> 2) to set there  no-eta-equality  before `constructor',
>
> 3) to add the functions like
>
>   makeFoo : {A : Set} → A → Foo A
>   f1  (makeFoo a _) = a
>   nat (makeFoo _ n) = n,
>
> that is to add the projection equation for each record field.
>
> And after this, the type check cost for this program has a chance to
> reduce essentially
> (no matter of whether  makeFoo  is used anywhere or not?).
>
> (The program will be so that it defines the projection equations without
> explicitly using them anywhere).
>
> Do I understand correct?
>
> Thank you for explanations,
>
> ------
> Sergei
>
>