[Agda] Re: [Coq-Club] Re: Universe Polymorphism

[Dan Doel]

(I'm copying the Agda list with this, since the conversation may be of 
interest there, too.)

On Thursday 16 September 2010 12:34:53 pm Andreas Abel wrote:

> thanks for your answer and the pointer to the EPTS paper.  I had not
> seen it so far, I always refer to a paper by Barras and Bernardo
> published at the same conference (FoSSaCS 2008) with nearly the same
> content!

In that case, one of the author's did an entire thesis on the subject:

  http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.154.5619

Including extending the erasure/irrelevance stuff to inductive types, 
erasability analysis (which may or may not be what you asked for later in your 
mail), and thoughts on proof irrelevance (although, I'm personally not 
convinced that this sort of erasability captures that notion precisely).

> In MiniAgda, I am using EPTSs and I started implementing them for
> Agda, although there are some issues to clarify when you scale up from
> PTSs to a real dependent type theory with types defined by cases.

Yeah. The thesis above presents an analysis of a type theory with strong 
eliminators and erasure. I'm not sure how hard it would be to translate that 
to Agda's pattern-matching-as-primitive theory. Hopefully not very.

> - PTS rules can be used to forbid your embed function, if you put
> Level outside of the Set tower.
> If TLevel is the sort of Level, then just do not add rules like (Set
> i, Level, Level).

Yeah, that's true. The theme of the EPTS papers/thesis, though, is that 
irrelevance/erasability/parametricity should not (necessarily) be intrinsic to 
types; it should be based on use. So, I thought it would be similarly nice if 
one could make universe polymorphism always parametric while not making any 
types intrinsically irrelevant. And I believe my scheme achieves that (it was 
the more fully baked idea).

> Finding out whether something is a universe is not completely trivial
> in Coq or Agda, because of types defined by cases and cumulativity.

Yeah, you're right. Data in higher universes is a problem.

  data T : Set 5 where
    t u : T

  foo : T -> Nat
  foo t = 0
  foo u = 1

T is obviously relevant in foo, but T : Set 5 and Nat : Set 0, 5 > 0. I 
obviously hadn't thought that one through well enough. :)

> Regarding the Set\omega:  It is forbidden in Agda, so some things
> cannot be expressed.  But if we add it to Agda and internally use a
> Set(\omega + 1) to type Set\omega, would there not again things you
> cannot express?
> 
> Of course, there is no reason why the hierarchy should stop at \omega,
> you could go to higher ordinals... :-)  However, maybe we should wait
> with this until practical applications appear that use more than 3
> levels. :-)

There would, of course, be things you can't express. Adding a Set(ω+1) could 
well have the same problems, because the problem isn't a lack of a universe 
above Setω, but an asymmetry with its inhabitants. Currently, we have

  Π i:Level. T[i] : Setω, for T[i] : Set (f i)

but not

  Σ i:Level. T[i]

And thus we can write:

  (i : Level) -> T[i] -> R

but not

  (Σ i:Level. T[i]) -> R

even though it's isomorphic to the former. I don't mind the hierarchy having a 
top as it does, and I think omega is a good place to stop (it's where I 
stopped in my own interpreter). I'm okay with not allowing:

  (S : Setω) -> ...

But, to put inductive types in Setω (which would be okay, with caveats, I 
think), we have to be able to mention it, due to Agda's syntax:

  data T : Setω where ...

The usage there is not quantification over the universe, but akin to:

  ((i : Level) -> Set i) : Setω

Cheers,

-- Dan