The Coq mailing list

[Meven Lennon-Bertrand <mgapb2 AT cam.ac.uk>]

    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:

PH0PR14MB5382BC042261BC72FDC449C1AFC82 AT PH0PR14MB5382.namprd14.prod.outlook.com">

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/