← def, let, implicit arguments Index

Recall

Formal definitions cited in this section, gathered here for quick reference (full citations in the Bibliography):

Every function seen so far has a fixed codomain: double : Nat → Nat returns a Nat regardless of the input n. Lean’s type theory allows something more general: a type that itself depends on a value, and a function whose return type changes depending on which argument it was given. This is a dependent type. It is the single feature that separates Lean (and other proof assistants) from an ordinary typed programming language, so it is worth building up slowly, from the smallest possible example, before naming the general pattern.

The problem, in Python first

Before any Lean syntax, here is the actual problem dependent types solve, in a language with no type checker enforcing anything at all. Suppose a dot-product function is written over two lists:

def dot(xs, ys):
    return sum(x * y for x, y in zip(xs, ys))

dot([17, -3, 42], [99, 8, 6])   # 1911 — correct
dot([17, -3, 42], [99, 8])      # 1659 — silently wrong: zip() truncates to the shorter list

This is worse than a crash. dot([17, -3, 42], [99, 8]) does not raise anything — zip just quietly drops the third element of xs and hands back a number that looks like a perfectly good answer. The bug (calling dot on two lists of different lengths, which is mathematically nonsensical) is never caught, not by Python, not by a test that happens not to cover this call site, not by anything short of a human noticing the number looks off.

The underlying mistake is that a Python list carries no information about its own length in any way Python’s function signatures can see or enforce. xs : list and ys : list say nothing about whether the two lists agree in size — that fact exists only as a comment at best, never checked by anything. What is actually wanted is a signature saying “dot accepts two lists of the same length n, for any n” — a signature that mentions and constrains a value (n), not just a type (list). Ordinary type systems, Python’s included even with type hints added, have no way to say that. This is exactly the gap dependent types close, and the rest of this section builds the machinery to say it, starting from the smallest possible example.

First: a type family, one type per number

Here is the smallest genuine example of a dependent type, and it is already sitting in Lean’s core library. Fin n is the type of natural numbers strictly less than n:

#check Fin 3   -- Fin 3 : Type
#check Fin 5   -- Fin 5 : Type

Fin itself is not one type. It is a recipe that produces a type once handed a number: Fin 3 and Fin 5 are both genuine types, but they are different types — Fin 3 has exactly three inhabitants (the numbers 0, 1, 2) and Fin 5 has exactly five. Compare this to something already known not to be dependent, List α: List Nat and List Bool are different types too, but only because Nat and Bool are different types fed in for α. Fin is a different kind of thing. Fin 3 and Fin 5 differ even though 3 and 5 are both perfectly ordinary terms of the exact same type, Nat. The type Fin produces depends on which value it is given, not just which type. That value-dependence is the entire definition of “dependent type,” and Fin is the simplest possible example of one.

The construction of Fin can be inspected directly:

#print Fin
-- structure Fin (n : Nat) : Type
-- fields:
--   Fin.val  : Nat
--   Fin.isLt : val < n

So a term of Fin n is literally a pair: a Nat value, plus a proof that the value is below n. The proof’s very statement (val < n) mentions n, the value supplied. Change n and the result is a genuinely different type, with a genuinely different proof obligation attached. This bundling — data, plus a proof whose statement depends on that data — is the second half of the dependent-types story (formalized later in this section as a Σ-type); Fin is a real, live example of it, not a made-up one.

Second: a function whose return type changes with its argument

Now for the companion idea: a dependent function, one whose return type depends on the specific value of its argument, not just the argument’s type. Define fixed-length vectors from scratch, the standard first example in any dependent-type-theory course:

inductive Vec (α : Type) : Nat → Type where
  | nil  : Vec α 0
  | cons : α → Vec α n → Vec α (n + 1)

Read this exactly like Nat’s two-constructor definition from the previous section, with one new ingredient: Vec α is not a single type, it is a family of types indexed by a Nat — Vec α 0, Vec α 1, Vec α 2, … are all different types, one per length, and the length is tracked in the type itself, not just at runtime. nil builds the unique length-0 vector; cons takes an element and a length-n vector and produces a length-(n+1) vector — the n used on both sides of cons’s arrow is the same n, so the constructor itself enforces “one longer than whatever it started with.”

