[Agda] 'Dummie' question - why records?

[Daniel Peebles]

Records have eta, meaning in a sense that Agda "knows" that there's a
constructor whenever it has a value of the record type.

The difference between:

record True' : Set where
  constructor tt

and

data True' : Set where
  tt : True'

is that in the former case, you can prove:

alwaysTrue :: (t : True) -> t == tt
alwaysTrue _ = refl -- note that there's no pattern matching

in the latter case,

alwaysTrue' :: (t : True') -> t = tt
alwaysTrue tt = refl -- this won't work without pattern matching on tt


>From a practical standpoint, it means that you can assert to Agda that your
function that returns a certain type (say a pair) always produces an
inhabited value. On the other hand, single-constructor data types may not be
inhabited if their indices can't be satisfied (take refl and the equality
type, for example).

- Dan

On Mon, Oct 17, 2011 at 1:27 PM, Dirk Ullrich
<dirk.ullrich at googlemail.com>wrote:

> Hallo Agdanistas,
>
> 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'?
>
> Dirk
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20111017/39dc855a/attachment.html