[Agda] 'Dummie' question - why records?
pumpkingod at gmail.com
Mon Oct 17 20:07:11 CEST 2011
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
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).
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'?
> Agda mailing list
> Agda at lists.chalmers.se
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Agda