[Agda] 'Dummie' question - why records?

[Wojciech Jedynak]

> Hallo Agdanistas,

Hello Dirk,

> maybe this is a stupid question: Why do we have, beside type
> declarations using `data', declarations for record types by `record'
> in Agda?
> 1. Cannot, at least in principle, any n-fold record type be replaced
> by an appropriate n-fold product over the same types?
> 2. If the anwser to 1. is yes: what is the rationale of having
> `record' beside `data'?

I don't know about the theoretical nuances concerning records, but I
also think that the answer to 1. is yes - for example, sigma types can
be defined using an inductive definition.
My guess would be that records are included for practical reasons. One
could simulate them using a data definition, but a lot of boilerplate
code would be required for each and every definition to get the
projections. Using records you get all the projections for free.
Additionally, a helper module is generated for every record (also for
free ;)), which allows you to i.e. create a virtual
accessor/projection.

For more example about what you *do* with records, take a look at:
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Records

Greetings,
Wojciech Jedynak