<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><br class="">
<div><br class=""><blockquote type="cite" class=""><div class="">On 5 Jun 2019, at 14:48, Jesper Cockx <<a href="mailto:Jesper@sikanda.be" class="">Jesper@sikanda.be</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class=""><div class="">I guess most of the reasons why one would use a record type instead of a single-constructor datatype still apply:</div><div class="">- You get the projections for free</div><div class="">- You can define new elements using copatterns</div></div></div></blockquote><div><br class=""></div><div>maybe so, but I think I’m going to impose the no-records-in-Prop restriction manually until I’m forced to give it up </div><div><br class=""></div><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class="">- You can make the record coinductive if needed</div></div></div></blockquote><div><br class=""></div><div>whoa! coinductively defined propositions, now there’s a thought…</div><div><br class=""></div><div>A :-)</div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><br class=""></div><div class="">-- Jesper<br class=""></div></div><br class=""><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Jun 5, 2019 at 3:46 PM Andrew Pitts <<a href="mailto:andrew.pitts@cl.cam.ac.uk" class="">andrew.pitts@cl.cam.ac.uk</a>> wrote:<br class=""></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div style="overflow-wrap: break-word;" class="">Dear Jesper,<br class="">
<div class=""><br class=""><blockquote type="cite" class=""><div class="">On 5 Jun 2019, at 13:34, Jesper Cockx <<a href="mailto:Jesper@sikanda.be" target="_blank" class="">Jesper@sikanda.be</a>> wrote:</div><br class="gmail-m_7757473178893307641Apple-interchange-newline"><div class=""><div dir="ltr" class=""><div class="">Hi Andy,</div><div class=""><br class=""></div><div class="">When you define a datatype in Prop, the resulting type is automatically 'squashed', i.e. any two elements are equal. In contrast, for record types this is not possible because then it is impossible to define the projections. For your definition of ∃ in Prop, (true , _) is equal to (false , _) of type `∃ Bool (λ _ → ⊤)`, but their first projections are not equal. It would theoretically be possible to have such a record type but not give access to the projections and disabling eta-equality, but then you could've equally defined it as a single-constructor datatype.</div></div></div></blockquote><div class=""><br class=""></div>I see. So to paraphrase your explanation, Agda imposes a simple syntactic restriction on what record types can be declared to have type Prop in order to maintain the soundness of forcing all elements of an element of a Prop to be definitionally equal.</div><div class=""><br class=""></div><div class="">I can think of a simple syntactic restriction that is less liberal than the current one: don’t allow record types in Prop! Is there an example of why my restriction is too restrictive? —- in other words a case where using a record of Prop type is really better than using a corresponding single-constructor datatype of type Prop?</div><div class=""><br class=""></div><div class="">(I am thinking that one often uses a record type in Set instead of a single-constructor-datatype in Set, in order to get definitional eta expansion; but that’s automatic for elements of Prop, due to the definitional proof irrelevance.)</div><div class=""><br class=""></div><div class="">Andy</div><div class=""><div class=""><br class=""></div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><br class=""></div><div class="">-- Jesper<br class=""></div></div><br class=""><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Jun 5, 2019 at 1:09 PM Andrew Pitts <<a href="mailto:andrew.pitts@cl.cam.ac.uk" target="_blank" class="">andrew.pitts@cl.cam.ac.uk</a>> wrote:<br class=""></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Here is another question about Prop in Agda 2.6. Can anyone enlighten me?<br class="">
<br class="">
The documentation says<br class="">
<br class="">
"Just as for Set, we can define new types in Prop’s as data or record types”<br class="">
<br class="">
However, although Agda 2.6 allows the declaration of the following one-constructor datatype<br class="">
<br class="">
data ∃ {l m}(A : Set l)(P : A → Prop m) : Prop (l ⊔ m) where<br class="">
_,_ : (x : A)(p : P x) → ∃ A P<br class="">
<br class="">
if instead I try to define a record type<br class="">
<br class="">
record ∃ {l m : Level}(A : Set l)(B : A → Prop m) : Prop (l ⊔ m) where<br class="">
constructor _,_<br class="">
field<br class="">
fst : A<br class="">
snd : B fst<br class="">
<br class="">
Agda complains (somewhat ungrammatically) that <br class="">
<br class="">
"Set l is not less or equal than Prop (l ⊔ m) when checking the definition of ∃”<br class="">
<br class="">
So it doesn’t mind the parameter (A : Set l) when defining a datatype in Prop (l ⊔ m), but does mind it when defining a record type.<br class="">
<br class="">
Why is that?<br class="">
<br class="">
Andy<br class="">
<br class="">
<br class="">
_______________________________________________<br class="">
Agda mailing list<br class="">
<a href="mailto:Agda@lists.chalmers.se" target="_blank" class="">Agda@lists.chalmers.se</a><br class="">
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank" class="">https://lists.chalmers.se/mailman/listinfo/agda</a><br class="">
</blockquote></div>
</div></blockquote></div><br class=""></div></blockquote></div>
</div></blockquote></div><br class=""></body></html>