Type Systems

A type system assigns types to program expressions, catching errors before runtime. Type systems are one of the most important tools for software correctness.

Static vs Dynamic Typing

Static Typing

Types are checked at compile time. Type errors prevent compilation.

x: Integer ← 42
// y: Integer ← "hello"   // COMPILE ERROR: type mismatch

Languages: Rust, C, C++, Java, Haskell, Go, TypeScript.

Benefits: Catch errors early. Enable IDE support (autocomplete, refactoring). Enable optimization (compiler knows types). Documentation (types are documentation).

Dynamic Typing

Types are checked at runtime. Variables can hold any type.

x = 42
x = "hello"  # OK — x changes type
x + 1         # Runtime error: can't add string and int

Languages: Python, JavaScript, Ruby, Lisp, Erlang.

Benefits: Faster prototyping. More flexible. Less boilerplate.

Costs: Errors discovered late (at runtime, possibly in production). Harder to refactor safely. Less IDE support.

Gradual Typing

Add optional type annotations to a dynamically typed language. Type-checked where annotations exist, dynamically checked elsewhere.

TypeScript = JavaScript + types. mypy = Python + type hints. Sorbet = Ruby + types.

Strong vs Weak Typing

Strong typing: Operations on incompatible types are errors (Rust, Python, Haskell).

"3" + 4  # TypeError in Python (strong)

Weak typing: Implicit coercions between types (JavaScript, C, PHP).

"3" + 4  // "34" in JavaScript (weak — coerces 4 to string)
"3" - 1  // 2 in JavaScript (coerces "3" to number)

Note: Strong/weak is a spectrum, not a binary. Rust is very strong. C is relatively weak (implicit pointer/integer conversions).

Type Inference

The compiler deduces types without explicit annotations.

Hindley-Milner Type Inference

The gold standard. Infers the most general type (principal type) automatically.

x ← 5                         // inferred: integer
y ← [1, 2, 3]                 // inferred: list of integers
z ← MAP(y, v -> v * 2)        // inferred element type

Algorithm W (Damas-Milner, 1982):

1. Assign fresh type variables to all expressions.
2. Generate constraints from the program structure.
3. Solve constraints via unification.
4. Substitute to get concrete types.

Complete inference: Haskell, ML, OCaml — almost no type annotations needed. Partial inference: Rust, Kotlin, Swift — local inference within functions, annotations at function boundaries.

Bidirectional Type Checking

Combine inference (synthesize types bottom-up) and checking (propagate expected types top-down). Used in Rust, TypeScript, Scala 3.

Parametric Polymorphism (Generics)

Write code that works for any type.

FUNCTION IDENTITY<T>(x: T) -> T
    RETURN x

CLASS Stack<T>
    FIELDS: elements (list of T)

Monomorphization (Rust, C++): Compiler generates specialized code for each concrete type. Zero runtime cost. Binary size increases.

Type erasure (Java, Haskell): Generics are erased at runtime. One code path for all types. Information loss at runtime.

Ad-Hoc Polymorphism

Different behavior for different types, selected at compile time.

Overloading

Same function name, different parameter types. The compiler selects the right version.

int add(int a, int b) { return a + b; }
double add(double a, double b) { return a + b; }

Type Classes (Haskell) / Traits (Rust)

Define a set of operations that types can implement.

INTERFACE Display
    FUNCTION FMT(formatter) -> Result

IMPLEMENT Display FOR Integer
    FUNCTION FMT(formatter)
        WRITE(formatter, self)

FUNCTION PRINT_IT<T: Display>(val: T)
    PRINT val

Trait bounds: T: Display + Clone means T must implement both Display and Clone.

Coherence (orphan rule): Each trait implementation must be unique. In Rust, you can implement a trait for a type only if either the trait or the type is defined in your crate.

Subtyping

Type S is a subtype of T (S <: T) if a value of type S can be used wherever a value of type T is expected.

Cat <: Animal
// A Cat can be used wherever an Animal is expected

Variance

How subtyping of type constructors relates to subtyping of their parameters.

Covariant: If S <: T, then F<S> <: F<T>. (Same direction.)

