Inclusions and subtypes II: Higher-order case

The first-order theory of subtypes as inclusions developed in Part I is extended to a higher-order context. This involves providing a higher-order equational logic for (inclusive) subtypes, a categorical semantics for such a logic that is complete and has initial models, and a proof that this higher-order logic is a conservative extension of its first-order counterpart. This higher-order categorical semantics includes a new notion of homomorphism between models that is both very natural in terms of its preservation properties and substantially more general than other notions of higher-order homomorphism proposed previously. The categorical semantics of higher-order inclusive subtypes is then generalized to a notion of model with two subtype relations τ ≤ τ′ (inclusion) and τ ≤: τ′ (implicit conversion) thus reconciling and relating the two different intuitions that have so far prevailed in the first-order and higher-order cases. Axioms are then given that integrate the ≤ and ≤: relations in the unified categorical semantics. Besides enjoying the benefits provided by each of the notions without their respective limitations, this framework supports rules for structural subtyping that are more informative and can discriminate between inclusions and implicit conversions.