[Agda] no-eta-equality

[Andrea Vezzosi]

>The pragma {-# OPTIONS --no-eta-equality #-} affects how the
> typechecker compares elements of record types defined inside that
> module.

I mean that it affects the types defined inside that module, even when
you use them or define elements of them inside other modules.



On Mon, Sep 26, 2016 at 2:12 PM, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:
> Hi Sergei,
>
> The pragma {-# OPTIONS --no-eta-equality #-} affects how the
> typechecker compares elements of record types defined inside that
> module. Lambdas are unaffected.
>
> Consider the following record type
>
> record Pair (A B : Set) : Set where
>   constructor _,_
>   field
>     fst : A
>     snd : A
>
> Normally we have that given "x : Pair A B" then "fst x , snd x" is the
> same as "x" for the type-checker.
> However if "Pair" is defined with --no-eta-equality then, in general,
> "fst x , snd x" and "x" are only going to be propositionally equal.
>
> In other words equality for Pair with --no-eta-equality works very
> much the same as if Pair was defined as a datatype:
>
> data Pair (A B : Set) : Set where
>   _,_ : A -> B -> Pair A B
>
> fst (a , b) = a
> snd (a , b) = b
>
> Best,
> Andrea
>
>
> 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