[Agda] Setω and abstraction

[Dan Doel]

On Saturday 26 September 2009 9:51:28 am Nils Anders Danielsson wrote:
> The following code does not type check because "Setω is not a valid
> type":
> 
>   Substitutive : ∀ {a} {A : Set a} → (A → A → Set a) → ?
>   Substitutive {A = A} _∼_ =
>     {p : Level} (P : A → Set p) {x y : A} → x ∼ y → P x → P y
> 
> This definition states that a relation _∼_ (in a certain universe) is
> substitutive if /all/ relevant predicates (in arbitrary universes)
> respect the relation.
> 
> I can see that the type of this definition is problematic; in order to
> type code of the form
> 
>   ∀ {ℓ : Level} → …
> 
> there has to be a "level" which is not an inhabitant of Level. However,
> the body of Substitutive is valid code:
> 
>   postulate
>     subst : {p : Level} (P : A → Set p) {x y : A} → x ∼ y → P x → P y
> 
> This points to a problem: I can write down the type signature of subst,
> but I cannot give the type a name. Are there any thoughts about this?

I've been thinking and reading a bit about this a bit, although that's 
difficult, as there doesn't seem to be a lot of literature on universe 
polymorphism out there. However, from what I can gather, most systems people 
have tried don't allow one to quantify over universes like he can over other 
types.

Coq and LEGO seem to be the main examples, and universe levels are implicit 
there, but even in _Explicit Universes for the Calculus of Constructions_, 
which tries to be more explicit about working with universe levels, there's no 
quantification/Pi involving universes; they (or, constraints on universe 
variables/expressions specifically, I think) simply appear in typing contexts 
(and in judgments about their well-formedness, but in terms, only indexing 
Type).

In fact, _Explicit..._ doesn't handle universe polymorphism, proper, at all, 
if I'm understanding things correctly. Rather, it describes a more modular 
scheme for the old Coq situation of arranging universe variables in an acyclic 
graph. Then the authors expect polymorphism to be achieved by allowing modules 
(which the paper doesn't describe, but are expected to be layered over the 
core type theory) to be parameterized by universe levels, and opened multiple 
times with different levels when necessary.

And this, quite frankly, makes sense to me. It seems like treating universe 
levels as any other type with respect to Pi will easily lead to paradox, since 
those expressions have types, and a type that quantifies over all levels 
probably needs to have a type that is bigger than all levels. Now, you can do 
that, which sounds to me like what Setω is. But then you have to make other 
decisions about what happens from there. For instance, are there levels above 
Setω? Perhaps we have a Setα for every ordinal in ω + ω, but universe 
polymorphism only ranges over those in ω? Does that lead to the same code 
duplication problems?

Another option, it seems to me, would be to have Setω be an actual top to the 
hierarchy, like □ in the lambda cube. □ doesn't have a type, and it doesn't 
have the constructions over it that things below it do. There are no things of 
type □ → □ for instance. And it sounds like that's the situation with Setω 
now, because the type of your original construction would be:

  Substitutive : ∀ {a} {A : Set a} → (A → A → Set a) → Setω

But Setω is not allowed to be used in constructions like that. By contrast, 
subst has a complex type whose type is a bare Setω, but this is no different 
than Fω (or CoC) having arbitrarily fancy kind expressions whose type is a 
bare □.

Another suggestion I've seen is to restrict universe polymorphism to a rank-1 
Hindley-Milner sort of discipline, and is that not good enough for this case?

  Substitutive : ∀ {a p} {A : Set a} → (A → A → Set a) → Set (p + 1)
  Substitutive {a} {p} {A} _∼_
      = (P : A → Set p) {x y : A} → x ∼ y → P x → P y

  subst : ∀{p} → Substitutive {a} {p} {A} _∼_

I guess it means that you'll have to do extra re-quantifying over levels, but 
that may not be such a big deal in practice. I don't have a new-enough copy of 
Agda to test (and don't feel like re-compiling right now), but does avoiding 
higher-rank (perhaps that's not the right term exactly) definitions work all 
right? It seems like it would following the analogy with □ above, and Hindley-
Milner quantification and Setω-as-top might be one and the same.

Anyhow, food for thought.

-- Dan