Subtyping, Variance & Type Constraints

Overview

Subtyping adds hierarchy to type systems, enabling reuse and polymorphism.
When combined with generics or functions, however, it introduces variance problems — subtle but essential for type safety.

Note

Subtyping extends type systems horizontally (via relationships between types), while parametric polymorphism extends them vertically (via generic abstraction).

---

What Is Subtyping?

A type A is a subtype of B (A <: B) if every value of A can safely be used wherever a B is expected.

Formally:

A <: B ⇒ for all contexts C[•], if C[B] is valid, then C[A] is valid

This property is known as substitutability — the foundation of type-safe reuse.

Example:

class Animal {}
class Dog extends Animal {}
 
Animal a = new Dog();  // OK: Dog <: Animal

Tip

Subtyping ≠ inheritance, but many OO languages conflate the two.
In pure type theory, subtyping is a semantic relation, not a syntactic one.

---

The Subtyping Relation

Subtyping is reflexive and transitive:

A <: A
A <: B  and  B <: C  ⇒  A <: C

Languages extend this with additional rules for:

• Function types

• Product / record types

• Union and intersection types

• Generic type constructors

---

Function Types and Variance

Functions flip the direction of subtyping on parameters.

(A → B) <: (A' → B')  ⇔  A' <: A  ∧  B <: B'

Component	Direction	Intuition
Parameter (input)	Contravariant	Accepts more general arguments
Result (output)	Covariant	Returns more specific results

Example (in type-lambda form):

Parent → Child  <:  Animal → Object

Because:

• Animal is broader than Parent (contravariant on input),

• Child is narrower than Object (covariant on output).

Example

Diagram (function_variance.svg)
Arrows showing how subtyping reverses on inputs and preserves direction on outputs.

---

Variance of Type Constructors

When a type constructor F (like List or Box) wraps a type T, the question arises:

If A <: B, does that imply F[A] <: F[B]?

Possible Answers

Variance	Rule	Example	Safe For
Covariant	A <: B ⇒ F[A] <: F[B]	List[Dog] <: List[Animal]	Read-only containers
Contravariant	A <: B ⇒ F[B] <: F[A]	Comparator[Animal] <: Comparator[Dog]	Consumers (function arguments)
Invariant	Neither direction holds	Array[Dog] ≮: Array[Animal]	Mutable containers

Warning

Covariance becomes unsafe when mutation is allowed — you could insert a Cat into an array of Dog.

---

Example — Why Arrays Are Invariant

Java allows covariant arrays, but it’s unsound:

Animal[] animals = new Dog[1];
animals[0] = new Cat(); // Runtime ArrayStoreException

The type system lets it compile but must insert runtime checks to preserve safety.
Modern designs (like generics in Java or C#) default to invariance for mutable types.

---

Variance Ladder

Covariance, invariance, and contravariance form a conceptual ladder of generality.

Variance	Symbol	Meaning	Example
Covariant	+	Preserves subtyping	List[+T]
Invariant	0	No subtyping	Array[T]
Contravariant	-	Reverses subtyping	Func[-T]

Example

Diagram (variance_ladder.svg)
Three stacked levels with arrows showing direction of substitution.

---

Bounded Type Parameters

To control variance and maintain soundness, languages introduce type bounds:

Upper Bounds

T <: U — type parameter T must be a subtype of U.

class Box<T extends Number> { ... }

Lower Bounds

L <: T — type parameter T must be a supertype of L.

void copy(List<? super Integer> dest, List<? extends Integer> src)

These enable safe reuse across hierarchies:

• Upper bounds restrict outputs.

• Lower bounds restrict inputs.

Example

Diagram (bounded_types.svg)
Vertical arrow diagram showing allowed instantiations under extends and super.

---

Type Constraints and Type Inference

Type inference engines enforce and propagate subtyping relations:

Γ ⊢ e : A
A <: B
──────────────
Γ ⊢ e : B

This subsumption rule allows using an expression of a subtype wherever a supertype is expected.

Constraints (T <: U, L <: T) form a constraint graph, solved during compilation.

Note

In Hindley–Milner-like systems, explicit subtyping is often replaced by typeclass constraints or structural matching.

---

Interaction with Polymorphism

Subtyping and polymorphism interact in two main ways:

1. Ad-hoc polymorphism (overloading) — multiple implementations for distinct subtypes.

2. Parametric polymorphism — one generic definition for all types.

3. Subtype polymorphism — one definition reused through subtyping hierarchy.

Tip

Languages like Scala, Kotlin, and TypeScript unify these under flexible variance annotations and bounded generics.

---

Conceptual Summary

Concept	Meaning	Rule
Subtyping	Safe substitutability	A <: B
Variance	How subtyping lifts through type constructors	Covariant (+), Contravariant (-), Invariant (0)
Function Subtyping	Inputs contra, outputs co	(A→B) <: (A'→B') if A' <: A and B <: B'
Bounds	Restrict valid substitutions	T <: U, L <: T
Constraints	Relations solved during inference	Γ ⊢ e : A and A <: B ⇒ Γ ⊢ e : B

---

See also

• Hindley–Milner Type Inference

• Type Systems — Goals & Guarantees

• Objects, Classes, and Dispatch

• Parametric Polymorphism & ADTs