[TYPES] Universe Polymorphism

[Thorsten Altenkirch]

Hi Stefan,

> Thorsten,
>
>> It seems to me that Type:Type is an honest form of impredicativity,
>> because at least you know that the system is inconsistent as a logic
>> (as opposed to System F where so far nobody has been able to show
>> this :-). Type:Type includes System F and the calculus of
>> constructions and I think all *reasonable* programs can be reformed
>> into Type(i):Type(i+1) possibly parametric in i. However, sometimes
>> you don't want to think about the levels initially and sort this out
>> later - i.e. use Type:Type. A similar attitude makes sense in
>> Mathematics, in particular Category Theory, where it is convenient to
>> worry about size conditions later...
>
> From a programmer's perspective: what can be said about the  
> inferrability of universe polymorphism? I mean: it would be great if  
> the programmer could just proceed as if Type:Type and have the  
> compiler infer the correct indices, universe abstractions, and  
> universe applications.

Maybe a good starting point would be to answer the question what is  
the language of explicit universe polymorphism. Such a language should  
include at least abstraction and quantification over universe levels.  
Should the embedding from one universe into the next be implicit or  
explicit, i.e. do we want to have the rule A : Type(i) => A : Type(i+1)?

While many trivial uses of universe levels may be inferable, I suspect  
that there may be situations where you want to have a "manual  
override". However, as far as  know to find a good way to integrate  
explicit and implicit universe polymorphism is an open issue. Maybe  
somebody else can comment on this.

Btw, in the context of Type Theory much larger universes have been  
investigated, e.g. Palmgren introduced "superuniverses" and Setzer the  
"Mahlo universe". These constructions may also have interesting  
applications in programming with dependent types.

Cheers,
Thorsten


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.