[Agda] How does level polymorphism fit into a valid type theory?
(from "More universe polymorphism")
Martin Escardo
m.escardo at cs.bham.ac.uk
Mon Jul 1 23:03:34 CEST 2013
On 01/07/13 20:16, Guillaume Brunerie wrote:
> Well, if you want to define a polymorphic function (polymorphic on all
> small types, not restricted to some universe), you have to quantify
> over all levels.
> Or you can use typical ambiguity,
I don't think this should be an "either or" situation. One should have
an explicit understanding of what universes and levels are, and typical
ambiguity should be a shorthand for making types and terms readable
(very much like implicit-argument notation) by erasing levels that can
be automatically inferred.
> but this is kind of cheating.
It doesn't need to be.
> Maybe you could instead have a notion of universal quantification over
> all universes which would be a primitive notion, distinct from the
> usual Pi types.
It is sort of what you are doing, except that you quantify over indices.
I find it slightly disturbing that the indices come with unspecified
operations that "we know what they are" but we don't actually specify in
the language.
> Various people were talking about that at the IAS this
> year but I don’t know if anyone tried to write down the rules.
Wouldn't they be very much like what you wrote for universe indices?
Also, for cumulativity you probably need more than what you wrote:
Somehow you have to express that U_{sup f} is the union of U_{f i} in
your rules, don't you? Also, different zero-succ-sup expressions could
give different indices for the same universe (very unlikely in a
definitional way), and you can't talk about this in the type system you
propose, at least not at the moment as it is presented (does it matter?).
> But if having a type of universe levels is consistent and natural and
> pretty, I don’t see why we should try to avoid it.
Perhaps. But, for example, if giving computational meaning to function
extensionality, univalence, and higher-order inductive types is already
difficult, it is going to be no easier with first-class-citizen,
transfinite universe indices.
Moreover, I think it is nice to structure type theory in increasing
levels of generality. For example, the theory can be defined without any
universe. Then one can add one universe, then countably many universes,
where the indices are meta-linguistic (this is the way I read the brief
discussion about sequences of universes by Martin-Loef). If you
incorporate the indices as a type, I would prefer to be able to see the
previous system as naturally incorporated there. If you have a type of
levels, you will have to explain how the meta-language natural-number
indices live inside the object-language type of levels, to begin with.
So I am not sure (at least not yet) whether this is really "natural". We
can decide whether it is pretty when we see all the details written down.
Is there an algorithm for typical ambiguity for the transfinite
generalization of levels? Does it matter? Does this even make sense?
Best,
Martin
More information about the Agda
mailing list