Dependent Types

What if the compiler could prove: "this function never receives an empty list", "this index is always within array bounds", "this file is open before reading"? Not through tests, not through assertions - as a mathematical theorem, at compile time. Dependent types do exactly this: types become specifications, and programs become proofs.

• **Aerospace (Airbus, NASA):** verification of safety-critical software through Coq and Agda - dependent types as formal correctness proofs
• **Liquid Haskell at Jane Street:** financial code with refinement types - proven absence of divide-by-zero and out-of-bounds access
• **Rust const generics:** `[T; N]` - an array of exactly N elements, a direct descendant of dependent type ideas, already in production

Dependent Functions and Pi-Types

An ordinary function `length : List a -> Int` returns the same type `Int` regardless of the argument. A **dependent function** (Pi-type) allows the return type to depend on the *value* of the argument. The function `replicate : (n : Nat) -> a -> Vect n a` returns a vector of *exactly n elements* - guaranteed at the type level, not by tests.

The notation `(n : Nat) -> Vect n a` reads: "for each natural number n, the type Vect n a". The return type literally contains the variable `n`. This is a Pi-type (Π-type): a generalization of the function type where the codomain depends on the value of the argument.

**Pi-type vs parametric polymorphism:** `List a` has one implementation for any `a`, the type never changes. `Vect n a` - each value of `n` produces a *different type*. This is one level more expressive than generics.

Propositions as Types: the Curry-Howard Correspondence

In 1934, Curry noticed that combinators in logic correspond to types in lambda calculus. Howard formalized this in 1969. The result - the **Curry-Howard correspondence**: logical propositions and types are the same thing, and proofs and programs are also the same thing.

The consequence: if a program compiles, it is already a proof of the proposition corresponding to its type. In dependently typed languages, types can express arbitrary mathematical statements, and the compiler verifies their correctness.

**Practical consequence:** systems like Agda, Coq, Lean 4, and Idris use this isomorphism to verify programs. Proving a theorem = writing a function of the required type.

Idris 2: Dependent Types in Practice

Idris 2 is a language with full dependent types, aimed at practical use rather than pure theory. Its creator Edwin Brady describes the goal as "programming with proofs". Unlike Agda or Coq, Idris compiles to executable code and has syntax similar to Haskell.

The **state machines through types** idiom is particularly useful: an object's state is encoded in its type. `File Open` and `File Closed` are different types, and `read` only accepts an open file. The resource usage protocol becomes part of the type system.

**Holes and interactive development:** Idris supports `?hole` in code - the compiler shows what type needs to be constructed at that point. This makes writing proofs an interactive process.

Refinement Types: Liquid Haskell

Full dependent types require manual proofs. **Refinement types** are a practical compromise: a base type is refined by a logical predicate, and an SMT solver (Z3) checks correctness automatically. The programmer writes annotations; the compiler finds the proofs.

Liquid Haskell works on top of ordinary Haskell - no new type system required. Annotations do not affect runtime; they give the compiler additional information for verification. The Z3 SMT solver automatically finds proofs for simple arithmetic properties.

**Limits of refinement types:** SMT solvers handle many cases automatically, but not all. Complex proofs (e.g., commutativity of natural number multiplication) require manual lemmas. Full dependent types in Idris/Agda are more expressive but more labor-intensive.

Dependent Types

• Pi-type: the return type of a function depends on the *value* of the argument - `Vect n a` contains exactly n elements
• Curry-Howard correspondence: propositions = types, proofs = programs; compiled code is a proof
• Idris 2: state machines in types, safe indexing, protocol verification at the compiler level
• Liquid Haskell: refinement types with SMT automation - a practical compromise without manual proofs

Related Topics

Dependent types unite type theory, logic, and formal verification.

• Algebraic Data Types — Foundation: dependent types extend ADTs
• Linear and Affine Types — Another approach to static guarantees - resource lifecycle management
• Theorem Provers — Coq, Agda, Lean - systems where dependent types became the language of proofs

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

• The Pi-type `(n : Nat) -> Vect n a` and the parametric type `[a]` - what is the fundamental difference in the information available to the compiler?
• The Curry-Howard correspondence says: a function `A -> B` proves `A → B`. What does the function `(a -> b) -> ([a] -> [b])` (i.e., map) prove?
• In which domains (aerospace, medicine, finance, web) do the costs of dependent types pay off, and where is ordinary TDD sufficient?

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

• plt-08-generics — Dependent types generalize generics; parametric polymorphism is a conceptual prerequisite
• plt-06-lambda-calculus — Dependent type theory is an extension of typed lambda calculus (System F -> CoC)
• plt-07-algebraic-types — Dependent pattern matching over ADTs is a core use case in dependently-typed languages
• plt-10-linear-types — Both dependent and linear types represent advanced type theory; studying them together reveals the space of type system expressiveness
• ml-01