While taking a look at the Coq’s (or CIC’s) subtyping rules, I noticed that for pi type, the rule does not allow contravariant subtyping for the argument.
Is there a reason to not have this? (Like causing inconsistency or so)
Meven Lennon-Bertrand on coq-club yesterday said on this topic (https://sympa.inria.fr/sympa/arc/coq-club/2024-06/msg00025.html, may need to be opened in a private window as that site is buggy):
As far as I understand, the main reason comes from the set-theoretic semantics. In that setting, subtyping is interpreted as set inclusion. This makes it relatively easy to interpret implicit subtyping like Coq’s, because the same term can be used as the subtype and supertype. But this also heavily restricts what is a valid subtyping rule.
In particular, for function types (which are sets of pairs in set theory), (covariant) inclusion of the codomains leads to inclusion of the sets of functions, but (contravariant) inclusion of domains does not. This is because one has to remove some pairs (corresponding to the elements of the larger domain that do not exist in the smaller domain).
Thus, if one wants to model contravariant subtyping in set-theory, we would need something smarter than this model, which has not really been investigated (yet?). But I do not see any reason why such a subtyping would not be sensible. In particular, Coq does a “poor man’s” version of it, by η-expanding function during elaboration to basically emulate the contravariant rule (because if A <: A’ and f : A’ → B, even though f : A → B does not hold, λ x : A. f x : A → B does). I believe this could be promoted to a sensible version of contravariant subtyping.
We have a paper Definitional Functoriality for Dependent (Sub)Types | SpringerLink going in that direction at this year’s ESOP by the way, although it’s not quite ripe to apply to Coq’s type system yet I hope we can build on it to get there at some point, and properly justify contravariance for function types
1 Like
Oh shoot my coworker asked it in a different channel haha. Thanks for the link to that answer.