The Coq mailing list

[Dan Doel <dan.doel AT gmail.com>]

On Tuesday 14 September 2010 8:56:30 am Andreas Abel wrote:

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

Ah. I guess this solves the gotchas I'd thought of in this regard. I knew 
that 
people weren't happy with Agda's having non-parametric quantification over 
levels for use in Sets. However, I had thought that even without case 
analysis, you could do the following:

  embed : Nat -> Level
  embed zero    = zero
  embed (suc n) = suc (embed n)

  f : (n : Nat) -> ... embed n ...
  ...

and regain non-parametric quantification (by analysis on Nat), even without 
eliminators for Level. But, if Level is always irrelevent, embed is not a 
valid function (if this is anything like erasure pure type systems *).

My own thoughts on the issue were a bit wackier. I've been interested in 
EPTSes for a while, and came up with a way (I think), to extend them to 
provide some solutions. The EPTSes in the linked paper are presented as 
having 
function space rules like ordinary pure type systems. But, what if we allowed 
them to know whether irrelevant or relevant quantification is being 
performed, 
too (and for universe polymorphism, tell it what variable is being bound)? 
Then rules are of the form (sticking to functional relations):

 (var, phase, sort, sort) -> sort

(that may not be an ideal presentation of the rules, but it should suffice) 
The ordinary part of the hierarchy would go:

  (v, _, Set i, Set j) -> Set (lub i j) if v is not free in j

And for universe polymorphism, we can add:

  (v, c, Set i, Set j) -> Setω if v is free in j

The important part being that this only allows computationally irrelevant 
function spaces to be used for universe polymorphism. This means that embed 
is 
now valid:

  embed : Nat -> Level
  Nat : Set 0, Level : Set 0

  rule (_, r, Set 0, Set 0) = Set 0

But, when we go to try and use it to enable non-parametric universe 
dependence, we fail:

  f : (n : Nat) -> ... T : Set (embed n) ...
  f zero    = ...
  f (suc n) = ...

  Nat : Set 0, T : Set (embed n)
  rule (n, r, Set 0, Set (embed n)) = error

So, appropriate behavior is not ensured by making Level itself inherently 
irrelevant, but by ensuring that only irrelevant things (regardless of type) 
are used in universe polymorphism. For instance, we could instead write 
(using, I think, similar notation to the irrelevance stuff you've proposed 
for 
Agda):

  g : .(n : Nat) -> ... T : Set (embed n) ...
  g n {- no case analysis -} = ...

(I also have another idea of where the above style rules could be useful. **)

> 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 know. Although, I think it could be useful (and non-problematic) to allow 
talking about it. I have my own simple interpreter for fooling with Agda-like 
universe stuff (without the irrelevance stuff I mentioned above; I haven't 
gotten around to implementing something with all that yet), and it allows 
sigma types like:

  (Σ i : Level. Σ T : Set i. T) : Ω

(incidentally, I also think a type not of the form SetN is kind of 
appropriate 
as a top, because Setω kind of makes ω look like a Level.) But you cannot 
construct a similar type in Agda:

  data All : Setω where
    con : (i : Level) -> (T : Set i) -> T -> All

because that "Setω" is an error. Yet for any All -> T, the corresponding 
curried function is allowed.

> I think we have a systematic and fairly simple solution to the problem
> of universe polymorphism.

I do like it. Making universe levels (roughly) ordinary, first-class values 
seems simpler and more natural than a lot of other proposals I've seen. But I 
can understand people being a weirded out by, essentially, Set being a family 
that contains its own index/parameter type.

-- Dan

[*] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.156.2558

[**] One redundancy of EPTSes is that quantification on Sets is probably 
naturally parametric when doing (x : Set i) -> (T : Set j) i > j stuff. It is 
in Agda, I believe. You could solve this redundancy by adding type case as a 
language primitive. Then parametric quantification would ensure that type 
case 
isn't used, and types could be erased.

But, you could also use the above rules to disallow using the ordinary 
function space where it's necessarily parametric, like so (ignoring variables 
for now):

  (_, Set i, Set j) -> Set j if i <= j
  (c, Set i, Set j) -> Set i if i >  j

And now we can no longer write:

  id : (A : Set) -> A -> A

only:

  id : .(A : Set) -> A -> A

Forcing us to tag all the Sets that can be erased. I'm not actually certain 
this is useful, since it imposes an additional burden on the programmer to 
provide information the compiler could figure out, but it might be 
interesting 
in an intermediate language.