The Coq mailing list

[nicolas tabareau <nicolas.tabareau AT inria.fr>]

Hi Jason,

There is a notion of cumulativity over context in Coq and actually we have formalized 

it and proven the metatheory of it in the MetaCoq project. 

Properties of context cumulativity are actually admissible in Coq, see for instance: 

https://github.com/MetaCoq/metacoq/blob/67097a400c5889c03fd1f3f232b75d5391031a25/pcuic/theories/Typing/PCUICContextConversionTyp.v#L313

So the question of naturality you are mentioning is actually proven to hold. 

However, because of a lack of model justifying it (as Meven was explaining), we have not yet promoted 

context cumultiivitry into (contravariant) cumulativity over Pi types in the theory, but maybe we should investigate 

it more if there is a real user demand.

Best, 

— Nicolas

On 21 Jun 2024, at 23:31, Jason Hu <fdhzs2010 AT hotmail.com> wrote:

Thank you Xavier for your example and Meven for your careful explanations.

I am working on a mechanization of MLTT and I notice that cumulativity and subtyping essentially should go hand in hand. The problem with no contravariant subtyping which I noticed is that it makes the type theory "un-natural". That is, say we know t : T and T <: U. Now let's substitute t for x : U. Currently the ONLY way in Coq is to do subtyping first to obtain t : U, and then apply the substitution t/x. However, another way to do it is to apply the subtyping to the target context first. Namely, we strengthen the context of x so that now our goal becomes to substitute x : T. Then we can safely apply t/x. The naturality here is that the order of subtyping and substitution should not matter, but in Coq, it does. 

I guess in my mechanization, one new goal now is to verify that subtyping and substitution can indeed naturally coexist, but at this moment, I do think that there is a problem in Coq. My feeling is that the subtyping decision should be safe; it's probably even structural in beta-eta normal forms.

Thanks,

Jason Hu

https://hustmphrrr.github.io/

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Meven Lennon-Bertrand <mgapb2 AT cam.ac.uk>
Sent: Friday, June 21, 2024 12:26 PM
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Why subtyping rule is not contravariant in input types for Pi

 

Hi Jason,

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 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 :)

Best,

Meven LENNON-BERTRAND
Postdoc – Computer Lab, University of Cambridge
www.meven.ac

On 20/06/2024 16:11, Jason Hu wrote:

Hi all,

I am reading the subtyping rules for Coq: https://coq.inria.fr/doc/V8.18.0/refman/language/cic.html#subtyping-rules

Rule 5 says that Coq only checks equivalence for the input types while only the output types are subject to subtyping. How is the subtyping rule is not contravariant in the input types?

I understand that in System F, this rule is problematic and causes undecidability but I don't think it applies here. In particular, if for the sake of discussion we let U <: T and compare x : U |- T' <: U', this extra information of x : U should affect the result of comparing T' <: U' at all. How is the rule designed in this way? What consideration am I missing here?

Thanks,

Jason Hu

https://hustmphrrr.github.io/