[Agda] Universe polymorphism in the standard library

[Thorsten Altenkirch]

> 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. ;)

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.

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.

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:
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AIMX
Maybe he has written more about this?

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.

Cheers,
Thorsten



> -Edward Kmett
>
> On Thu, Nov 19, 2009 at 3:09 PM, Thorsten Altenkirch <txa at cs.nott.ac.uk 
> > wrote:
> Hi,
>
> 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.
>
> As a stop gap I am using
> {-# OPTIONS --type-in-type #-}
>
> It is usually easy to see wether your definitions can be stratified.
>
> Cheers,
> Thorsten
>
> On 19 Nov 2009, at 18:41, Edward Kmett wrote:
>
>> When did universe polymorphism sneak in?
>>
>> The lack of it was the reason I stopped using Agda!
>>
>> -Edward Kmett
>>
>> On Thu, Nov 19, 2009 at 1:33 PM, Luke Palmer <lrpalmer at gmail.com>  
>> wrote:
>> I have been diving into Agda recently, and have a decent amount of
>> tuits.  I notice that a decent amount of the standard library is not
>> using universe polymorphism.  Is there a reason for this, or is it
>> just that nobody has got a round tuit?  I'd be happy to start
>> converting things if the latter.
>>
>> Luke
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>
>
> 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.
>
>


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.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20091120/512695f7/attachment.html