Type Systems & Type Checking

Informally, a type is a set of values together with the operations that make sense on them. The integer type contains ..., -2, -1, 0, 1, 2, ... and supports addition, subtraction, multiplication. The string type contains "hello", "world", ... and supports concatenation, indexing. Mixing them without conversion is a semantic error.

More precisely, in the tradition of programming language theory, a type is a syntactic classification assigned to expressions. The type system is a set of rules that map every well-formed expression to a type (or flag an error). The assignment is purely syntactic — we read the code, not the runtime values.

This distinction matters: if true then 1 else "hello" has both a 1 (int) and a "hello" (string) at runtime only the 1 is ever evaluated, but a static type system still rejects it because it cannot determine the type of the whole expression without running the program.

Types serve three roles:

1. Documentation: a machine-checked annotation of intent.
2. Optimization: knowing that a value is always a 32-bit int lets the compiler emit a single machine instruction instead of a dynamic dispatch.
3. Safety: the type checker proves that certain bad things (applying a non-function, indexing a non-array) cannot happen at runtime.

-- Haskell: the compiler knows these are different types
add :: Int -> Int -> Int
add x y = x + y

-- add 1 "hello"   -- Type error: expected Int, got String
-- This is caught at compile time, not runtime.

The central axis in type system design is when type checking happens.

Static typing checks types at compile time, before the program runs. Every expression is assigned a type by the compiler. Examples: Java, C, Haskell, Rust, TypeScript. The key benefit is that type errors are caught early, and the type annotations serve as lightweight formal specifications.

Dynamic typing defers type checking to runtime. Values carry their type as a tag, and operations check that tag before proceeding. Examples: Python, JavaScript, Ruby, Lisp. The benefit is flexibility — you can put any value in a list, write generic code without explicit type annotations, and prototype quickly. The cost is that type errors surface only when the bad code path is actually exercised (potentially never in testing, then in production).

A common misconception: "dynamically typed" does not mean "untyped." Python values absolutely have types (type(42) is int). The difference is when and by whom types are checked: compiler vs. runtime.

Gradual typing (TypeScript, mypy for Python, typed Racket) is a modern hybrid: you annotate where you want static guarantees, and unannotated parts remain dynamically checked. The type system inserts runtime checks at the boundary between typed and untyped code.

A subtler distinction: strong vs. weak typing. A strongly typed language (Python, Haskell) never silently coerces incompatible types. A weakly typed language (C, JavaScript) may implicitly reinterpret bits (C's void*, JS's 1 + "2" = "12"). Strong/weak and static/dynamic are independent axes.

# Python — dynamic: error only at runtime
def add(x, y):
    return x + y

add(1, 2)       # fine
add(1, "oops")  # TypeError raised at runtime

// TypeScript — static: error at compile time
function add(x: number, y: number): number {
    return x + y;
}
add(1, "oops"); // TS2345: Argument of type 'string' is not
                // assignable to parameter of type 'number'

The lambda calculus is the minimal formal model of computation with functions. Every Turing-complete language can be encoded in it. The simply-typed variant adds a type discipline that rules out nonsensical programs.

Syntax of the STLC:

Types τ ::= Bool | τ₁ → τ₂ (base types and function types)

Terms t ::= x | λx:τ.t | t₁ t₂ | true | false | if t then t else t

• x — a variable
• λx:τ.t — a function (lambda abstraction) that takes an argument x of type τ and returns t
• t₁ t₂ — function application: apply t₁ to argument t₂

Notice that we annotate the bound variable with its type. This is the key move that makes the calculus "simply typed."

Example terms:

• λx:Bool. x — the identity function on booleans, type Bool → Bool
• λf:Bool→Bool. λx:Bool. f (f x) — applies f twice, type (Bool→Bool) → Bool → Bool
• (λx:Bool. if x then false else true) true — negation applied to true, should reduce to false

The STLC is not Turing-complete — every well-typed STLC program terminates. This is a feature for verification, but a limitation for general programming. Real languages add recursion (and thus the possibility of nontermination) on top.

-- STLC terms in Haskell-like pseudocode
-- Identity on Bool
id_bool :: Bool -> Bool
id_bool x = x

-- Apply f twice
apply_twice :: (Bool -> Bool) -> Bool -> Bool
apply_twice f x = f (f x)

-- In pure lambda notation:
-- λx:Bool. x          : Bool → Bool
-- λf:Bool→Bool. λx:Bool. f (f x)  : (Bool→Bool) → Bool → Bool

