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

---

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]

---

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.

---

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

Sources

• “Subtyping,” Wikipedia. https://en.wikipedia.org/wiki/Subtyping . Supports subtyping as a relation A <: B grounded in substitutability (a value of a subtype is usable wherever a supertype is expected), and its reflexive and transitive structure.
• “Covariance and contravariance (computer science),” Wikipedia. https://en.wikipedia.org/wiki/Covariance_and_contravariance_%28computer_science%29 . Supports the covariant, contravariant, and invariant treatment of type constructors, the contravariant-input/covariant-output rule for function subtyping, and the unsoundness of covariant mutable arrays.