The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

On Sep 13, 2010, at 5:47 PM, Dan Doel wrote:
>  data T {i : Level} : Set (suc i) where
>    t : Set i -> T
>
>  u : forall {i} -> T {suc i}
>  u = t T
>
> I'm not sure how the Aczel set theory thing would work out. I  
> suspect it would
> fail earlier, or you'd only be able to prove that R i \in R (suc i)  
> (depending
> on how R was defined).
>
> Level is almost an ordinary type---there's a little compiler support  
> for
> normalizing expressions like 'lub x x' to 'x' even for open terms; I  
> think
> this is in part due to Agda totaly lacking cumulativity, so lubs of  
> multiple
> levels variables need to be used instead of implicitly lifting  
> everything
> involved to a single level.

During the Agda meeting which finished a week ago we started to add  
cumulativity which makes things much more smooth in practice.   
Explicit lubs won't be needed anymore.  Also level won't be an  
ordinary type anymore, it will be a version of the natural numbers you  
cannot compute on.  This ensures that levels remain irrelevant for  
computation, they are only there to sort out the universe  
stratification.  This is in analogy to sizes in the type-based  
termination approach: sizes are only there to sort out the  
termination, they are computationally irrelevant.

As of now, you can play with explicit universe polymorphism and  
cumulativity in MiniAgda (see my homepage).  There your example looks  
like:

data T (i : Size) : Set $i
{ inn : (out : Set i) -> T i
}

fun U : (i : Size) -> T $i
{ U i = inn $i (T i)
}

MiniAgda-bug reports welcome!

> Also, I believe the rule for universe polymorphic
> functions is adequately described by:
>
>  if U[x] : Set S, where x is free in S
>  then ((x : T) -> U[x]) : Setω
>
> Where ω is not itself a Level (and thus Setω is not itself of the  
> form Set i
> for some i : Level, which would probably be paradoxical).
>
> This stuff isn't remotely well-established theoretically as far as I  
> know,
> though. At least, it's novel with respect to all the published  
> papers I've
> seen on universe polymorphism. So I could understand people being  
> reluctant to
> put it in Coq at this point.


I think with making levels non-computational it is not as scary any  
more.  Of course the rule for universe-polymorphic function types  
above is still needed.  However, it does not have to be a special  
rule. If you want to type check

  (x : Level) -> U[x] : ?

then ? cannot mention x, but continuing

  x : Level |- U[x] : ?

you need an upper bound for all the sorts (Set S[x]) and that can only  
be Setω.  Note that Setω is not part of the Agda syntax, it is used  
only internally, and plays the role of "Type" in the Martin-L"of  
logical framework.

I think we have a systematic and fairly simple solution to the problem  
of universe polymorphism.  It can be described as a PTS with  
cumulativity and subtyping in a straightforward manner.  There is a  
cost in type checking due to an additional level argument in all  
universe-polymorphic definitions, but I hope to keep it low by adding  
Miquel/Barras/Bernardo-style irrelevance for level-polymorphic things.

--Andreas


Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/