Stream: Coq users

Topic: contravariance on universe level

Lapinot (Aug 05 2023 at 15:17):

Hi! Is there a reason why there is no "contravariant" variance specifier for universe cumulativity? I'm doing a proof-of-concept predicative church encoding as `Definition nat_r@{i j | j < i} : Type@{i} := forall X : Type@{j}, X -> (X -> X) -> X .` and it would be useful to me to declare `j` contravariant.. In fact i can declare just fine the coercion myself by eta-expansion:

``````Definition lower_r@{i0 i1 j0 j1 | j0 < i0 , j1 < i1 , j1 <= j0}
: nat_r@{i0 j0} -> nat_r@{i1 j1} := fun n X => n X .
``````

Also i'm not so sure how to properly use explicit universe polymorphism: from my little experience i have had some trouble with using the successor (level `i+1`) as in `Definition nat_r@{i} : Type@{i+1} := forall X : Type@{i}, X -> (X -> X) -> X `, but this definition has the advantage of having one less level parameter (which makes subsequent definitions less clutered with tons of parameters and inequalities). Is using `i+1` discouraged or should i stick with it? (i don't remember precisely but i think in some places like constraints i couldn't write such expressions)

Paolo Giarrusso (Aug 05 2023 at 15:29):

IIRC/IIUC: `i+1` is an algebraic universe, and I'm no expert but it's been discussed that Coq does not support them well because they increase the asymptotic complexity of type inference/elaboration.
https://coq.zulipchat.com/#narrow/search/algebraic.20universe finds multiple discussions, like

Lapinot (Aug 05 2023 at 15:33):

Thanks, I didn't know they were part of a different feature! I'll checkout the links!

Jason Gross (Aug 06 2023 at 01:54):

I think Coq supports contravariance but only for inductive types (see the `Polymorphic Inductive Cumulativity` flag). I don't know why it's not also supported for constants (though as you note it adds no expressivity power, only performance and convenience (and ease of use of tactics, probably), since it can always be accomplished by delta-expanding the constants, eta-expanding the functions, and making use of inductive cumulativity.)

Gaëtan Gilbert (Aug 06 2023 at 07:06):

there is no contravariance in Coq, only eta expansion

Gaëtan Gilbert (Aug 06 2023 at 07:06):

Last updated: Jun 22 2024 at 16:02 UTC