[Agda] no-eta-equality

[Sergei Meshveliani]

On Mon, 2016-09-26 at 14:12 +0200, Andrea Vezzosi 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.
> [..]


I see. Thank you for explanation.

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?

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?

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
>