[TYPES] Universe Polymorphism

[Thorsten Altenkirch]

Hi Klaus,

> What are the practical implications of having "type:type"? I read  
> that it destroys the consistency of the
> type system as a logic, but this is not relevant for my purposes. On  
> one hand, I have read
> that type-checking in systems with "type:type" is not decidable, but  
> on the other hand, the paper
> "Why dependent types matter" mentions in Sec. 7 that the authors  
> have adopted "type:type" in their
> Epigram language. How does this fit together? Are there any useful  
> examples in Epigram (or any other language) that
> use the "type:type" possibility?

To add to this: recently, I asked for Type:Type (or rather Set:Set) to  
be added to Agda because since Agda currently doesn't support any sort  
of universe polymorphism you frequently had to duplicate code. Thanks  
to Ulf and Nisse this was implemented very quickly - now you only have  
to set a flag to indicate that you are "lying".

One particular example was that the Agda library has a function [_,_]  
for copairing, i.e. if f : A -> C and g : B -> C then [f,g] : A+B -> C  
and I wanted to use this on dependent types, i.e. I had f: A -> Set  
and g : B -> Set and wanted to construct [f.g]: A+B -> Set. Agda  
complained that Set:Set1 but the function [_,_] required C:Set.

This sort of example is covered by currently implemented forms of  
universe polymorphism (e.g. in Coq) but when you start programming  
with types more seriously you easily run into examples which are  
beyond the state of the art, e.g. you may want that the function
\  F:Type -> Type. F o F has the Type
(Pi i.Type (i) -> Type(i+1)) -> Type (j) -> Type (j+2).

Indeed, I think, this was the reason for  Conor to avoid this issue  
altogether when implementing Epigram and use Type:Type as a stop-gap  
until a reasonable form of universe polymorphism is implemented.

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

Btw, Andreas Abel and I have recently written a paper which uses  
Type:Type as an example of a partial type theory. We show that our  
type checker is sound and "partially complete", it will only fail to  
accept a welltyped term because there are diverging terms in the type  
derivation (http://www.cs.nott.ac.uk/~txa/publ/msfp08.pdf). This is  
only for beta, while there is an algorithm to typecheck Type:Type with  
beta-eta, I think even soundness is open for this case.

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.