Here is a function that builds one of these, and its type is the dependent-function payoff:

def Vec.replicate (a : α) : (n : Nat) → Vec α n
  | 0     => Vec.nil
  | n + 1 => Vec.cons a (Vec.replicate a n)

#check @Vec.replicate
-- @Vec.replicate : {α : Type} → α → (n : Nat) → Vec α n

#eval (Vec.replicate (-42 : Int) 3 : Vec Int 3)
-- Vec.cons (-42) (Vec.cons (-42) (Vec.cons (-42) Vec.nil))

Vec.replicate recurses exactly once per unit of length, so it is worth watching the recursion unwind one call at a time. Adding a dbg_trace line to each branch (harmless — it only prints, and changes nothing about what the function returns) makes every step visible:

def Vec.replicate' (a : α) : (n : Nat) → Vec α n
  | 0     => dbg_trace s!"replicate: n=0, base case, returning Vec.nil"; Vec.nil
  | n + 1 => dbg_trace s!"replicate: n={n+1}, prepending one copy of a, recursing with n={n}";
             Vec.cons a (Vec.replicate' a n)

#eval (Vec.replicate' (-42 : Int) 3 : Vec Int 3)
-- replicate: n=3, prepending one copy of a, recursing with n=2
-- replicate: n=2, prepending one copy of a, recursing with n=1
-- replicate: n=1, prepending one copy of a, recursing with n=0
-- replicate: n=0, base case, returning Vec.nil
-- Vec.cons (-42) (Vec.cons (-42) (Vec.cons (-42) Vec.nil))

Read the trace bottom-to-top against top-to-bottom: the four dbg_trace lines print in the order each recursive call is entered (n=3, then n=2, then n=1, then the base case n=0), and only once the base case returns does the final #eval line print the fully-built Vec. This is the general shape every structurally-recursive function over Vec/Nat in this book has: one line printed per recursive call, in call order, with the base case’s line printed last before the result appears. a’s own value cannot be printed generically inside the trace: α is an arbitrary type here, and nothing says a Repr α instance (the typeclass that lets a value be turned into displayable text) exists for whichever type α turns out to be at a given call site. This is why the message names the step (which branch fired, what n is) rather than the data — the same reason dbg_trace traces later in this book stick to naming steps and concrete, already-known values, never a still-generic argument.

This example deliberately stores Int values, not Nat values. With a Vec Nat n holding Nat elements, the length n and the stored numbers would both be Nat, and it becomes easy to lose track of which Nat is playing which role. Int keeps the elements visibly numeric — unlike, say, Bool — while still being unmistakably a different type from the length’s Nat: -42 is large and negative, nothing a length ever is, so no reader could mistake it for the 3.

Real or complex numbers would make the distinction just as clear, but are not an option this early. ℝ/ℂ are Mathlib types, and this book stays Mathlib-free through Chapter 11. Lean’s reals in particular are noncomputable (built from Cauchy sequences with no decidable equality), so #eval cannot evaluate one at all, not even in principle. Int is the closest numeric type that is both core Lean and actually computable. The next example, Vec.dot, uses Vec Int n for the same reason.

Look closely at the type (n : Nat) → Vec α n. The n that appears on the left of the arrow (the argument) reappears inside the type on the right of the arrow (the result). Feed Vec.replicate a the number 3, and the result has type Vec α 3, specifically. Feed it 5, and the very same function returns something of type Vec α 5 instead. This is categorically different from double : Nat → Nat, where the output type (Nat) is fixed in advance and never reads the input value at all. Here, the type itself changes based on which number was passed in. That is exactly what “the codomain depends on the argument” means, made as concrete as possible.

Why bother: invariants become part of the type, not a side promise

The payoff is not just bookkeeping. Because the length lives in the type, Lean can rule out a whole class of mistakes before running anything at all. Define a function that reads a vector’s first element, which only makes sense for a non-empty vector:

def Vec.head : Vec α (n + 1) → α
  | Vec.cons a _ => a

The argument type Vec α (n + 1) says, in the type itself, “this only accepts vectors of length at least one” — there is no separate runtime check for emptiness anywhere in this definition, because none is needed. Calling it on an empty vector is rejected before the expression ever runs:

#check Vec.head Vec.nil

error: Application type mismatch: The argument
  Vec.nil
has type
  Vec ?m 0
but is expected to have type
  Vec ?m (?n + 1)
in the application
  Vec.head Vec.nil

Nothing about “index out of range” happens at runtime, because the bad call is not a well-typed term in the first place — the same “ruled out before running” guarantee from Chapter 1, Section 1, now enforced by an invariant (non-emptiness) that an ordinary, non-dependent type could not have expressed at all. List α has no way to say “and this one is non-empty” as part of its type; Vec α (n+1) says exactly that, for free, using only the machinery already on the table.

Return to the Python example from the start of this section. Here is dot, rewritten for Vec instead of Python’s list, with both arguments required to share the same length n:

def Vec.dot : Vec Int n → Vec Int n → Int
  | Vec.nil, Vec.nil => 0
  | Vec.cons x xs, Vec.cons y ys => x * y + Vec.dot xs ys

The signature Vec Int n → Vec Int n → Int uses the same n — a Nat, the length — for both arguments; that is not a naming coincidence, it is the whole point. Elements are Int, not Nat, on purpose: this keeps the length (n, a Nat) and the stored numbers (Int) as visibly different types throughout, with no Nat/Nat overlap left to lose track of. The vectors below are also named vecA/vecB, not after their own lengths, to avoid yet another coincidence layered on top. Try to reproduce Python’s silent bug:

def vecA : Vec Int 3 := Vec.cons 17 (Vec.cons (-3) (Vec.cons 42 Vec.nil))
def vecB : Vec Int 2 := Vec.cons 99 (Vec.cons 8 Vec.nil)

#check Vec.dot vecA vecB

Vec.dot recurses on both arguments at once, consuming one element from each per call, and accumulates a running total on the way back up. Before seeing why the mismatched-length call above fails, watch a same-length call succeed, with a dbg_trace line added to each branch. Unlike Vec.replicate’s trace, this one can also print the actual numbers, since Int (unlike a fully generic α) does have a Repr instance:

def Vec.dot' : Vec Int n → Vec Int n → Int
  | Vec.nil, Vec.nil => dbg_trace s!"dot: both nil, base case, returning 0"; 0
  | Vec.cons x xs, Vec.cons y ys =>
      dbg_trace s!"dot: heads x={x}, y={y}, recursing on the rest";
      x * y + Vec.dot' xs ys

def vecC : Vec Int 3 := Vec.cons 2 (Vec.cons 5 (Vec.cons 1 Vec.nil))

#eval Vec.dot' vecA vecC
-- dot: heads x=17, y=2, recursing on the rest
-- dot: heads x=-3, y=5, recursing on the rest
-- dot: heads x=42, y=1, recursing on the rest
-- dot: both nil, base case, returning 0
-- 61

Each traced line names the pair of heads being multiplied before the recursive call is made, so the four lines above are exactly $17 \times 2$, $-3 \times 5$, $42 \times 1$, and the base case’s $0$, in that order — the same four terms the definition’s recursion adds together, made visible one at a time instead of only appearing as the final sum $34 + (-15) + 42 + 0 = 61$. vecA and vecB have different lengths on purpose, to set up the type-mismatch check next; vecC above is a third vector, the same length as vecA, used only to give Vec.dot' a legal pair to run on.

error: Application type mismatch: The argument
  vecB
has type
  Vec Int 2
but is expected to have type
  Vec Int 3
in the application
  vecA.dot vecB

Where Python’s dot([17,-3,42], [99,8]) silently returned 1659 — a wrong answer with no error at all — Lean’s version does not even compile. The length-mismatch bug is not caught by a clever runtime check added to Vec.dot; there is no such check anywhere in its three-line definition. It is caught because “both arguments have the same length” was stated once, in the type, and Lean enforces every type it is given, automatically, for every call site, without exception.

Lean’s actual, built-in Vector α n is distinct from the toy Vec built here. It is defined differently under the hood, as an Array α paired with a proof that its size equals n, for performance reasons — the same way Nat’s presentation above as Peano’s zero/succ does not reflect how Lean actually stores numbers at runtime (as fast arbitrary-precision integers). The Vec built in this section is the traditional textbook definition, simpler to reason about and the one every type-theory reference uses first, while Lean’s real Vector is engineered for speed. Both are dependent types in exactly the sense described here.

The general pattern: Π-types

Both examples above are instances of one idea. A dependent function type, written with $\Pi$ (“Pi,” for “dependent product”), generalizes the ordinary function-space $A \to B$:

\[\prod_{x : A} B(x)\]

Here $B$ is not itself a type — $B$ is a family of types indexed by $A$, formally a function $B : A \to \mathrm{Type}$ (or into Prop, the type of propositions — a distinct universe of its own, formally named Sort 0 in Chapter 1, Section 5 — as below): for each $x : A$, $B(x)$ is the specific type that family produces at $x$, and different $x$’s may give genuinely different types. Read the whole expression as: “a function that, given any $x : A$, returns a term of type $B(x)$” — a type allowed to mention $x$, because $B$ itself is allowed to vary with $x$. When $B(x)$ does not actually depend on $x$ (i.e. $B$ is a constant family), this collapses exactly to the ordinary function type $A \to B$. Π-types strictly generalize function types; they do not replace them. Vec.replicate’s type above literally is $\prod_{n : \mathtt{Nat}} \mathrm{Vec}\,\alpha\,n$, with Lean’s surface syntax (n : Nat) → Vec α n spelling out the same thing without needing the $\Pi$ symbol.

This is also, not by coincidence, exactly what ∀ means. ∀ n : Nat, n ≥ 0 is a Π-type where $B(n)$ happens to be a proposition (n ≥ 0 : Prop) rather than a data type like Vec α n — “for every n, produce a proof of the n-specific statement n ≥ 0.” Chapter 3 introduces ∀ and propositional logic properly; once it does, every ∀ written from that point on is already a dependent function in exactly this sense, whether or not this vocabulary is available yet when it is first met. Propositions are just the special case where the family $B$ happens to land in Prop instead of Type.

Looking ahead

Chapter 11 builds a genuinely more elaborate dependent type, Path Q : V → V → Type, a family of types indexed by a pair of vertices in a graph rather than by a single Nat — “the type of paths from u to w,” which differs for each choice of endpoints exactly as Vec α n differs for each length. Its cons-like constructor is a dependent function for the same reason Vec.replicate is one here: composing two paths is only accepted by the type-checker when their endpoints actually match, an invariant baked into the type rather than checked separately. Nothing new is needed to understand it once this section’s Fin/Vec examples make sense — it is the identical idea, with a richer index.

Mathematical reading (optional). For readers who already think categorically: an indexed family B : A → Type is exactly a functor out of the discrete category on A — or, thinking of A × A-indexed families as in the Path example above, an assignment of a $\mathrm{Hom}$-set to every pair of objects in a category. A Π-type over such a family is a dependent product; a term of $\sum_{x:A} B(x)$ (Σ-type, next covered formally in Chapter 1, Section 5) is a dependent sum. Both are literal categorical limits/colimits in the appropriate indexed sense, not merely named after them by analogy.

Read more: Chapter 1, Section 5 gives Π-types (and Σ-types) their formal typing rules, with more worked examples, rather than only the walkthrough given here.

References

Full citations in the Bibliography. Formal definitions and verbatim quotes are gathered in Recall, above.

← def, let, implicit arguments Index Next: Terminology →
Try Lean
Lean playground · v1.4.18 ↗