The Coq mailing list

[Lauri Alanko <la AT iki.fi>]

On Wed, Apr 18, 2007 at 07:48:14PM +0300, Lauri Alanko wrote:
> However, it means that if we want to prove theorems
> universe-polymorphically, we can never ever use the names ENS or ENS2,
> as those are fixed to a particular universe. Instead, we have to say
> "forall (A : Type) (e : ens A), ..." everywhere, which is a bother...
> 
> Hm, wait a second, isn't { A : Type & ens A } polymorphic, too? So
> perhaps the best thing would be to use a _syntactic_ definition that
> expands to the above. I must try that out and see how it fares.

All right, I did a bit of experimenting. It turns out that yes, one
can get workable universe polymorphism in definitions and theorems if
one always factors the (A : Type) into an explicit parameter instead
of packing it in an existential or other structure. Then to get
instances of a structure for different universes, one just has to
duplicate the packing and unpacking.

This is in itself still bearable. The explicit parameters are a
bother, but not too bad, thanks to the sectioning mechanism.

However, there's a killer. If I use the usual mechanism of packing a
carrier type into a structure, I get e.g.:

C : Category
A : Ob C
B : Ob C

Now I can write just A --> B, expanding to (Hom _ A B), since the
actual category C can be inferred from the type of A and B.

However, with the carrier type factored out, I get:

T : Type
C : Category_On T
A : T
B : T

Now, since the type of C depends on the type of A, instead of vice
versa, the category can no longer be inferred in (Hom _ A B), so the
category has to be explicitly given. Though some shorthands could no
doubt be devised, I think the repercussions on code clarity and
verbosity would still be enormous.

So it still seems there's call for removing the "monomorphism
restriction" from the current sort polymorphism. Admittedly the
default invisibility of universes can cause seemingly unintuitive
things, but that is already happening now. And one can always Set
Printing Universes to see what's really going on. (Although the syntax
of that, as well as Print Universes, could perhaps be improved.)


Lauri