• Vec<Cat> can be used as Vec<Animal> (if read-only).
• Function return types are covariant.

Contravariant: If S <: T, then F<T> <: F<S>. (Reversed direction.)

• Function parameter types are contravariant.
• Fn(Animal) can be used as Fn(Cat) (if a function accepts any animal, it certainly accepts cats).

Invariant: No subtyping relationship.

• Mutable references must be invariant: &mut Vec<Cat> is NOT a subtype of &mut Vec<Animal> (you could insert a Dog through the Animal reference!).

Rust: References are covariant in their lifetime parameter and in their type parameter (for shared refs). Mutable references are invariant.

Advanced Type Features

Existential Types

"There exists a type T such that..." Hides the concrete type behind an interface.

// Existential type: hide the concrete type behind an interface
FUNCTION MAKE_ITER() -> Iterator<Integer>
    RETURN range(0, 10)
// Caller doesn't know the concrete iterator type

Phantom Types

Type parameters that don't appear in the data but enforce compile-time constraints.

// Phantom types: type parameters enforce constraints without storing data
TYPE Meters
TYPE Seconds

CLASS Quantity<Unit>
    FIELDS: value (number)

FUNCTION SPEED(distance: Quantity<Meters>, time: Quantity<Seconds>) -> number
    RETURN distance.value / time.value
// Can't accidentally pass Seconds as Meters — compile error!

GADTs (Generalized Algebraic Data Types)

Constructors can specify different type parameters.

data Expr a where
    IntLit  :: Int -> Expr Int
    BoolLit :: Bool -> Expr Bool
    Add     :: Expr Int -> Expr Int -> Expr Int
    If      :: Expr Bool -> Expr a -> Expr a -> Expr a

eval :: Expr a -> a
eval (IntLit n)    = n
eval (BoolLit b)   = b
eval (Add e1 e2)   = eval e1 + eval e2
eval (If c t f)    = if eval c then eval t else eval f
-- Type-safe! Can't Add two BoolLits.

Type-Level Programming

Compute types at compile time.

// Type-level natural numbers
TYPE Zero
TYPE Succ<N>

TYPE One = Succ<Zero>
TYPE Two = Succ<One>
TYPE Three = Succ<Two>

// Type-level addition via interface
INTERFACE Add<B>
    TYPE Result

IMPLEMENT Add<B> FOR Zero
    TYPE Result = B

IMPLEMENT Add<B> FOR Succ<A> WHERE A: Add<B>
    TYPE Result = Succ<A.Add<B>.Result>
// Succ<Succ<Zero>> + Succ<Zero> = Succ<Succ<Succ<Zero>>>  (2 + 1 = 3)

Dependent Types (Introduction)

Types that depend on values. The most expressive type systems.

// Pseudocode (Idris/Agda style)
Vector : Nat -> Type -> Type
Vector 0     a = Nil
Vector (n+1) a = Cons a (Vector n a)

// append : Vector m a -> Vector n a -> Vector (m + n) a
// The return type depends on the input lengths!

Covered in depth in the advanced type theory topic (topic 41).

Rust's Type System Highlights

• Ownership + borrowing: Prevents use-after-free, double-free, data races at compile time.
• Lifetimes: Types carry information about how long references are valid.
• Algebraic data types: enum for sum types, struct for product types.
• Pattern matching: Exhaustive, with destructuring.
• Trait-based polymorphism: No inheritance. Static (monomorphized) and dynamic (dyn Trait) dispatch.
• No null: Option<T> instead of null pointers.
• No exceptions: Result<T, E> instead of try/catch.

Applications in CS

• Program correctness: Types prevent entire classes of bugs (null pointer, type confusion, buffer overflow in safe languages).
• API design: Types communicate constraints and contracts. A well-typed API is hard to misuse.
• Compiler optimization: Type information enables better code generation (monomorphization, devirtualization).
• Documentation: Types serve as machine-checked documentation.
• Refactoring: Strong types make large-scale refactoring safe (compiler catches all affected code).
• Formal verification: Dependent types can encode program specifications as types (proofs as programs).