Records have eta, meaning in a sense that Agda "knows" that there's a constructor whenever it has a value of the record type.<div><br></div><div>The difference between:</div><div><br></div><div>record True' : Set where</div>
<div> constructor tt</div><div><br></div><div>and </div><div><br></div><div>data True' : Set where</div><div> tt : True'</div><div><br></div><div>is that in the former case, you can prove:</div><div><br></div><div>
alwaysTrue :: (t : True) -> t == tt</div><div>alwaysTrue _ = refl -- note that there's no pattern matching</div><div><br></div><div>in the latter case,</div><div><br></div><div>alwaysTrue' :: (t : True') -> t = tt</div>
<div>alwaysTrue tt = refl -- this won't work without pattern matching on tt</div><div><div><br></div><div><br></div><div>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).</div>
<div><br></div><div>- Dan</div><div><br></div><div><div class="gmail_quote">On Mon, Oct 17, 2011 at 1:27 PM, Dirk Ullrich <span dir="ltr"><<a href="mailto:dirk.ullrich@googlemail.com">dirk.ullrich@googlemail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">Hallo Agdanistas,<br>
<br>
maybe this is a stupid question: Why do we have, beside type<br>
declarations using `data', declarations for record types by `record'<br>
in Agda?<br>
1. Cannot, at least in principle, any n-fold record type be replaced<br>
by an appropriate n-fold product over the same types?<br>
2. If the anwser to 1. is yes: what is the rationale of having<br>
`record' beside `data'?<br>
<br>
Dirk<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div></div>