Stream: Coq users

Topic: contravariance on universe level


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

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

https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Universe.20polymorphic.20definition.20with.20unbound.20levels/near/261525227 or https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/.60False.20.3A.20Prop.60.20vs.20.60Empty_set.20.3A.20Set.60/near/282235398.

view this post on Zulip Lapinot (Aug 05 2023 at 15:33):

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

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

view this post on Zulip Gaëtan Gilbert (Aug 06 2023 at 07:06):

there is no contravariance in Coq, only eta expansion

view this post on Zulip Gaëtan Gilbert (Aug 06 2023 at 07:06):

see also https://github.com/coq/ceps/pull/47


Last updated: Jun 22 2024 at 16:02 UTC