Search code examples
subtypetype-theory

Is (A -> B) /\ (C -> D) <: (A /\ C) -> (B /\ D)?

Is (A -> B) /\ (C -> D) a subtype of (A /\ C) -> (B /\ D)?

It seems like it shouldn't be, simply on account of -> being contravariant, but I can't find a good counterexample.

If it is, how can I derive this?

If not, what would a counterexample be?

(To clarify, I'm using /\ for intersection here.)

Solution

  • These types are in a subtype relation, precisely because of contravariance. The union would be a supertype of A and C, so would violate contravariance.

    Recall the subtyping rule for functions, which is contravariant in the domain type:

    T → U <: T' → U' iff T' <: T and U <: U'

    For intersection types, you also have a distributivity rule over arrow types:

    (T → U) ∧ (T → V) = T → (U ∧ V)

    And of course we have the usual elimination rules for intersection types:

    T ∧ U <: T
    T ∧ U <: U

    Plugging these four rules together, you can easily derive the subtyping you're asking about:

    (A → B) ∧ (C → D)
    <: (by contravariance and left elimination)
    ((A ∧ C) → B) ∧ (C → D)
    <: (by contravariance and right elimination)
    ((A ∧ C) → B) ∧ ((A ∧ C) → D)
    <: (by distributivity)
    (A ∧ C) → (B ∧ D)

    FWIW, with union types, you also have the dual distributivity rule:

    (U → T) ∨ (V → T) = (U ∨ V) → T

    With that, you can analogously derive:

    (A → B) ∨ (C → D) <: (A ∨ C) → (B ∨ D)