Stream: Coq users

Topic: Universes and sigma types


view this post on Zulip 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)?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Mar 18 2022 at 11:41):

template poly is much more intricate and limited

view this post on Zulip Pierre-Marie Pédrot (Mar 18 2022 at 11:41):

only inductive types can be template poly to start with

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Mar 18 2022 at 11:44):

let's pick an example : Inductive option (A : Type) := None | Some : A -> option A

view this post on Zulip 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}) := ...

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Mar 18 2022 at 11:45):

and the type of the result is option@{u} : Type@{u}

view this post on Zulip Pierre-Marie Pédrot (Mar 18 2022 at 11:46):

for the template poly case, there is no such thing

view this post on Zulip Pierre-Marie Pédrot (Mar 18 2022 at 11:46):

but the kernel realizes that A can be a template-poly parameter

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Mar 18 2022 at 11:47):

no need to carry around an instance

view this post on Zulip Pierre-Marie Pédrot (Mar 18 2022 at 11:47):

there are two added quirks to that

view this post on Zulip Pierre-Marie Pédrot (Mar 18 2022 at 11:48):

  1. Template poly needs to handle the case where the inductive / constructor is not applied enough.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Mar 18 2022 at 11:52):

  1. Template poly is slightly more expressive than univ poly, because it allows Prop levels

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Irene Yoon (Mar 19 2022 at 00:25):

Pierre-Marie Pédrot said:

  1. 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..)

view this post on Zulip 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.

view this post on Zulip 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....

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Mar 19 2022 at 12:40):

You mean, using univpoly + cumulativity? That's the replacement plan.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Paolo Giarrusso (Mar 19 2022 at 12:42):

I've seen bugs with tactics and heard of inefficiency, not sure on the last point.

view this post on Zulip Paolo Giarrusso (Mar 19 2022 at 12:42):

Crystal-ball time: is the ETA for this closer to 6 months or 10 years?

view this post on Zulip Paolo Giarrusso (Mar 19 2022 at 12:43):

some answer seems implicit in "it's not worth improving template poly"

view this post on Zulip Pierre-Marie Pédrot (Mar 19 2022 at 12:43):

honestly, I don't know

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Mar 19 2022 at 12:46):

I'll share a link in a minute...

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Mar 19 2022 at 12:56):

and the kernel will reject an insufficiently expanded term

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Mar 19 2022 at 12:57):

and I'm not even sure the elaborator should, to be honest.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Mar 19 2022 at 13:00):

That's also what I hope for.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Mar 19 2022 at 13:02):

That, I don't buy. For primitive projections we also have a canonical form.

view this post on Zulip Paolo Giarrusso (Mar 19 2022 at 13:03):

but the other forms are well-typed [in prim. projections], unlike here.

view this post on Zulip Pierre-Marie Pédrot (Mar 19 2022 at 13:05):

Right.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Jan 31 2023 at 14:03 UTC