Эти типы находятся в отношении подтипа, в точности , потому что противоречивости. Объединение было бы супертипом A и C, поэтому нарушало бы контравариантность.
Напомним правило подтипа для функций, которое является контравариантным в типе домена:
T → U <: T '→ U' тогда и только тогда, когда T '<: T и U <: U' </p>
Для типов пересечений у вас также есть правило распределения по типам стрелок:
(T → U) ∧ ( T → V) = T → (U ∧ V)
И, конечно, у нас есть обычные правила исключения для типов пересечений:
T ∧ U <: T <br>T ∧ U < : U
Объединяя эти четыре правила вместе, вы можете легко получить подтип, о котором вы спрашиваете:
(A → B) ∧ (C → D)
<: (из-за контравариантности и устранения слева) <br>((A ∧ C) → B) ∧ (C → D)
<: (из-за контравариации и исключения справа) <br>((A ∧ C) → B) ∧ ((A ∧ C) → D)
<: (по дистрибутиву) <br>(A ∧ C) → (B ∧ D)
FWIW, с объединением типов, у вас также есть двойной дистрибутив Правило ти:
(U → T) ∨ (V → T) = (U ∨ V) → T
При этом вы можете аналогично получить:
(A → B) ∨ (C → D) <: (A ∨ C) → (B ∨ D) </p>