I recently heard about universe polymorphism. From the look of it, it seems to solve a few of the problems I’ve been having. However, before using it, I want to be sure that I won’t run into any unforeseen issues. My main question is this: does universe polymorphism extend the underlying theory of Coq itself, or is it all just a notational trick that re-defines objects in different universes implicitly? I use a few axioms in my setup and I want to ensure that there won’t be any inconsistency if I decide to use universe polymorphism.
2 Likes
The short answer is: no, you are completely fine. For instance, the MetaCoq project that aims at formalizing the metatheory of “real” Coq handles those without any issue.
The long answer is: universe polymorphism is at least as much an engineering trick as a “theoretical” feature of the type theory.
On paper, one usually considers a hierarchy of universes indexed by integer levels. However to be able to perform typical ambiguity (i.e. not give the level of every Type that appears in your terms), Coq instead uses level variables (one is basically introduced for each use of Type), and graph reasoning to be sure that there are no invalid constraints, so that the levels could be in principle projected down to the integers – but this is never done in practice.
Now whenever you have a new declaration (be it a definition or a new inductive type), Coq generates fresh levels and checks that their constraints are valid. But there are then two ways to see those levels: either you see them as global ones, and so the declaration also adds a bunch of level variables that are fixed once and for all – this is the default behaviour, and is called monomorphic in that context; or you see those as local to the declaration, so that the declaration is universe polymorphic in the same way that e.g. functions in OCaml can be polymorphic with respect to their type variables.
In the polymorphic case, every use of the declaration generates new level variables, which more or less amounts to having one new monomorphic declaration each time you use the polymorphic one. So is mostly a practical way to avoid having to redo the same declaration multiple times to be able to use it at different levels. While this could in theory be simulated by copying the same monomorphic declaration multiple times, this would of course be very unpractical in an actual proof assistant.
Note that this is the story for what is referred to in the manual as Polymorphic Universes, but there is also another older mechanism called Template Polymorphism, which is somewhat different – but I guess this is not what you were talking about
1 Like
My experience with it isn’t great - I found once that I had to use it to
avoid some error to do with universes. But finding out which
definitions (etc) to make Polymorphic was a matter of trial and error.
And some places adding Polymorphic made the code not work where it would
work without the Polymorphic declaration. So it required a long time of
trial and error
Jeremy
But finding out which
definitions (etc) to make Polymorphic was a matter of trial and error.
Did you use automatic generalization over universes or explicit generalization over names given by the user?
sorry I don’t understand the question.
It was quite a long time ago,
I don’t remember all about it. But I did at various times try putting
Set Universe Polymorphism in some files, and
alternatively putting Polymorphic in front of particular definitions.
Maybe that answers your question.
I put a message on the mailing list early last year, as follows:
Re: [Coq-Club] universe inconsistency – Mon, 13 Jan 2020 14:27:55 +0100
(CET)
Fortunately the problem hasn’t recurred, so I haven’t had to try to
understand why it happened
Jeremy
Sorry, I was too elliptic. I meant
Set Universe Polymorphism.
Definition foo@{i j} := Type@{i} -> Type@{j}.
Set Printing Universes. Set Printing All. Print foo.
(*
foo@{i j} =
forall _ : Type@{i}, Type@{j}
: Type@{max(i+1,j+1)}
(* i j |= *)
*)
where you control the order and occurrences of the universe variables, versus
Set Universe Polymorphism.
Definition foo := Type -> Type.
Set Printing Universes. Set Printing All. Print foo.
(*
foo@{Top.1 Top.2} =
forall _ : Type@{Top.1}, Type@{Top.2}
: Type@{max(Top.1+1,Top.2+1)}
(* Top.1 Top.2 |= *)
where you don’t.