Irene Yoon (Mar 17 2022 at 23:43): Irene Yoon (Mar 17 2022 at 23:43):Hi, I was wondering what the difference between the universe(template) flag and the universe(polymorphic) flag was in Coq, and why sigma types use template polymorphism.
In "Type Checking with Universes (1991)" by Harper and Pollack, the authors suggest that strong sums are the motivating reason for introducing cumulative universes, and having a "universe-polymorphic" algorithm would help with the usability of hierarchal universes.
What is the difference between the template polymorphism and universe polymorphism flags in Coq (do either of them correspond more closely to the algorithm presented in the Harper & Pollack paper?), and is there a somewhat simple explanation why sigma types use universe(template)?
Paolo Giarrusso (Mar 18 2022 at 10:27):Not an expert, but on the last point:
and is there a somewhat simple explanation why sigma types use universe(template)?
Coq only had universe(template) for a long time so that's what the stdlib used. Template polymorphism has lots of problems, but universe(polymorphic) is not a drop-in replacement , and IIUC some Coq features/tactics/... do not deal with it correctly yet.
Pierre-Marie Pédrot (Mar 18 2022 at 11:38):I didn't know the Harper-Pollack paper but a cursory glance seems to indicate it deals with elaboration more than actual kernel type-checking.
Pierre-Marie Pédrot (Mar 18 2022 at 11:39):Template poly is a historical attempt at providing universe polymorphism. I like to see it as an "optimization" of univpoly with added quirks.
Pierre-Marie Pédrot (Mar 18 2022 at 11:39):Univpoly is really dumb, it's just that every definition abstracts over the set of universe levels it mentions à la Hindley-Milner.
Pierre-Marie Pédrot (Mar 18 2022 at 11:40):so, effectively it is as if you had a copy of every definition inlined every time you mention it, with a list of universes
Pierre-Marie Pédrot (Mar 18 2022 at 11:40):in univ poly, every global definition (constants, inductive types, etc.) is polymorphic, i.e. it comes with its quantification
Pierre-Marie Pédrot (Mar 18 2022 at 11:41):dually every use comes with the list of variables (the "instance") to fill in these variables
Pierre-Marie Pédrot (Mar 18 2022 at 11:41):template poly is much more intricate and limited
Pierre-Marie Pédrot (Mar 18 2022 at 11:41):only inductive types can be template poly to start with
Pierre-Marie Pédrot (Mar 18 2022 at 11:42):morally, template poly corresponds to the fragment of univ poly where the instances can be rebuilt (so no need to carry them around / abstract over them)
Pierre-Marie Pédrot (Mar 18 2022 at 11:43):universes that can be template poly are the parameters of inductive types which have type Type
Pierre-Marie Pédrot (Mar 18 2022 at 11:44):let's pick an example : Inductive option (A : Type) := None | Some : A -> option A
Pierre-Marie Pédrot (Mar 18 2022 at 11:44):in univpoly mode this would be elaborated to Inductive option@{i} (A : Type@{i}) : Type@{i}) := ...
Pierre-Marie Pédrot (Mar 18 2022 at 11:45):this means that every time you write option A, None or Some there is an implicit @{u} that is added for some universe level u
Pierre-Marie Pédrot (Mar 18 2022 at 11:45):and the type of the result is option@{u} : Type@{u}
Pierre-Marie Pédrot (Mar 18 2022 at 11:46):for the template poly case, there is no such thing
Pierre-Marie Pédrot (Mar 18 2022 at 11:46):but the kernel realizes that A can be a template-poly parameter
Pierre-Marie Pédrot (Mar 18 2022 at 11:47):so, when it sees option A, to decide in which Type@{u} it lives, it infers the type of A and returns that instead
Pierre-Marie Pédrot (Mar 18 2022 at 11:47):no need to carry around an instance
Pierre-Marie Pédrot (Mar 18 2022 at 11:47):there are two added quirks to that
Pierre-Marie Pédrot (Mar 18 2022 at 11:48): Pierre-Marie Pédrot (Mar 18 2022 at 11:48):indeed, when the user writes option without an argument, there is no way to guess in which Type this lives
Pierre-Marie Pédrot (Mar 18 2022 at 11:49):so there is a "default" universe attached to template poly parameters that gets picked when the argument is missing
Pierre-Marie Pédrot (Mar 18 2022 at 11:49):(such a problem does not happen in univ poly because the instance is there, so the type is already decided for you)
Pierre-Marie Pédrot (Mar 18 2022 at 11:50):the "default" universe must obey certain rules to be valid (there are some bounded-below constraints to satisfy to be sound, but I don't want to enter the details too much).
Pierre-Marie Pédrot (Mar 18 2022 at 11:52):this is the root of many spurious universe constraints appearing when using non-fully-eta-expanded template poly inductive types
Pierre-Marie Pédrot (Mar 18 2022 at 11:52): Pierre-Marie Pédrot (Mar 18 2022 at 11:53):A typical example of that is the cartesian product type. If A : Prop and B : Prop then prod A B : Prop in template poly mode, but in univ poly instance levels cannot be Prop for technical reasons.
Irene Yoon (Mar 18 2022 at 15:50):Thanks for the detailed explanation @Pierre-Marie Pédrot ! That helps a bit with my understanding, I recently observed a problem with the non-fully-eta-expanded template poly inductive types, that's helpful to know that it's a common problem
Irene Yoon (Mar 19 2022 at 00:25):Pierre-Marie Pédrot said:
- Template poly needs to handle the case where the inductive / constructor is not applied enough.
Actually, this behavior for template poly is quite concerning to me, considering that inductive types are template poly by default. Why is this deemed OK behavior (is it deemed OK?) / is this a fixable problem by allowing some kind of cumulativity here? (Obviously it's hard to tell without knowing details, I apologize if this suggestion is very naïve..)
Pierre-Marie Pédrot (Mar 19 2022 at 11:10):What do you find concerning exactly? The fact that we can get universe constraints or the metatheory of the feature? In the first case it's not fundamentally worse than monomorphic universes, and in the second, well, that's another story.
Paolo Giarrusso (Mar 19 2022 at 12:32):I don't want to speak for @Irene Yoon (and please push back if I'm doing it anyway), but I reviewed their MR working around another missing eta expansion in Iris (https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/782, tho this link is temporarily down) — which brings up again the usual FAQ:
To add insult to injury, the eta-contracted term is generated by a simple vanilla intuition after Require Import Program.Program....
Pierre-Marie Pédrot (Mar 19 2022 at 12:37):I think the official answer is "backwards compatibility". Ideally, for theoretical reasons I think that template poly inductive types should be guaranteed to be fully applied in the kernel AST. But then this brings in the usual litany of horrible hardwired quotients that we already experienced with primitive projections.
Pierre-Marie Pédrot (Mar 19 2022 at 12:39):(I am actually supportive of having statically fully applied template poly, it would simplify a lot of things in the kernel.)
Pierre-Marie Pédrot (Mar 19 2022 at 12:40):The no-so official answer is that template poly is likely going to be replaced eventually, so maybe not worth putting much effort into it.
Paolo Giarrusso (Mar 19 2022 at 12:40)::cry: :sob: but do you know of some other conceivable solution, maybe along what @Irene Yoon was proposing?
Pierre-Marie Pédrot (Mar 19 2022 at 12:40):You mean, using univpoly + cumulativity? That's the replacement plan.
Pierre-Marie Pédrot (Mar 19 2022 at 12:41):But it's not trivial because now you have to adapt everything to have additional indices elaborated at pretyping.
Pierre-Marie Pédrot (Mar 19 2022 at 12:41):(plus the usual caveats of univpoly, including but not limited to: bugs with tactics, inefficiency, modularity issues when used in a mono context)
Paolo Giarrusso (Mar 19 2022 at 12:42):I've seen bugs with tactics and heard of inefficiency, not sure on the last point.
Paolo Giarrusso (Mar 19 2022 at 12:42):Crystal-ball time: is the ETA for this closer to 6 months or 10 years?
Paolo Giarrusso (Mar 19 2022 at 12:43):some answer seems implicit in "it's not worth improving template poly"
Pierre-Marie Pédrot (Mar 19 2022 at 12:43):honestly, I don't know
Pierre-Marie Pédrot (Mar 19 2022 at 12:44):it's not very hard to elaborate template inductive types to always be fully applied, but I am very wary of the consequences on the already existing code.
Pierre-Marie Pédrot (Mar 19 2022 at 12:44):(also, the stuff I am working on right now is very related to the template poly mess, since it has interactions with SProp and the like.)
Paolo Giarrusso (Mar 19 2022 at 12:45):my guess: some things will break, but they'd break worse if we tried to emulate this purely in .v files, as @Jason Gross proposed.
Paolo Giarrusso (Mar 19 2022 at 12:46):I'll share a link in a minute...
Pierre-Marie Pédrot (Mar 19 2022 at 12:47):I can cook up a patch in a day, if this is really desired, though I'd rather prefer working on the replacement plan.
Paolo Giarrusso (Mar 19 2022 at 12:52):... as long as the replacement plan has no ETA, eta-expansion seems worthwhile. And potentially better than doing it by hand: https://github.com/coq-community/coq-ext-lib/pull/123#discussion_r783638620
Paolo Giarrusso (Mar 19 2022 at 12:54):to be clear, I applaud @Jason Gross for being brave enough to try, but having to do that by hand is clearly wrong.
Pierre-Marie Pédrot (Mar 19 2022 at 12:55):but do you want the higher layers to identify the eta-long form with the short one? This is basically impossible (cf. again primitive projections)
Pierre-Marie Pédrot (Mar 19 2022 at 12:56):I'm just proposing the invariant that any term mentioning a template ind should be fully eta-expanded
Pierre-Marie Pédrot (Mar 19 2022 at 12:56):and the kernel will reject an insufficiently expanded term
Paolo Giarrusso (Mar 19 2022 at 12:57):I'd hope the elaborator can eta-expand the types for you, but nothing more than that.
Paolo Giarrusso (Mar 19 2022 at 12:57):and I'm not even sure the elaborator should, to be honest.
Paolo Giarrusso (Mar 19 2022 at 12:59):so indeed, any code traversal that expects the eta-contracted form will break and will have to be fixed, and this might turn out to be unworkable.
Paolo Giarrusso (Mar 19 2022 at 13:00):my hope is that (if elaboration can automatically eta-expand) most code will just keep working and only some ltac matches will break.
Pierre-Marie Pédrot (Mar 19 2022 at 13:00):That's also what I hope for.
Paolo Giarrusso (Mar 19 2022 at 13:02):additionally, unlike primitive projections, it _might_ be possible to normalize _some_ patterns, and it might even be useful: here we have a single legal form, not 3 different forms on an equal status.
Pierre-Marie Pédrot (Mar 19 2022 at 13:02):That, I don't buy. For primitive projections we also have a canonical form.
Paolo Giarrusso (Mar 19 2022 at 13:03):but the other forms are well-typed [in prim. projections], unlike here.
Pierre-Marie Pédrot (Mar 19 2022 at 13:05):Right.
Paolo Giarrusso (Mar 19 2022 at 13:06):so if I write the pattern F option and that pattern gets elaborated enough, you know it's safe to eta-expand it. But in other cases, you can't — that's why I don't know if this is helpful.
Paolo Giarrusso (Mar 19 2022 at 13:08):so this isn't trivial, but if you spent that day on the core patch, we could see if the porting is easy.
Paolo Giarrusso (Mar 19 2022 at 13:17):of course, this only makes sense if the full replacement adds worse breakage. From here, it looks as far away as the famed unifall :-|, but of course I know nothing. Good luck!
Last updated: Oct 13 2024 at 01:02 UTC