[Agda] Setω and abstraction

[Dan Doel]

On Wednesday 30 September 2009 6:00:50 am Nils Anders Danielsson wrote:
> On 2009-09-30 01:09, Dan Doel wrote:
> > 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 prefer systems where, everything else being equal, I can abstract over
> as much as possible. I guess everything else may not be equal in this
> case, though.

Incidentally, it occurred to me as I was falling asleep that of course Setω as 
the top of the hierarchy isn't the same as only quantifying HM style, because 
you can have arbitrary rank quantifications just like in System F/Calculus of 
Constructions. What's actually ruled out are the analogues of:

  \(A : *) (x : A) -> (B : *) -> B -> B

which, in my CoC evaluator complains that you can't take the sort of □. So you 
can't return a type that quantifies over */Setω from a function (and of 
course, you can't quantify over □ in arguments to make kind-polymorphic 
functions), which is what you ran into. But, you can still do stuff like:

  \(A : *) (f : (B : *) -> B -> B) (x : A) -> f A x
  : ∀A -> (∀B -> B -> B) -> A -> A

At least in the calculus of constructions (I haven't recompiled to test Agda 
yet). So this might be a more permissive (than HM) middle ground, assuming it 
doesn't cause problems somewhere.

I've been thinking about trying to add a system with universe polymorphism to 
my PTS evaluator so I can play around with various choices, but I don't think 
it's 'just another set of axioms,' so I don't know how far I'll get.

Cheers,

-- Dan