[Agda] Pattern matching weirdness?

[Wojciech Jedynak]

2011/12/19 Pierre Hyvernat <pierre.hyvernat at univ-savoie.fr>:
>
>> If you want eta-expansion of ∑, you should define it as a "record", as in
>> the standard library.
>>
> OK.
> However, using record prevents you from defining functions by pattern
> matching, doesn't it?

Not really, it suffices to add an explicit constructor (see [1]) and
then you can pattern match on records (see [2]).

[1] http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Records#Explicitrecordconstructors
[2] http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Records#pattern-details

> Mmm...
> Is there a reason we don't want eta-expansion on data (surjective pairing),
> or is this just an implementation artefact?

There has been a discussion about this matter not that long ago (I
added some notes to the wiki: [3]).
I think it might be connected to the fact that records can't be
indexed while inductive families can.
I'm not sure about it, so I'll just reference the previous thread: [4].

[3] http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Records#versus_data
[4] https://lists.chalmers.se/pipermail/agda/2011/003394.html

Greetings,
Wojtek