<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><br class="Apple-interchange-newline"><blockquote type="cite">I had started by using --type-in-type, but I backed off, mainly because I was never entirely sure that Hurkens'/Girard's paradox wasn't lurking in any of my proofs. It kind of defeated the purpose of doing everything so rigorously. ;)<font class="Apple-style-span" color="#000000"><font class="Apple-style-span" color="#144FAE"><br></font></font></blockquote><div><br></div>I understand. However, at least for now none of the proof assistants are entirely trustworthy. It is quite likely that there are other sources of unsoundness, e.g. using inductive recursive definitions in the case of Agda. But I admit that there is a difference between a potential unsoundness (which can be fixed once it is found) and a principal source of unsoundness.</div><div><br></div><div>There is a tension between elegance and ease of expression and trustworthiness. We will only be able to tackle this once we decouple the surface language and a small trusted core language.</div><div><br></div><div>One idea we discussed at the last AIM was to basically implement a universe hierarchy just using Set : Nat -> Type and exploit the usual implicit argument mechanism for universe polymorphism. Ulf implemented a prototype during the meeting:</div><div><a href="http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AIMX">http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AIMX</a></div><div>Maybe he has written more about this?</div><div><br></div><div>Another approach would be to do universe checking like termination checking, i.e. use Type:Type but then check wether this can be stratified. The nice thing is that you wouldn't have to clutter your code with additional indizes. And it is analogue to termination checking, where Agda basically uses general recursion but then checks wether they are structural / guarded. One big disadvantage is that stratification is not a modular property, i.e. you have to check the whole program. But maybe one could live with this.</div><div><br></div><div>Cheers,</div><div>Thorsten</div><div><br></div><div><br><br><blockquote type="cite">-Edward Kmett<br><br><div class="gmail_quote">On Thu, Nov 19, 2009 at 3:09 PM, Thorsten Altenkirch <span dir="ltr"><<a href="mailto:txa@cs.nott.ac.uk">txa@cs.nott.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<div style="word-wrap: break-word;">Hi,<div><br></div><div>Ulf has got an experimental implementation of universe polymorphism. However, I'd think it is too early to reimplement the whole library based on this.</div><div>
<br></div><div>As a stop gap I am using </div><div><div>{-# OPTIONS --type-in-type #-}</div></div><div><br></div><div>It is usually easy to see wether your definitions can be stratified. </div><div><br></div><div>Cheers,</div>
<div>Thorsten</div><div><div></div><div class="h5"><div><br></div><div><div><div>On 19 Nov 2009, at 18:41, Edward Kmett wrote:</div><br><blockquote type="cite">When did universe polymorphism sneak in? <br><br>The lack of it was the reason I stopped using Agda!<br>
<br>-Edward Kmett<br><br><div class="gmail_quote">On Thu, Nov 19, 2009 at 1:33 PM, Luke Palmer <span dir="ltr"><<a href="mailto:lrpalmer@gmail.com" target="_blank">lrpalmer@gmail.com</a>></span> wrote:<br> <blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
I have been diving into Agda recently, and have a decent amount of<br> tuits. I notice that a decent amount of the standard library is not<br> using universe polymorphism. Is there a reason for this, or is it<br> just that nobody has got a round tuit? I'd be happy to start<br>
converting things if the latter.<br> <br> Luke<br> _______________________________________________<br> Agda mailing list<br> <a href="mailto:Agda@lists.chalmers.se" target="_blank">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> _______________________________________________<br>Agda mailing list<br><a href="mailto:Agda@lists.chalmers.se" target="_blank">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></div></div><br><p>
This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.
</p>
</blockquote></div><br>
</blockquote></div><br></body><br/>
<p>
This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.
</p>
</html>