[Agda] More universe polymorphism

[Dan Doel]

On Fri, Jun 28, 2013 at 5:04 PM, Martin Escardo <m.escardo at cs.bham.ac.uk>wrote:

> Uncomment to get the error "Setω is not a valid type".
>
> That is, the type "{l : Level} (n : ℕ {l}) → Set(newlife n)" is too
> big. But it is the type of the function f, which Agda accepts.
>
> The point I am trying to make is that it doesn't make sense to have a
> type of universe levels. Type levels ought to be meta-liguistic.
>

I don't really think you've demonstrated that.

For one, the Setω handling in Agda is a little funky. It is inferred as a
type for some things, but isn't allowed to occur in other places that would
be expected based on that. I think that's wrong, but it's just a bug. I
wrote a type checker a while back to experiment with Agda-like universe
polymorphism, and it doesn't have this issue (or, wouldn't need to if I
handled definitions more like Agda's; it would involve a special case
somewhere, though). There is just a top type Ω for universe polymorphic
types, and it's relatively normal as a type. You can even take sums over
universes with sigma in my system, which is impossible in Agda, because it
would require specifying that a data definition has type Setω, which is one
of the things that is not allowed. But again, I think that is a _bug_ in
the implementation, not a fundamental property.

Now, what you can't do in my system (as I recall; it's been a while since I
wrote it) is quantify over Ω. Which also means you can't write functions Ω
-> Ω and so on. But this is not out of the ordinary at all in type theory.
The lambda cube is typically formulated with values which have types, types
which have kinds involving * and arrow, and a box, which classifies all the
kinds. But box is the only thing at its level; there are no function spaces
between boxes, or quantification over box things.

So hierarchies with tops that don't have all the properties of the things
below it aren't unusual in type theory. I just think Agda's a bit busted,
and no one has spent the effort to fix it up (because it doesn't bite
often). But, the statement:

> there is an Agda type that doesn't have any Agda type.

is not necessarily cause for alarm (in fact, Martin-Löf type theory as
often presented does not have types for types at all; types are the top
level, and there are only universes, which are types whose values represent
types, but are not types; and original MLTT only had the one universe,
which of course did not have a value representing itself).

I suggest that Agda should move to typical ambiguity, using Harper's
> algorithm. This would both solve this problem and make the Agda users'
> lives easier, and Agda programs much more readable.
>

Does typical ambiguity allow you to do everything that Agda's current
polymorphism does? Is it what Coq uses? I know that in the past people
routinely ran into (erroneous) universe conflicts without getting very far
into formalizing parts of category theory in Coq. So adopting a similar
system might kill one of the largest developments currently in Agda.

I do think it's annoying to have to explicitly specify all the universe
levels of everything in Agda. But I also know there's a fair amount of
literature out there suggesting that having the opportunity (if not the
obligation) to handle universes explicitly is important. Or at least,
completely implicit systems tend to lack generativity necessary for certain
examples.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130628/1097b43f/attachment.html