Records have eta, meaning in a sense that Agda &quot;knows&quot; that there&#39;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&#39; : Set where</div>
<div>  constructor tt</div><div><br></div><div>and </div><div><br></div><div>data True&#39; : Set where</div><div>  tt : True&#39;</div><div><br></div><div>is that in the former case, you can prove:</div><div><br></div><div>
alwaysTrue :: (t : True) -&gt; t == tt</div><div>alwaysTrue _ = refl -- note that there&#39;s no pattern matching</div><div><br></div><div>in the latter case,</div><div><br></div><div>alwaysTrue&#39; :: (t : True&#39;) -&gt; t = tt</div>
<div>alwaysTrue tt = refl -- this won&#39;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&#39;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">&lt;<a href="mailto:dirk.ullrich@googlemail.com">dirk.ullrich@googlemail.com</a>&gt;</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&#39;, declarations for record types by `record&#39;<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&#39; beside `data&#39;?<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>