[Agda] 'Dummie' question - why records?

[Alan Jeffrey]

In the past, I've used single-constructor datatypes precisely to switch 
off η-reduction, since I was getting horrible performance from records. 
This was before the recent improvement of projection functions though, 
so the need for non-η-equivalent datatypes might not be as strong as it 
used to be.

A.

On 10/18/2011 04:05 AM, Nils Anders Danielsson wrote:
> On 2011-10-17 20:07, Daniel Peebles wrote:
>> Records have eta, meaning in a sense that Agda "knows" that there's a
>> constructor whenever it has a value of the record type.
>
> One might wonder why we don't simply implement η-equality for, say,
> non-recursive single-constructor data types. One reason is that, while
> there are many situations in which η-equality is nice to have, there are
> some where it's nice not to have η. Ulf's "inspect on steroids" is one
> example.
>