A typing judgment has the form Γ ⊢ t : τ, read "under context Γ, term t has type τ." The typing context Γ is a finite map from variable names to types — it records what type each in-scope variable has.

Typing rules are written as inference rules in the style of natural deduction:

        (premises)
    ─────────────────  (rule name)
        (conclusion)

The core rules of the STLC:

T-Var (variable lookup):

    x : τ ∈ Γ
  ────────────
  Γ ⊢ x : τ

T-Abs (lambda abstraction):

  Γ, x:τ₁ ⊢ t : τ₂
  ─────────────────────────
  Γ ⊢ (λx:τ₁. t) : τ₁ → τ₂

T-App (function application):

  Γ ⊢ t₁ : τ₁ → τ₂    Γ ⊢ t₂ : τ₁
  ─────────────────────────────────
        Γ ⊢ t₁ t₂ : τ₂

T-True, T-False: Γ ⊢ true : Bool, Γ ⊢ false : Bool

T-If:

  Γ ⊢ t₁ : Bool   Γ ⊢ t₂ : τ   Γ ⊢ t₃ : τ
  ─────────────────────────────────────────
        Γ ⊢ if t₁ then t₂ else t₃ : τ

A type derivation (or type proof) is a tree of these rules whose root is the judgment we want to establish and whose leaves are axioms (T-Var, T-True, T-False). If a derivation exists, the program is well-typed. The type checker's job is to construct (or refute) such a derivation.

The beauty: type checking is syntax-directed — for each syntactic form of term, exactly one rule applies. This makes type checking decidable and efficient (linear in the size of the term for STLC).

-- Derivation for: ∅ ⊢ (λx:Bool. x) true : Bool
--
-- Step 1: T-True gives  ∅ ⊢ true : Bool
-- Step 2: T-Var gives   {x:Bool} ⊢ x : Bool
-- Step 3: T-Abs gives   ∅ ⊢ (λx:Bool. x) : Bool → Bool
-- Step 4: T-App combines steps 1 and 3:
--         ∅ ⊢ (λx:Bool. x) true : Bool  ✓

-- In Haskell, GHC constructs exactly this derivation implicitly:
result :: Bool
result = (\x -> x) True

"Well-typed programs do not go wrong" — this is the informal statement of type safety (also called soundness). But what does "go wrong" mean precisely? In the STLC, it means reaching a stuck term: a term that is not a value but cannot reduce further (e.g., applying true as if it were a function: true false).

Type safety is established by proving two theorems about the STLC's operational semantics (the rules that describe how terms reduce step-by-step).

Theorem 1 — Progress: If ∅ ⊢ t : τ (t is closed and well-typed), then either t is a value, or there exists a term t' such that t → t' (t can take a step).

Reading: a well-typed program is never stuck. It either is already a final answer (a value), or it can make progress.

Theorem 2 — Preservation (also called Subject Reduction): If Γ ⊢ t : τ and t → t', then Γ ⊢ t' : τ.

Reading: evaluation steps preserve types. If you start with a well-typed term, every intermediate term during evaluation has the same type. Types are invariant under reduction.

Together: start with a well-typed term. By Progress, it either is a value or steps. If it steps, by Preservation the result is still well-typed. By Progress again, still not stuck. By induction, the program runs to completion or diverges — but never crashes with a type error.

Both theorems are proved by structural induction on the typing derivation. The key lemma needed for Progress is the Canonical Forms Lemma: if ∅ ⊢ v : Bool and v is a value, then v is true or false; if ∅ ⊢ v : τ₁→τ₂ and v is a value, then v is a lambda abstraction λx:τ₁.t. This tells you that the shape of a value is determined by its type.

-- Preservation example in pseudocode:
-- Term: (λx:Bool. if x then false else true) true
-- Type: Bool  (by T-App)
--
-- Step 1 (beta-reduce): if true then false else true
--   Still has type Bool  ✓ (Preservation holds)
--
-- Step 2 (if-true): false
--   Still has type Bool  ✓
--
-- false is a value → Progress says we're done, and
-- Preservation says the type is still Bool.

-- A STUCK term (not reachable in STLC but imagine untyped LC):
-- true false   -- 'true' is not a function, can't apply it
-- The type system rejects this before it ever runs.

To prove Progress and Preservation, we need to define precisely what it means for a term to reduce. The standard approach is small-step operational semantics (also called structural operational semantics, SOS), which defines a binary relation t → t' ("t reduces to t' in one step").

