[Agda] no-eta-equality

[Andrea Vezzosi]

On Mon, Sep 26, 2016 at 2:37 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> ...
> And how the --no-eta-equality option correlates with the `constructor'
> declaration in a record? It there any difference of whether this
> declaration is set or not?

You can have or not have a constructor, though I would strongly
suggest that you add one otherwise some proofs might be impossible,
e.g. the proof that "fst x , snd x" and "x" are prop. equal would go
by pattern matching on x.

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

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.


e.g. with Pair defined with --no-eta-equality as before, and these definitions

foo : Pair Nat Nat
fst foo = e1
snd foo = e2

bar : Pair Nat Nat
fst bar = e3
snd bar = e4

We will have that the typechecker will simply fail when comparing
"foo" and "bar", without having to look at or reduce the possibly big
expressions e1,e2,e3,e4.
This is because foo (and same for bar) does not reduce further, only
"fst foo" and "snd foo" reduce. However "fst foo" and "snd foo"
reducing is not relevant for equality checking because we disabled eta
for Pair.

You will not have this advantage if you use the constructor instead,
because if we have

foo' = (e1 , e2)
bar' = (e3 , e4)

then comparing foo' and bar' means comparing (e1 , e2) and (e3 , e4).

However notice that this is not for free, now you have that fewer
things are equal, e.g. if we define foo2 as

foo2 : Pair Nat Nat
fst   foo2 = e1
snd foo2 = e2

then foo and foo2 are still going to be considered different, even if
their bodies are the same.


Best,
Andrea

>
> Thanks,
>
> ------
> Sergei
>
>
>
>
>
>
>> On Mon, Sep 26, 2016 at 11:33 AM, Sergei Meshveliani <mechvel at botik.ru> wrote:
>> > People,
>> > I am trying to use the  no-eta-equality  key in order to reduce space
>> > eagerness of the type checker.
>> >
>> > And there arise several questions.
>> >
>> > 1. Currently the project is successfully type-checked by
>> >    agda $agdaLibOpt +RTS ... -RTS TypeCheckAll.agda
>> >
>> > Now, I set  {-# OPTIONS --no-eta-equality #-}
>> > to the head of each .agda file.
>> >
>> > Then, several files are type-checked, and others are not.
>> > Is this a bug in Agda?
>> >
>> > 2. Does the above {-# OPTIONS --no-eta-equality #-} apply only to
>> > records, or to all functions?
>> >
>> > 3. I understand eta-equality as that Agda converts
>> >    lambda x.(f x) --> f,  everywhere where x does not occur in the
>> > lambda term f
>> > -- is Agda so?
>> > Also record is internally related to a lambda term, where the above x is
>> > matched against the record labels
>> > -- is this so?
>> >
>> > 4. In my program,  Semigroup, Group, Ring ... (many of them) are records
>> > in which one structure is often a field value for another structure.
>> > Do I need to set  --no-eta-equality  not to the whole files but
>> > individually to each record declaration of Semigroup, Group, Ring ...,
>> > and not to touch other parts?
>> >
>> > Thanks,
>> >
>> > ------
>> > Sergei
>> >
>> > _______________________________________________
>> > Agda mailing list
>> > Agda at lists.chalmers.se
>> > https://lists.chalmers.se/mailman/listinfo/agda
>>
>
>