Stream: Coq users

Topic: Contravariant subtyping

Meven Lennon-Bertrand (Mar 06 2023 at 14:33):

Pierre-Marie Pédrot said:

(that said it's not true in the Set model and I wouldn't be surprised if it contradicted mildly classical axioms)

Is it really not? Maybe not on the nose in a naïve way, but surely you can build a set-theoretic model of explicit contravariant subtyping? And I believe this explicit subtyping would satisfy enough equations that you can elaborate implicit subtyping to it

Meven Lennon-Bertrand (Mar 06 2023 at 14:34):

Also, what
Pierre-Marie Pédrot said:

(that said it's not true in the Set model and I wouldn't be surprised if it contradicted mildly classical axioms)

Also, what classical axioms do you have in mind, and how would they fail?

Pierre-Marie Pédrot (Mar 06 2023 at 14:36):

changing the interpretation of functions in Set into something else makes it a non-Set model, to me. Adding explicit subtyping is more subtle, I agree that cumulativity is basically underspecified in Set but interpreting it as something else than inclusion does make it not really set-theoretic (e.g. I think it matters for weird stuff like Prop ⊆ Type).

Paolo Giarrusso (Mar 06 2023 at 14:37):

IIRC contravariant subtyping _on types_ (not universes) was trivial at least in a _logical relations_ set-theoretic model of implicit subtyping... I wonder which of those differences breaks it, maybe the log rel part?

Pierre-Marie Pédrot (Mar 06 2023 at 14:37):

As for axioms, anything that looks like EM has consequences about the existence (or not) of bijections between sets constructed as impredicative fixpoints, so YMMV.

Pierre-Marie Pédrot (Mar 06 2023 at 14:38):

@Paolo Giarrusso you're talking about a universe-free theory, I assume? I.e. you can interpret your logical relation as a proof-irrelevant predicate on terms?

Meven Lennon-Bertrand (Mar 06 2023 at 14:41):

Pierre-Marie Pédrot said:

changing the interpretation of functions in Set into something else makes it a non-Set model, to me. Adding explicit subtyping is more subtle, I agree that cumulativity is basically underspecified in Set but interpreting it as something else than inclusion does make it not really set-theoretic (e.g. I think it matters for weird stuff like Prop ⊆ Type).

So for you interpreting cumulativity as the existence of a coercion/injection between the two sets is not Set-theoretic? Then maybe this is where we disagree, but I feel like non-hardcore set-theorists blur the line between the two quite a bit

Meven Lennon-Bertrand (Mar 06 2023 at 14:43):

Pierre-Marie Pédrot said:

As for axioms, anything that looks like EM has consequences about the existence (or not) of bijections between sets constructed as impredicative fixpoints, so YMMV.

Not sure I see the relation of this with the rest… If you mean that in a system with explicit cumulativity you'd have to be careful about what you do with inductive types, then I agree. But I'm not sure I see the relation with EM

Pierre-Marie Pédrot (Mar 06 2023 at 14:46):

I have no precise example obviously, but a lot of these weird "paradoxes" from EM are statements about the non-existence of retractions between e.g. X and (X → R) → R for well-chosen X and R, oftentimes involving Prop. Given the shape of these objects, I wouldn't be surprised if this were conflicting with contravariant subtyping, since it gives you more definitional retractions. But again, this is just baseless blabbering.

Meven Lennon-Bertrand (Mar 06 2023 at 14:47):

Paolo Giarrusso said:

IIRC contravariant subtyping _on types_ (not universes) was trivial at least in a _logical relations_ set-theoretic model of implicit subtyping... I wonder which of those differences breaks it, maybe the log rel part?

AFAICT, the big problem with contravariant subtyping in set-theory is that it is not on the nose: if $A \subseteq A'$, you do not get a literal inclusion $A' \to B \subseteq A \to B$, only an injection $i : A' \to B \subseteq A \to B$ which discards those pairs in $A' \to B$ whose first component is not in $A$. But interpreting implicit subtyping by the existence of an inclusion is a pain, because you need this inclusion to respect all term-formers from your theory for it to be "transparent enough"

Meven Lennon-Bertrand (Mar 06 2023 at 14:48):

Which is why I think going first through an equivalence with a theory with explicit coercion + all the equations it should satisfy, and then into set-theoretic (or other) models is saner, as it separates the concerns

Paolo Giarrusso (Mar 06 2023 at 19:18):

yeah, with log rels _on terms_ subtyping's on the nose because the "elements" are the same terms — if $\forall v \in A', f\; v \in B$ and $A \subseteq A'$ then $\forall v \in A, f\; v \in B$

Leo Colisson (Mar 07 2023 at 07:43):

Oups, sorry I forgot to create a new thread.

Last updated: Oct 04 2023 at 23:01 UTC