It seems to me that there are no real reasons to not like cumulativity (the example given here seems to not be too relevant, according to the comments), and yet most proof assistants (apart from Coq?) don't have cumulativity. Why is this so? This seems a very nice property mathematically, and is akin to how most people would think of universes intuitively.
$\begingroup$
$\endgroup$
6
2 Answers
$\begingroup$
$\endgroup$
15
The short answer is that cummulativity is just one possible design choice which does not fit all purposes.
The slightly longer answer is that baking commulativity into type theory is a very dramatic design choice that complicates the typing rules, equality and conversion, universe management, and the semantics.
The real question is not whether we should have cummulativity but rather how to organize universes so that the user can control them when they wish or must do so, and at the same time the proof assistant can handle them by itself in a reasonable way. It is not clear (to me) that cummulativity is the best way to approach the problem. There are other options, such as implicit coercions, explicit coercions (also known as "lifting"), univere polymorphism, etc.
There is also a wider issue, namely that from a foundational point of view there seems little reason to fix a specific hierachy of universes (such as a linearly ordered sequence of universes indexed by natural numbers). You may call me a logician but I really dislike arbitrary choices in foundations of mathematics.
-
$\begingroup$ To be fair, the reason that this is bothering me currently is that in Lean, explicit tyles like
nat/ratare inType, as opposed toType u. So making things more polymorphic would fix this sort of issue. What sort of complications does it cause on the typing rules? Is this the sort of thing that's mentioned on the linked question? $\endgroup$ Feb 20, 2022 at 14:22 -
$\begingroup$ I found out from Mario Carneiro on the Lean Zulip that "complication" further implies that it's actually still an open problem whether Coq's type theory is consistent (and similarly for a cumulative Lean). The extent of this complication wasn't clear to me $\endgroup$ Feb 21, 2022 at 23:04
-
1$\begingroup$ @It'sNotALie.: Thank you. All I see there is an unsubstantiated claim in quotes. Perhaps there are some Coq developers lurking here who can comment on this business of "consistency [of Coq] is widely believed but an open question". At least a very large chunk of Coq obviously has a set-theoretic model, including cummulative universes. It ought to be at least as consistent as ZFC + countably many inaccessible cardinals. $\endgroup$ Mar 2, 2022 at 12:19
-
1$\begingroup$ @JamesMartin: Universes are by no means necessary in a proof assistant. They are rather one possible solution that gets implemented over and over, and which seems to cover most needs. All I am saying is that baking in a solution just because the previous proof assistant baked in the solution is not necessarily the way of progress. Of course, we learn a great deal with every generation of proof assistants, and we should reuse good solutions. But we should also be on the lookout for implicit assumptions about the design. I feel that sometimes universes are taken for granted. $\endgroup$ Mar 2, 2022 at 12:21
-
2$\begingroup$ @AndrejBauer I'll open up a question, I guess asking about the general status of consistency of the metatheory of proof assistants in general. $\endgroup$ Mar 2, 2022 at 12:43
$\begingroup$
$\endgroup$
The biggest problem in my head is that cumulativity opens the door of subtyping in type theory, which, IMO, a potential calamity to type theory. If you elaborate cumulativity to non-cumulativity + lifting, then it's probably fine, but let me say something about the subtyping-based approach.
Once you have subtyping, you'll start thinking about covariance and contravariance, which brings a lot more things to the type theory. Also, subtyping itself distinguishes two notions: consider $(a:A)\in\Gamma$, then "the type of $a$" and "$A$" are no longer the same under the context $\Gamma$. Instead, "the type of $a$" is a subtype of $A$, and when you want to, for example, apply $a$ to the identity function with the type argument an implicit argument, then probably you can't solve the metavariable because $A$ won't be the most accurate solution (I thank Pavel for sharing some ideas with me about this).
Apart from that, cumulativity generates more complex universe level equations, which are harder to solve.
intandreallive inType := Type 0, the bottom universe. If I want to copy them over to another universe I have touliftthem and right now there's a bunch of API which is missing on the lifted copies (e.g. the order structure), although some API does lift (e.g. the ring structure). Of course this is just missing API... $\endgroup$intto be polymorphic, with a specified copy in every universe. $\endgroup$