Type Theory

What if a program's type is its mathematical proof? Type theory erases the boundary between code and mathematics: the compiler becomes a proof checker, and a bug becomes a logical contradiction.

• **Coq and Agda:** Formal verification of CompCert (bug-free C compiler), seL4 kernel (OS with proven security guarantees)
• **Haskell/Scala:** System F underpins both - parametricity guarantees properties of functions from their types alone
• **Rust:** The borrow checker is a restricted form of linear types, proving memory safety statically

Предварительные знания

• Natural Deduction
• Recursive Functions and Computability Theory

Simply Typed Lambda Calculus

Rust's borrow checker and Haskell's type system are implementations of the Simply Typed Lambda Calculus. TypeScript, used by 10M+ developers, adds STLC-style types to JavaScript. The Curry-Howard correspondence proves that every STLC type is a logical proposition - type-checking is theorem proving.

Types are given by the grammar: τ ::= Base | τ₁ → τ₂. A function of type A→B takes an argument of type A and returns a value of type B. Typing guarantees normalization: every well-typed term evaluates to a normal form.

System F and Polymorphism

System F (Girard, Reynolds, 1972) adds **parametric polymorphism**: functions can be generalized over types. This is the foundation of Haskell, ML, and Scala type systems. In System F, natural numbers, booleans, and recursion can all be encoded via types.

A natural number n is encoded as an iterator: n applies a function n times. This is called Church encoding-an elegant way to represent data through behavior.

The Curry - Howard Isomorphism

The Curry - Howard Isomorphism (CHI) is a deep correspondence between **logic** and **type theory**: types correspond to propositions, programs correspond to proofs. To write a program of type T is to prove the proposition T.

This is not a metaphor-it is a precise isomorphism. The same formalism describes both computation and logical proofs. Coq and Agda exploit this principle for program verification.

Dependent Types: A Preview

Dependent types allow types to **depend on values**. The type 'vector of length n' depends on the number n. This makes the type system powerful enough to express and prove arbitrary mathematical theorems.

In Agda/Coq, the concatenation function has type Vec n A → Vec m A → Vec (n+m) A. The compiler statically verifies the arithmetic of lengths-length errors are impossible.

Key Ideas

• **STLC**: simply typed λ-calculus: types prevent errors and guarantee normalization
• **System F**: adds ∀α (polymorphism): one function works for all types
• **Curry-Howard**: types = propositions, programs = proofs; writing a function means proving a theorem
• **Dependent types**: types depend on values: Vec n A encodes length in the type, making length errors impossible

Related Topics

Type theory unites logic, computation, and mathematics:

• Natural Deduction — STLC typing rules are exactly the rules of intuitionistic natural deduction
• Recursive Functions — System F encodes recursion via types; μ-recursion is linked to non-termination
• Intuitionistic Logic — CHI: intuitionistic logic = types of STLC; constructivity = computability
• MLTT and Dependent Types — The next lesson covers the full story with dependent types and constructive mathematics

Вопросы для размышления

• If a Haskell program compiles, does it mean it is 'correct' in some logical sense?
• What is the difference between proving a theorem in Coq and writing an algorithm in Haskell? Is there a fundamental distinction?
• Dependent types allow expressing arbitrary theorems - why don't all programming languages use them?

Связанные уроки

• plt-09-dependent-types