The reduction rules for STLC:

E-AppAbs (the key beta-reduction rule):

(λx:τ.t₁₂) v₂ → [x ↦ v₂] t₁₂

Applying a lambda to a value substitutes the value for the bound variable.

E-App1 (reduce the function position):

t₁ → t₁'
──────────────────
t₁ t₂ → t₁' t₂

E-App2 (reduce the argument, once function is a value):

    t₂ → t₂'
──────────────────
v₁ t₂ → v₁ t₂'

E-IfTrue, E-IfFalse:

if true  then t₂ else t₃ → t₂
if false then t₂ else t₃ → t₃

E-If (reduce the condition):

          t₁ → t₁'
──────────────────────────────────────
if t₁ then t₂ else t₃ → if t₁' then t₂ else t₃

The call-by-value strategy (used by most languages: ML, Java, Python) is captured by E-App2: we reduce the argument to a value before substituting. Call-by-name (Haskell's lazy evaluation is call-by-need, a memoized variant) would skip E-App2 and substitute the unreduced argument directly.

Substitution [x ↦ v] t (replace free occurrences of x with v in t) must be defined carefully to avoid variable capture — a subtlety that leads to the notion of alpha-equivalence (renaming bound variables).

-- Trace of: (λx:Bool. λy:Bool. x) true false
-- Step 1: E-AppAbs (outermost application)
--   (λx:Bool. λy:Bool. x) true → λy:Bool. true
--   Term: (λy:Bool. true) false
-- Step 2: E-AppAbs
--   (λy:Bool. true) false → true
--   Term: true  (a value, done)

-- In Haskell, this is just the 'const' function:
const :: a -> b -> a
const x _ = x
-- const True False  =>  True

In the STLC as presented, programmers annotate every lambda parameter with its type. Real languages (Haskell, Rust, OCaml, modern C++) infer most types automatically. Type inference is the process of reconstructing type annotations from the program structure.

The foundational algorithm is Algorithm W by Milner (1978), which solves the type inference problem for the Hindley-Milner (HM) type system — an extension of STLC with parametric polymorphism.

The core idea is unification. The algorithm:

1. Assign a fresh type variable α to every unannotated subexpression.
2. Generate constraints: equations between types. For an application t₁ t₂ where t₁ has type τ₁ and t₂ has type τ₂ and the result has type τ, add the constraint τ₁ = τ₂ → τ.
3. Unify all constraints: find a substitution (mapping type variables to types) that satisfies all equations simultaneously. If unification fails, there is a type error.
4. Apply the resulting substitution to get the inferred types.

Example: λx. x + 1

• Assign type α to x.
• + has type Int → Int → Int, so x + 1 requires α = Int.
• Inferred type of the whole term: Int → Int.

HM type inference is complete: it finds the principal type (most general type) of every typeable expression. Algorithm W runs in nearly-linear time in practice (theoretically almost-linear in the Ackermann function). Rust's type inference is more powerful (it can look ahead to how a value is used) but is consequently incomplete in theory — some programs require explicit annotations.

-- Haskell infers types without any annotations:
twice f x = f (f x)
-- GHC infers:  twice :: (a -> a) -> a -> a
-- Why? f is applied to x (so f :: a -> _)
--      f is applied again to the result (so f :: a -> a)
--      thus f :: a -> a, x :: a, result :: a

-- The constraint system for 'twice f x':
-- Let f :: α, x :: β, result of 'f x' :: γ
-- f x => α = β → γ
-- f (f x) => α = γ → δ
-- From both: β → γ = γ → δ  =>  β=γ=δ=a (free variable)
-- Final: twice :: (a->a) -> a -> a  ✓

Parametric polymorphism (generics) lets a single function work over many types. In HM, the type of the identity function is ∀a. a → a — it works for any type a. This is System F (Girard-Reynolds) at its simplest.

The Curry-Howard correspondence is one of the deepest results in logic and computer science: types are propositions, and programs are proofs. Under this correspondence:

A function f : A → B is a proof that "if A then B." Applying it to a proof a : A gives a proof f a : B. Type-checking is proof-checking. The lambda calculus is a proof calculus.

This is not a metaphor — it is a precise bijection. Proof assistants like Coq, Lean, and Agda are built on this correspondence: writing a program is constructing a proof, and the type checker verifies your proof is valid.

For the practitioner: this means that when you define a type like Result<T, E> in Rust or Either e a in Haskell, you are doing lightweight formal specification. A function f : Input -> Result<Output, Error> is literally a proof sketch: "given a valid input, I either produce a valid output or a well-typed error."

-- Curry-Howard in Haskell:
-- The type (a -> b) -> a -> b  is the proposition "(A→B)→A→B"
-- The term  \f x -> f x        is its proof (modus ponens!)
mp :: (a -> b) -> a -> b
mp f x = f x  -- This is modus ponens as a program.

-- The type  (a, b) -> a  is the proposition "A∧B → A"
fst' :: (a, b) -> a
fst' (x, _) = x  -- Proof: from A and B, extract A.

-- The empty type has no inhabitants → corresponds to False
-- A function  Void -> a  is a proof of "False → anything"
-- (ex falso quodlibet), and it is vacuously true.

A type system is sound if every well-typed program satisfies the safety property — Progress + Preservation hold. Soundness is a theorem, not a design goal you can approximate. You either prove it or you don't.

Many real type systems are deliberately unsound for pragmatic reasons:

• Java arrays are covariant: String[] is a subtype of Object[], which allows storing a non-String into a String[] array — caught only at runtime with ArrayStoreException.
• TypeScript with any: any cast to any escapes the type system entirely.
• C casts: (int*)ptr can reinterpret any pointer, bypassing all type guarantees.

These are escape hatches — they grant power at the cost of soundness. The key insight: unsoundness is a choice. Language designers make it deliberately when the alternative (a stricter but sound rule) would be too inconvenient.

Type safety vs. memory safety: a type-safe language can still have memory issues if it uses a garbage collector and GC pressure causes OOM. A memory-safe language additionally guarantees no use-after-free, no buffer overflow, no dangling pointers — Rust's borrow checker provides this through an affine type system.

Blame assignment in gradual type systems: when a runtime check fails at the boundary between typed and untyped code, the system must assign blame correctly — was it the typed side or the untyped side that violated the contract? This is the core technical challenge of gradual typing theory (Tobin-Hochstadt & Felleisen, 2006).

// Java: covariant arrays — a classic soundness hole
String[] strings = new String[1];
Object[] objects = strings;   // allowed (covariance)
objects[0] = 42;              // compiles! But throws
                              // ArrayStoreException at runtime

// Haskell: no such hole — type system is sound
-- You cannot put an Int into a [String]; rejected at compile time.

// Rust: sound AND memory-safe via borrow checker
let v: Vec<String> = vec!["hello".to_string()];
// v[0] = 42;  // compile error: type mismatch
// Rust also prevents use-after-free, dangling references, etc.

Subtyping adds a relation τ₁ <: τ₂ meaning "a value of type τ₁ can be safely used wherever a τ₂ is expected." The subsumption rule allows upcasting:

Γ ⊢ t : τ₁    τ₁ <: τ₂
────────────────────────
      Γ ⊢ t : τ₂

The most important subtyping rule for functions is contravariance in the argument, covariance in the return:

τ₁' <: τ₁    τ₂ <: τ₂'
──────────────────────────
(τ₁ → τ₂) <: (τ₁' → τ₂')

Intuitively: a function that accepts a broader input (τ₁' which τ₁ is a subtype of — i.e., accepts more things) and returns a narrower output is strictly more capable — it can do everything the original could do and more.

This formalizes the Liskov Substitution Principle (LSP) from object-oriented design: if S is a subtype of T, then objects of type S may be used wherever objects of type T are expected, without altering the program's correctness.

Variance in generics: List<Cat> is not automatically a subtype of List<Animal> even if Cat <: Animal. If it were, you could add a Dog to a List<Cat> via List<Animal>. This is why Java generics are invariant (unlike arrays). Scala and Kotlin allow explicit variance annotations (+T for covariant, -T for contravariant).

-- Haskell doesn't have subtyping but we can illustrate in Scala:
// Scala variance:
class Animal
class Cat extends Animal

// List is covariant in Scala: List[Cat] <: List[Animal]
val cats: List[Cat] = List(new Cat)
val animals: List[Animal] = cats  // OK — covariant

// Function[-A, +B]: contravariant in A, covariant in B
val f: Animal => String = (a: Animal) => a.toString
val g: Cat => String = f  // OK: Animal=>String <: Cat=>String
//  because Cat <: Animal (contravariant input),
//  and String <: String (covariant output)