[Agda] no-eta-equality

[Andrea Vezzosi]

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