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