5 min read
On this page

Advanced Type Systems

Type Safety

Type safety means well-typed programs do not "go wrong" at runtime. Formally established via two theorems.

Progress

If e : T (closed, well-typed term), then either e is a value or there exists e' such that e -> e'.

No well-typed closed term gets stuck. Proved by case analysis on the typing derivation.

Preservation (Subject Reduction)

If e : T and e -> e', then e' : T.

Types are preserved across evaluation steps. Proved by induction on the typing derivation, with substitution lemma as key dependency.

Together, progress + preservation guarantee: evaluation of well-typed terms either produces a value of the expected type, diverges, or (in languages with effects) raises a controlled exception. They never reach an undefined state.

System F (Polymorphic Lambda Calculus)

Extends the simply-typed lambda calculus with universal type quantification.

Syntax

Types:  T ::= α | T1 -> T2 | ∀α. T
Terms:  e ::= x | λx:T. e | e1 e2 | Λα. e | e [T]
  • Λα. e abstracts over a type variable (type abstraction)
  • e [T] instantiates a polymorphic term (type application)

Key Typing Rule

Γ |- e : ∀α. T
─────────────────
Γ |- e [S] : T[S/α]

Examples

id   : ∀α. α -> α           = Λα. λx:α. x
auto : (∀α. α -> α) -> (∀α. α -> α) = λf:(∀α. α -> α). f [∀α. α -> α] f

Properties

  • Type inference is undecidable (Wells, 1999)
  • Rank-2 polymorphism is decidable; rank-1 (Hindley-Milner) has principal types
  • System F is strongly normalizing (all well-typed terms terminate)
  • Parametricity (Wadler's "free theorems"): the type of a polymorphic function constrains its behavior. E.g., any f : ∀α. α -> α must be the identity

System F-omega

Extends System F with type-level computation via type operators (functions from types to types).

Kinds:  K ::= * | K1 -> K2
Types:  T ::= α | T1 -> T2 | ∀α:K. T | λα:K. T | T1 T2
  • Kind * classifies proper types
  • Kind K1 -> K2 classifies type constructors
  • λα:K. T is a type-level function; T1 T2 is type-level application

Example: List : * -> * is a type constructor of kind * -> *.

System F-omega subsumes System F and is the theoretical basis for ML module systems and Haskell's type system (with extensions).

Subtyping

Subtyping S <: T means a value of type S can be used wherever type T is expected.

Subsumption Rule

Γ |- e : S    S <: T
─────────────────────
      Γ |- e : T

Function Subtyping

T1 <: S1    S2 <: T2
─────────────────────
S1 -> S2 <: T1 -> T2

Contravariant in the argument, covariant in the result.

Record Subtyping

Width subtyping: {x:A, y:B, z:C} <: {x:A, y:B} (more fields is a subtype). Depth subtyping: if A <: A', then {x:A} <: {x:A'}.

Complications

  • Subtyping + parametric polymorphism: bounded quantification ∀α <: T. ... (System F-sub). Type checking becomes undecidable for full F-sub
  • Algorithmic subtyping must be carefully designed to avoid infinite loops with recursive types
  • Coercive vs. inclusive interpretations: does subtyping insert runtime conversions or is it purely structural?

Intersection and Union Types

Intersection Types

e : A ∩ B means e has both type A and type B.

Γ |- e : A    Γ |- e : B
─────────────────────────
      Γ |- e : A ∩ B
  • Characterize strong normalization: a term is strongly normalizing iff it is typable with intersection types
  • Used in refinement type systems and overloading
  • TypeScript uses intersection types (A & B)

Union Types

e : A ∪ B means e has type A or type B.

  • Elimination requires case analysis or exhaustive checking
  • Untagged unions (TypeScript) vs. tagged unions (sum types)
  • Distributes over functions: (A -> C) ∩ (B -> C) <: (A ∪ B) -> C

Recursive Types

Types that refer to themselves: T = μα. F(α).

Equi-recursive vs. Iso-recursive

  • Equi-recursive: μα. F(α) is equal to F(μα. F(α)). Types are infinite regular trees. Type checking requires structural equality on recursive types
  • Iso-recursive: μα. F(α) and F(μα. F(α)) are isomorphic but distinct. Explicit fold/unfold coercions. Used in ML (datatype), Haskell (newtype)

Example

List α = μL. Unit + (α × L)
   unfold: List α -> Unit + (α × List α)
   fold:   Unit + (α × List α) -> List α

Recursive types are needed for self-application λx. x x (typeable as μα. α -> T), recursive data structures, and object encodings.

Row Polymorphism

Polymorphism over record structure. A row variable ρ represents "the rest of the fields."

f : ∀ρ. {x : Int | ρ} -> Int
f r = r.x

f works on any record with at least an x : Int field.

  • Avoids the complexity of width subtyping while providing similar flexibility
  • Used in OCaml (polymorphic variants), PureScript, Elm
  • Row types support: field access, extension, restriction, and update
  • Lacks the "forgetting" semantics of subtyping but is decidable and has principal types

Gradual Typing

Bridges static and dynamic typing within a single language.

The Dynamic Type

A special type ? (or * or Dyn) is consistent with every type. Consistency ~ replaces equality in type checking.

A ~ ?    ? ~ A    (for all A)
A ~ A

Consistency is reflexive and symmetric but NOT transitive (otherwise all types would be consistent).

Runtime Casts

When static information is insufficient, the compiler inserts runtime casts (checks):

<Int <= ?> : ? -> Int     (cast from dynamic to Int, may fail)
<? <= Int> : Int -> ?     (always succeeds)

Properties

  • Gradual guarantee: adding type annotations never changes the behavior of a program (only makes it fail earlier with a cast error)
  • Fully annotated: behaves like static typing. Unannotated: behaves like dynamic typing

Blame Calculus

Formalizes who is responsible when a cast fails.

  • Every cast is labeled with blame labels: <T <= S>^l
  • When a cast fails, the blame label identifies the source of the type mismatch
  • Blame theorem (Wadler-Findler): if a term with precise type annotations is composed with a less precisely typed term, blame never falls on the precisely typed side
  • Positive/negative blame: tracks whether the failure is in the value produced or consumed
  • Provides theoretical foundation for contract systems and gradual typing implementations

Summary Table

| System | Key Feature | Decidable Checking | |---|---|---| | Simply typed | Basic function types | Yes | | Hindley-Milner | Rank-1 polymorphism, inference | Yes (principal types) | | System F | Impredicative polymorphism | No (type inference) | | System F-omega | Type operators, higher kinds | Yes (checking, not inference) | | F-sub | Bounded quantification | No (full), Yes (kernel) | | Gradual | Static-dynamic interop | Yes (with casts) | | Intersection | Multiple types for one term | No (general) |

Each extension trades off expressiveness against decidability and complexity. Practical languages pick points in this design space: Haskell approximates System F-omega with extensions; TypeScript uses structural subtyping with unions/intersections; Typed Racket uses gradual typing with blame.