8
$\begingroup$

In a recent development, I used the no-eta-equality attribute on a record. The motivation in that case was ad hoc: I noticed that I'd get better metavariable resolution for uses of definitions like map-⊗ᴿ if I could make _⊗ᴿ_ more opaque. However, it got me wondering whether I could be taking more advantage of no-eta-equality by recognising some patterns in which it is useful.

Are there any best practices or heuristics to decide whether to use no-eta-equality on a given record? Are there cases where both choices are justifiable? And what are the costs and benefits in each case?

Improve this question
$\endgroup$
1
  • $\begingroup$ Perhaps eta-equality would be the better name for the tag, though it's not so different in meaning from eta-conversion (I don't think I'd usually say “eta-conversion” myself – I'd prefer “eta-equality”, “eta-expansion”, or “eta-contraction”, depending on what I wanted to talk about). I don't think this is necessarily an Agda-specific question; the mapping to language-agnostic theoretical concepts is straightforward. I doubt there would be many more questions you could ask with the agda-no-eta-equality tag. $\endgroup$
    – James Wood
    Commented Feb 21, 2022 at 23:34

1 Answer 1

Reset to default
3
$\begingroup$

When you're absolutely sure you don't need it. Then disabling eta equality for a record saves time for Agda. For instance, the Iso type for isomorphism is mostly used to carry the information of an isomorphism, and then convert it to a HoTT-sense of equivalence and then send it to the Glue type former. So, it adds no-eta-equality to improve performance of type checking.

Apart from performance, coinductive records also require the absence of eta equality to work. So if you want to do some beautiful guarded corecursion then you need no-eta-equality. But this is implied by the coinductive keyword which you put at the same place where you put no-eta-equality, so you don't actually need to write it out when using coinductive.

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ I think this leaves out the key part: if I were writing library code, how could I know that no user would need η-equality? IIUC, the example you give works because Iso is essentially a helper structure that we don't pass around terms of. But even this surprises me: it makes smart constructors like isoToEquiv and isoToPath have different elaboration behaviour to uncurried versions of them. $\endgroup$
    – James Wood
    Commented Feb 22, 2022 at 8:31

Not the answer you're looking for? Browse other questions tagged or ask your own question.