English
A type is a classification of computational values that determines what operations on them are meaningful. In every programming language, values have types — integers, strings, functions, lists. What type theory asks is: what are types, and how far can they go? The answer turns out to be much further than type systems in mainstream programming languages suggest. Types can express not just “this is a list of integers” but “this is a sorted list of integers,” not just “this is a function from integers to integers” but “this is a function that returns a list whose length equals its input.” When types can say this much, the program that satisfies the type is providing a proof that the specification holds. The type checker becomes a proof checker. Writing the program and proving the theorem are the same act.
This insight — that types are propositions and programs are proofs — is the Curry-Howard correspondence, and it is the organizing revelation of type theory. It was not anticipated by the founders of either programming languages or mathematical logic; it emerged slowly from the convergence of two independent traditions and was recognized fully only decades after the mathematical facts that imply it were in place. Type theory is the discipline of working out what follows from this correspondence, both for programming (what can types be used to specify and verify?) and for mathematics (what does computation as proof mean for the foundations of mathematics?).
The subject sits at the convergence point of §3.4 (PLT) and §3.1 (Logic). PLT gave the technical machinery — lambda calculi, operational semantics, type soundness. Logic gave the proof-theoretic framework — natural deduction, sequent calculi, constructive reasoning. Type theory is the discipline that lives at their intersection, taking both seriously. It connects forward to §3.6 (Formal Methods), where the proof assistants that type theory enables are applied to the verification of real software.
Prerequisites: Programming language theory (§3.4) — familiarity with typed lambda calculi, type soundness, and the basic Curry-Howard observation. Logic (§3.1) — natural deduction and sequent calculi. Mathematical maturity for proofs by induction over derivation trees.
From Paradox Resolution to the Foundations of Mathematics
Type theory began as damage control. Bertrand Russell discovered in 1901 that Gottlob Frege’s comprehension principle — the principle that any definable property determines a set — leads to contradiction: the set of all sets that do not contain themselves both does and does not contain itself. Russell’s proposed resolution, in his 1908 paper “Mathematical Logic as Based on the Theory of Types,” was to stratify mathematical objects into a hierarchy of types: individuals at type 0, sets of individuals at type 1, sets of sets at type 2, and so on. An object of type n can only be a member of an object of type n+1, blocking the self-referential construction that produced the paradox. The Principia Mathematica (1910–1913), which Russell wrote with Alfred North Whitehead, attempted to reconstruct mathematics within this type-stratified framework. The result was vast, correct, and nearly unreadable.
Alonzo Church’s simply typed lambda calculus (1940) refined Russell’s ramified type theory into something cleaner. Church’s system had two layers: a typed functional calculus, and a logic for reasoning about it. Types were built from a base type and function types A → B; terms had unique types derivable from their structure; the system was consistent and contained no paradoxes. The simply typed lambda calculus was not designed for programming — it predated stored-program computers — but it established the mathematical architecture that every subsequent type system has inherited: types built from base types and connectives, terms given types by inference rules, and the whole system designed to block paradoxical constructions.
The Curry-Howard correspondence was discovered in two stages, forty years apart, by two people who were working on apparently unrelated problems. Haskell Curry observed in 1934 that the combinators in his combinatory logic corresponded to tautologies of propositional logic: the combinator K (which takes two arguments and returns the first) corresponds to the propositional tautology A → (B → A), and the combinator S (the composition combinator) corresponds to the tautology (A → B → C) → (A → B) → (A → C). This was a curiosity — a formal correspondence between combinators and propositions, with no obvious significance. William Howard, working in 1969 on the proof-theoretic analysis of natural deduction, noticed that the structure of proofs in intuitionistic natural deduction corresponded exactly to the structure of well-typed terms in the simply typed lambda calculus. Proofs were programs; propositions were types; logical connectives corresponded to type constructors; proof normalization corresponded to program evaluation. Howard circulated his observation as an unpublished manuscript; it was published only in 1980, when it was beginning to influence both type theory and proof theory.
The significance of the correspondence, once recognized, was transformative. Intuitionistic logic — the logic in which proofs must be constructive, where a proof of “A or B” must exhibit either a proof of A or a proof of B — had been developed by Brouwer, Heyting, and Kolmogorov primarily for philosophical reasons, as a stricter standard of mathematical evidence. Under Curry-Howard, intuitionistic logic became the logic of computation: a proof is a construction, and the correspondence gives proofs computational content. Classical logic, which admits proof by contradiction and the law of excluded middle, has no direct computational interpretation under Curry-Howard — adding classical logic to a type system collapses the computational content.
Per Martin-Löf, a Swedish logician and philosopher, developed the framework that made Curry-Howard into a foundation for mathematics. His intuitionistic type theory, presented in a series of lectures and papers from 1972 through 1984, extended the simply typed lambda calculus in two fundamental directions. First, dependent types: types that can depend on values, so that the type of a vector can include its length as part of the type, or the return type of a division function can depend on whether the divisor is zero. Second, types as propositions taken seriously as a foundational stance: Martin-Löf’s system was not just a type system with a logical interpretation but an alternative foundation for constructive mathematics, proposing to replace set theory as the basis on which mathematics is done. His type theory included natural numbers, pairs, sums, identity types, and a universe type (a type whose elements are types), arranged to be simultaneously a programming language and a logic.
The practical realization of these ideas came through proof assistants. Thierry Coquand and Gérard Huet, working at INRIA in the early 1980s, developed the Calculus of Constructions — a dependent type theory combining the dependent types of Martin-Löf with the polymorphism of System F. Coq (from Calcul des constructions, French) implemented this calculus beginning in 1984 and developed, over decades of refinement, into the proof assistant that has been used to verify the four-color theorem (Gonthier, 2005), the Feit-Thompson theorem (Gonthier et al., 2012), and the CompCert verified C compiler (Leroy, 2009). Agda, implemented in Gothenburg, took a different design direction: less tactic automation, more direct term-level programming, closer to the experience of writing programs in a dependently typed language. Lean, developed by Leonardo de Moura at Microsoft Research from 2013 (and entirely redesigned as Lean 4 from 2021), combined mathematical logic with programming language design and produced a proof assistant that has attracted a large community of mathematicians.
The contemporary turning point was Vladimir Voevodsky’s univalent foundations program, announced around 2006 and crystallized in the Institute for Advanced Study’s special year on Univalent Foundations in 2012-2013. Voevodsky, a Fields Medal winner in algebraic geometry, had become convinced that mathematics needed mechanically checked proofs and that the existing proof assistants were inadequate. His contribution was the univalence axiom: an axiom for Martin-Löf type theory asserting that equivalent types are equal. This axiom, added to Martin-Löf type theory, produces homotopy type theory (HoTT) — a type theory in which types behave like spaces (in the homotopy-theoretic sense), type equality is homotopy equivalence, and the identity type of a type has a rich higher-dimensional structure. The HoTT Book, a collaborative effort produced by the special year’s participants and published in 2013, presented this framework comprehensively. The subsequent development of cubical type theory (Cohen, Coquand, Huber, Mörtberg, 2016) provided a computational interpretation of univalence that the original HoTT lacked, making the axiom consistent with the constructive character of type theory.
The practical significance of Lean and its accompanying mathlib library has become clear over the last five years. The Liquid Tensor Experiment, initiated by Peter Scholze (another Fields Medal winner) in late 2020, challenged the formalization community to mechanically verify a difficult recent theorem from his work on condensed mathematics. The experiment was completed in June 2022 — a research-level result formalized in Lean in under two years. The episode demonstrated that contemporary pure mathematics at the frontier, not just foundational or computational mathematics, could be mechanically verified. The mathematical community’s response has included a significant increase in mathematicians learning Lean, a growth in the mathlib library’s coverage, and a genuine open question about whether mechanized proof will become a standard part of mathematical practice.
The Propositions-as-Types Correspondence and Its Depth
What Curry-Howard Actually Says
The Curry-Howard correspondence is not a single theorem but a family of correspondences, each connecting a logical system to a type system. The simplest instance connects intuitionistic propositional logic to the simply typed lambda calculus:
- Propositions correspond to types
- Proofs correspond to terms
- Logical connectives correspond to type constructors
- Proof normalization corresponds to term reduction (beta-eta reduction)
In detail: the conjunction A ∧ B corresponds to the product type A × B (a pair whose first component has type A and second has type B). A proof of A ∧ B is a pair of proofs — exactly a term of type A × B. The disjunction A ∨ B corresponds to the sum type A + B (a tagged union). A proof of A ∨ B is either a proof of A (left injection) or a proof of B (right injection) — exactly a term of type A + B. Implication A → B corresponds to the function type A → B. A proof of A → B is a function that takes a proof of A and returns a proof of B — exactly a term of type A → B. The empty type ⊥ corresponds to the proposition False; there is no term of the empty type, and no proof of False.
The correspondence extends to quantifiers under dependent types. Universal quantification ∀(x : A). B(x) corresponds to the dependent function type Π(x : A). B(x): a proof of ∀(x : A). B(x) is a function that, given any element a of type A, produces a proof of B(a). Existential quantification ∃(x : A). B(x) corresponds to the dependent pair type Σ(x : A). B(x): a proof of ∃(x : A). B(x) is a pair of an element a and a proof that B(a) holds.
The identity type Id_A(a, b) — the type of proofs that a equals b — is where the correspondence reveals its deepest content. In homotopy type theory, the identity type is not just “is there a proof that a = b” but “what are all the ways that a = b?” — a type whose elements are proofs of equality, whose elements of elements are proofs that those proofs are equal, and so on through all dimensions. This higher-dimensional structure is what connects type theory to algebraic topology and what makes homotopy type theory a genuine synthesis of type theory and topology.
Dependent Types as a Specification Language
Dependent types allow types to express specifications that simple types cannot. A vector of length n has type Vec A n where n is an ordinary value. A function that appends two vectors has type (m n : Nat) → Vec A m → Vec A n → Vec A (m + n) — the type specifies that the output length equals the sum of the input lengths. Any term of this type, if it type-checks, provably satisfies this specification; the type checker’s verification is a proof that the function is correct.
The expressiveness scales. A sort function can have type (xs : List A) → Σ(ys : List A). Sorted ys × Permutation xs ys — the return type is a dependent pair of a list and a proof that it is sorted and a permutation of the input. A divide function can have type (a b : Int) → b ≠ 0 → Int — the type requires a proof that the divisor is nonzero. A parser can have type (input : String) → Either ParseError (Σ(result : AST). parse input = Success result) — the type couples the parsed result to a proof that parsing succeeded.
The cost is elaboration: writing programs at this level requires providing explicit proofs alongside values, which increases the verbosity of code. In Lean and Agda, proof obligations can often be discharged automatically by tactics, reducing the burden significantly. In Idris, a language designed for type-driven development, the interactive proof process is integrated into the editor, with the system generating proof obligations and accepting tactic scripts to discharge them.
The spectrum of type theories trades expressiveness for decidability. Simple types have decidable type-checking and inference; they can only express structural properties. System F (polymorphic types) has decidable type-checking but undecidable type inference in general; it can express abstract properties via universally quantified types. Dependent types have undecidable type-checking in the most general case; most practical systems impose restrictions (no type-level computation involving general recursion) that recover decidability. The Martin-Löf type theories and the Calculus of Constructions are the standard decidable dependent type theories used in proof assistants.
Constructivity and Its Consequences
Type theory is fundamentally constructive: every proof is a construction, and the existence of a mathematical object must be demonstrated by exhibiting it. This distinguishes type theory from classical mathematics, which accepts proof by contradiction (showing that the negation of a claim leads to a contradiction, without constructing what the claim asserts) and the axiom of choice (asserting that choice functions exist without constructing them).
The consequence is that classical results — the law of excluded middle (every proposition is either true or false), double negation elimination (¬¬A implies A), the axiom of choice — are not provable in basic type theory. They can be added as axioms, and adding them is common in practice (Lean’s mathlib uses classical logic; Agda allows postulating excluded middle), but adding them sacrifices the computational content of proofs. Under Curry-Howard, a proof of A ∨ ¬A should be a program that, given any A, decides whether A holds or not — which is not in general computable.
The constructivity constraint is sometimes experienced as a limitation but is better understood as a different kind of information. A constructive proof of “there exists an x such that P(x)” provides an x and a proof that P(x) holds — this is a program that computes a witness. A classical proof provides only the existence, not the witness. The computational content of constructive proofs is what makes them executable in proof assistants, what connects them to program extraction (automatically deriving verified programs from proofs), and what makes the Curry-Howard correspondence work.
What Studying This Changes
Type theory produces cognitive shifts that are not available from any other CS subject.
The first shift is the unification of programming and proving. A practitioner who has internalized the Curry-Howard correspondence sees writing a program and constructing a mathematical proof as the same activity in different clothing. When they write a function, they are defining an element of a type; when they prove a theorem, they are constructing a term. This dual vision changes how both activities are approached: programs are written with their proof-theoretic structure in mind, and proofs are constructed with their computational content visible. Practitioners who hold this view consistently produce code that is more transparently correct and arguments that are more computationally illuminating.
The second shift is access to the proof assistant ecosystem. Coq, Lean, Agda, and Isabelle are the most powerful tools for establishing the correctness of mathematical and computational artifacts, and using them beyond the tutorial level requires understanding the type theory they implement. A practitioner who has studied Martin-Löf type theory can navigate the Lean proof assistant and read the mathlib library; one who has not is limited to copying patterns from tutorials. The proof assistant ecosystem is growing rapidly, and its importance to high-assurance software and to mathematical research is growing with it.
The third shift is the ability to express specifications as types. When a programmer knows only simple types, specifications live in documentation — comments, README files, unit tests. When they know dependent types, specifications can be expressed in the type system, enforced by the type checker, and impossible to violate without a type error. This is not a marginal improvement but a qualitative change in the relationship between code and its correctness argument. The cost is verbosity and the need to prove things that would be obvious informally; the benefit is that the correctness argument is in the code and machine-checked.
The fourth shift is the understanding of the foundations of mathematics. Most mathematicians and computer scientists treat set theory as the implicit foundation of mathematics, rarely examining what that means. Studying type theory reveals that the choice of foundation is a real choice with real consequences: type-theoretic mathematics is constructive, computational, and organized around the program-proof correspondence; set-theoretic mathematics is classical, non-computational (in the sense that it does not automatically extract programs from proofs), and organized around membership. The comparison makes visible what is implicit in standard mathematical practice and provides a genuine alternative.
Resources
Books and Texts
Pierce’s Types and Programming Languages (TAPL, MIT Press, 2002) is the right first book for most readers. It develops the typed lambda calculi from scratch — simply typed lambda calculus, subtyping, recursive types, System F — with proofs of type soundness for each system, and ends with a brief sketch of dependent types that motivates the rest of the subject. TAPL is demanding but pedagogically generous, and the first encounter with Curry-Howard (stated in the final chapters) lands with appropriate force because the machinery to understand it has been built. Pierce’s companion Advanced Topics in Types and Programming Languages (ATTAPL, MIT Press, 2005) extends TAPL into dependent types, linear types, effect systems, and typed assembly language.
Martin-Löf’s Intuitionistic Type Theory (the Padua lecture notes, 1980, free online in various scans) is the primary source for the type theory that underlies all serious proof assistants. It is dense and brief (around 100 pages), written in the idiom of philosophical logic, and entirely different from a programming language theory paper. Reading it is demanding and essential: the four judgments (A is a type, A and B are equal types, a is of type A, a and b are equal of type A) and the four kinds of inference rules that Martin-Löf introduces are the conceptual core of everything that follows. No secondary account fully substitutes for it.
The Homotopy Type Theory Book (HoTT Book, 2013, free at homotopytypetheory.org) is the collaborative presentation of homotopy type theory produced by the IAS special year. It covers Martin-Löf type theory, homotopy-theoretic interpretation, the univalence axiom, and substantial developments in synthetic homotopy theory. It is mathematically demanding — assumes comfort with abstract algebra and some topology — but is the right reference for the contemporary frontier of type theory. Reading the introduction and the first two chapters is accessible to readers with solid PLT background; the later chapters require more.
For hands-on proof assistant engagement, the best structured paths are:
- Software Foundations (Pierce et al., free at softwarefoundations.cis.upenn.edu) in Coq — the industry standard for learning PLT and type theory through mechanical proof. Volume 1 teaches Coq and logic; Volume 2 formalizes operational semantics, type soundness, and Hoare logic.
- Programming Language Foundations in Agda (Wadler, Kokke, Siek, free at plfa.inf.ed.ac.uk) — covers the same PLT content as Software Foundations but in Agda, which is more directly a dependently typed programming language. Preferred by readers who find Agda’s programming style more natural.
- Theorem Proving in Lean 4 (de Moura, Ullrich, free at lean-lang.org) and Mathematics in Lean (Avigad, Massot, free at leanprover-community.github.io/mathematics_in_lean) — the primary resources for the Lean proof assistant. Lean 4 has become the most active platform for mathematical formalization.
For dependent types as a programming methodology, Brady’s Type-Driven Development with Idris (Manning, 2017, paid) is the standard text. Idris is a language designed for type-driven development — the practice of using types as specifications and letting the type-checker drive the implementation. The book is accessible and practical, the right introduction to dependent types for programmers who want to use them rather than study them foundationally. Friedman and Christiansen’s The Little Typer (MIT Press, paid) is a gentler conceptual entry to dependent types, written in the Little Schemer style. It is not rigorous enough to replace TAPL, Martin-Löf, or PLFA, but it lowers the barrier to the core intuition that types can describe programs and proofs.
Nordström, Petersson, and Smith’s Programming in Martin-Löf’s Type Theory (1990, free online) is the systematic textbook presentation of Martin-Löf type theory. It is less demanding than the original lecture notes and more systematic; the right companion to the Padua notes for learners who want a structured presentation.
| Book | Role | Type |
|---|---|---|
| Type-theory chapters in Pierce, Types and Programming Languages (TAPL) | Entry to typed lambda calculi and Curry-Howard | Entry |
| Advanced type-system chapters in ATTAPL | Dependent types, effects, linear types | Depth |
| Martin-Löf, Intuitionistic Type Theory (Padua notes, free) | Primary source for dependent type theory | Depth |
| The HoTT Book (free) | Homotopy type theory; contemporary frontier | Depth |
| Type-theory track in Software Foundations Vols. 1-2 (free) | Mechanized PLT and type theory in Coq | Practice |
| Wadler et al., Programming Language Foundations in Agda (free) | Mechanized PLT in Agda | Practice |
| de Moura et al., Theorem Proving in Lean 4 (free) | Lean 4 tutorial | Practice |
| Avigad & Massot, Mathematics in Lean (free) | Mathematical formalization in Lean | Practice |
| Brady, Type-Driven Development with Idris (paid) | Dependent types as programming methodology | Depth |
| Friedman & Christiansen, The Little Typer (paid) | Gentle dependent-types intuition | Auxiliary |
| Nordström, Petersson & Smith, Programming in Martin-Löf’s Type Theory (free) | Systematic Martin-Löf type theory | Depth |
| Type-theoretic foundations in Harper, PFPL (draft free) | Broader PLT with type-theoretic grounding | Depth |
| Dependent-type verification in Chlipala, Certified Programming with Dependent Types (free) | Coq-based verified software development | Depth |
Courses and Lectures
Oregon Programming Languages Summer School (OPLSS) archives all lectures freely on YouTube. The type theory content is consistently excellent: Frank Pfenning’s lectures on proof theory and logical frameworks, Robert Harper’s lectures on type theory, Stephanie Weirich’s lectures on type inference. Working through OPLSS lectures systematically provides a graduate-level survey of the subject.
Carnegie Mellon 15-317 (Constructive Logic, Harper) and 15-312 (Principles of Programming Languages) course materials, freely available, are among the best structured courses on type theory from a programming language perspective. Harper’s lecture notes for 15-317 in particular develop the Curry-Howard correspondence with unusual precision.
The Lean 4 community at leanprover-community.github.io maintains extensive tutorials, the Zulip chat, and structured learning paths for both programming and mathematical formalization. The community is unusually welcoming for a research-oriented mathematical tool.
Agda community resources at agda.readthedocs.io and through the PLFA book provide structured learning paths. The Agda Zulip is also active.
| Course | Platform | Type |
|---|---|---|
| OPLSS lectures — Pfenning, Harper, Weirich (free) | YouTube / OPLSS site | Reference |
| CMU 15-317 Constructive Logic (Harper, free) | CMU course site | Entry |
| Type-theory sequence in CMU 15-312 Principles of PL (Harper, free) | CMU course site | Depth |
| Lean 4 community tutorials (free) | leanprover-community.github.io | Practice |
Practice, Tools, and Current Sources
Working in a proof assistant is the primary engagement with the material. There is no visualization of type theory that substitutes for the experience of constructing a proof in Coq or Lean and having the system accept it — or reject it with an error message that forces re-examination of the proof’s structure. The tools listed below are the tools; use them.
Lean 4 with mathlib is currently the most active platform. Install via elan (the Lean version manager) and work through the first half of Mathematics in Lean. The mathlib4 repository at github.com/leanprover-community/mathlib4 is itself a learning resource — reading source proofs for results you already know demonstrates what Lean proof style looks like.
Agda with PLFA: install Agda through GHCup or Nix, work through the first part of the PLFA book. The structured exercises are graded in difficulty and provide immediate feedback.
Coq with Software Foundations: install through opam, work through Volume 2 (Programming Language Foundations). The PLT-specific content — operational semantics, type soundness, Hoare logic — is the most directly connected to §3.4.
Proof General (Emacs) or VSCoq (VS Code) provide interactive proof development interfaces where the proof state is visible after each tactic — essential for understanding what is happening during proof construction.
| Resource | Platform | Type |
|---|---|---|
| Lean 4 + mathlib (free) | elan / github.com/leanprover | Practice |
| Agda + PLFA (free) | agda.readthedocs.io | Practice |
| Coq + Software Foundations (free) | coq.inria.fr / softwarefoundations.cis.upenn.edu | Practice |
| Lean Zulip (free) | leanprover.zulipchat.com | Reference |
| mathlib4 source (free) | github.com/leanprover-community/mathlib4 | Reference |
Traps
| Trap | Why it misleads | Better response |
|---|---|---|
| Approaching type theory through language features rather than the correspondence | Many practitioners encounter type theory through generics, type inference, or algebraic data types in their primary language. This produces a fragmented view: type theory appears as a collection of features rather than as a coherent discipline organized around the propositions-as-types correspondence. The correspondence is not one fact among many; it is the organizing principle from which everything else follows. | Read TAPL sequentially rather than jumping to features. The development from the simply typed lambda calculus through System F to dependent types follows the logical structure of the correspondence, and reading in this order makes the correspondence’s increasing depth visible. |
| Staying in proof assistants without reading the theory | Proof assistants are powerful learning tools, but fluency in Lean or Coq without understanding Martin-Löf type theory produces proof engineering skill without type-theoretic understanding. The proof assistant’s error messages and behavior become interpretable only with the underlying type theory in view. | Alternate between reading the theory (Martin-Löf’s notes, TAPL’s type-theoretic chapters) and working in the proof assistant. After each theoretical concept, formalize a small example in the assistant; after each assistant exercise, read what theoretical result it corresponds to. |
| Attempting dependent types before mastering simple types | Dependent types require facility with ordinary typed lambda calculi, the Curry-Howard correspondence, and proof by induction over derivation trees. Learners who skip to dependent types encounter all of these prerequisites simultaneously and in their hardest form. | Work through TAPL Chapters 1–23 before engaging with dependent types. The simply typed calculus, System F, and the type reconstruction algorithm are prerequisites, not optional. Rushing to dependency produces confusion about which difficulties are fundamental to type theory and which are artifacts of insufficient preparation. |
| Treating constructivity as a limitation | Classical logic is more familiar and admits shorter proofs for some results. Learners who approach type theory as “logic with unnecessary restrictions” miss the point: constructivity is not a restriction but a different kind of information. A constructive proof is a program; a classical proof is not. | Study specific examples where constructive and classical proofs diverge. The intermediate value theorem, the well-ordering principle, and the Bolzano-Weierstrass theorem all have classical proofs that are non-constructive and constructive versions that extract algorithms. Understanding the difference — and what the constructive version provides that the classical does not — is the key to valuing constructivity rather than resisting it. |
| Expecting immediate practical payoff | Type theory’s industrial applications, while growing rapidly, are still concentrated in specialized domains: verified compilers, proof assistants, high-assurance systems. Most programmers will not use dependent types in their daily work for years. Learners who approach type theory expecting immediate applicable skills are disappointed by the distance between the theory and current mainstream practice. | Frame the investment correctly: type theory is a long-term cognitive investment, not a short-term skills acquisition. The understanding it provides — of what types can express, of why programming and proving are the same, of how to reason about programs with formal precision — pays off over careers, not quarters. The tools are improving rapidly; today’s advanced research applications are tomorrow’s language features. |
| Skipping the Curry-Howard correspondence itself | Some learners work through TAPL’s type-soundness proofs, some learn Coq tactics, some study Martin-Löf type theory — and never pause to see the Curry-Howard correspondence as the single organizing insight that connects all of these. The result is accumulated technique without synthesis. | At some point during the study — ideally after completing TAPL’s core and before engaging with dependent types — stop and state the Curry-Howard correspondence explicitly for each logical connective and its corresponding type. Write the correspondence out. Prove a simple logical tautology as both a proof and a program. The synthesis moment, when it occurs, reorganizes everything that preceded it. |
中文
类型是对计算值的分类，它决定了哪些操作对这些值有意义。在每一种编程语言中，值都有类型——整数、字符串、函数、列表。类型论追问的是：类型 是什么，以及类型能走多远？答案远远超出主流编程语言中的类型系统给人的印象。类型不仅可以表达“这是一个整数列表”，还可以表达“这是一个已排序的整数列表”；不仅可以表达“这是一个从整数到整数的函数”，还可以表达“这是一个返回列表的函数，而该列表长度等于它的输入”。当类型能表达这么多时，满足该类型的程序就在提供一个证明：规约成立。类型检查器变成证明检查器。写程序和证明定理成为同一个动作。
这一洞见——类型是命题，程序是证明——就是 Curry-Howard 对应，也是类型论的组织性启示。它并不是编程语言或数理逻辑的奠基者预先料到的；它是两个独立传统逐渐汇合之后才浮现出来的，而且是在蕴含它的数学事实已经存在数十年后，才被充分认识。类型论就是展开这个对应所带来后果的学科，既面向编程——类型可以用来规定和验证什么？也面向数学——把计算视为证明，对数学基础意味着什么？
这个主题位于 §3.4（PLT）和 §3.1（逻辑）的交汇处。PLT 提供技术机器——λ 演算、操作语义、类型可靠性。逻辑提供证明论框架——自然演绎、相继式演算、构造性推理。类型论就是存在于二者交叉处的学科，并且认真对待二者。它向前连接到 §3.6（形式化方法），在那里，由类型论支持的证明助手被应用于真实软件的验证。
前置知识：编程语言理论（§3.4）——熟悉类型化 λ 演算、类型可靠性，以及基本 Curry-Howard 观察。逻辑（§3.1）——自然演绎和相继式演算。用于对推导树做归纳证明的数学成熟度。
从解决悖论到数学基础
类型论最初是一种损害控制。Bertrand Russell 在 1901 年发现，Gottlob Frege 的概括原则——任何可定义性质都决定一个集合——会导致矛盾：所有不包含自身的集合所组成的集合，既包含自身又不包含自身。Russell 在 1908 年的论文 “Mathematical Logic as Based on the Theory of Types” 中提出的解决方案，是把数学对象分层为一个类型层级：个体位于类型 0，个体的集合位于类型 1，集合的集合位于类型 2，如此继续。类型 n 的对象只能成为类型 n+1 对象的成员，从而阻止产生悖论的自指构造。Russell 与 Alfred North Whitehead 合写的 Principia Mathematica（1910–1913）试图在这个类型分层框架中重建数学。结果庞大、正确，并且几乎不可读。
Alonzo Church 的简单类型 λ 演算（1940）把 Russell 的分支类型论精炼成更干净的形式。Church 的系统有两层：一个类型化函数演算，以及一个用于推理它的逻辑。类型由基类型和函数类型 A → B 构成；项具有由其结构推导出的唯一类型；系统一致，并且不含悖论。简单类型 λ 演算并不是为编程而设计的——它早于存储程序计算机——但它确立了后来每一个类型系统都继承的数学架构：类型由基类型和连接词构造，项通过推理规则获得类型，整个系统被设计用来阻止悖论性构造。
Curry-Howard 对应是由两个人在相隔四十年的两个阶段中发现的；他们当时处理的似乎是彼此无关的问题。Haskell Curry 在 1934 年观察到，他的组合逻辑中的组合子对应命题逻辑中的重言式：组合子 K（接受两个参数并返回第一个）对应命题重言式 A → (B → A)，组合子 S（组合组合子）对应重言式 (A → B → C) → (A → B) → (A → C)。这当时只是一个奇异现象——组合子和命题之间的一种形式对应，没有明显意义。William Howard 在 1969 年研究自然演绎的证明论分析时注意到，直觉主义自然演绎中的证明结构，恰好对应简单类型 λ 演算中的良类型项结构。证明就是程序；命题就是类型；逻辑连接词对应类型构造子；证明规范化对应程序求值。Howard 将这一观察作为未发表手稿流传；它直到 1980 年才出版，而那时它已经开始影响类型论和证明论。
一旦这一对应的重要性被认识到，它就具有变革性。直觉主义逻辑——一种要求证明必须是构造性的逻辑，其中 “A 或 B” 的证明必须展示 A 的证明或 B 的证明——原本主要由 Brouwer、Heyting 和 Kolmogorov 出于哲学理由发展出来，作为一种更严格的数学证据标准。在 Curry-Howard 之下，直觉主义逻辑变成了计算的逻辑：证明是一种构造，而这种对应赋予证明以计算内容。经典逻辑允许反证法和排中律，因此在 Curry-Howard 下没有直接的计算解释——把经典逻辑加入类型系统，会使计算内容坍缩。
瑞典逻辑学家和哲学家 Per Martin-Löf 发展了把 Curry-Howard 变成数学基础的框架。他的直觉主义类型论在 1972 年到 1984 年间通过一系列讲座和论文提出，并在两个根本方向上扩展了简单类型 λ 演算。第一，是依赖类型：类型可以依赖值，因此一个向量的类型可以把它的长度作为类型的一部分，或者除法函数的返回类型可以依赖除数是否为零。第二，是认真把类型作为命题，并把它当成一种基础立场：Martin-Löf 的系统不只是带有逻辑解释的类型系统，而是构造性数学的另一种基础，试图替代集合论成为数学实践的基础。他的类型论包括自然数、积、和、恒等类型，以及 universe type（其元素本身为类型的类型），并被安排成同时作为编程语言和逻辑。
这些思想的实践实现来自证明助手。Thierry Coquand 和 Gérard Huet 于 1980 年代初在 INRIA 工作时发展了构造演算——一种结合 Martin-Löf 依赖类型和 System F 多态性的依赖类型论。Coq（来自法语 Calcul des constructions）从 1984 年开始实现这一演算，并在数十年改进中发展为一套证明助手，用于验证四色定理（Gonthier，2005）、Feit-Thompson 定理（Gonthier 等，2012）以及 CompCert 验证 C 编译器（Leroy，2009）。Agda 在 Gothenburg 实现，采取了不同设计方向：较少依赖 tactic 自动化，更多直接在项层面编程，更接近用依赖类型语言写程序的体验。Lean 由 Leonardo de Moura 于 2013 年起在 Microsoft Research 开发，并在 2021 年起作为 Lean 4 完全重新设计；它结合数理逻辑与编程语言设计，形成了一套吸引大量数学家参与的证明助手。
当代转折点是 Vladimir Voevodsky 的单价基础纲领，大约在 2006 年提出，并在 Institute for Advanced Study 2012–2013 年关于 Univalent Foundations 的特别年度中定型。Voevodsky 是代数几何中的 Fields Medal 获得者，他逐渐相信数学需要机械检查证明，而且现有证明助手并不充分。他的贡献是单价公理：一个用于 Martin-Löf 类型论的公理，断言等价类型就是相等类型。把这一公理加入 Martin-Löf 类型论，就产生了同伦类型论（HoTT）——一种类型论，其中类型表现得像空间（在同伦论意义上），类型相等性就是同伦等价，而一个类型的恒等类型具有丰富的高维结构。HoTT Book 是该特别年度参与者协作完成并于 2013 年出版的作品，系统呈现了这一框架。随后发展出的 cubical type theory（Cohen、Coquand、Huber、Mörtberg，2016）为单价性提供了原始 HoTT 所缺乏的计算解释，使该公理与类型论的构造性特征一致。
Lean 及其配套 mathlib 库的实践意义，在过去五年中已经变得清楚。Liquid Tensor Experiment 由 Peter Scholze（另一位 Fields Medal 获得者）于 2020 年末发起，向形式化共同体提出挑战：机械验证他在 condensed mathematics 工作中的一个困难新近定理。该实验于 2022 年 6 月完成——一个研究级结果在不到两年内被 Lean 形式化。这个事件展示出，当代前沿纯数学，而不只是基础数学或计算数学，也可以被机械验证。数学共同体的回应包括：学习 Lean 的数学家显著增加，mathlib 库覆盖范围增长，以及一个真正开放的问题：机制化证明是否会成为数学实践的标准组成部分。
命题即类型对应及其深度
Curry-Howard 实际上说了什么
Curry-Howard 对应不是一个单一定理，而是一族对应，每一种都把某个逻辑系统连接到某个类型系统。最简单的实例，把直觉主义命题逻辑连接到简单类型 λ 演算：
- 命题对应类型
- 证明对应项
- 逻辑连接词对应类型构造子
- 证明规范化对应项归约（beta-eta 归约）
具体说：合取 A ∧ B 对应积类型 A × B，也就是一个二元组，其第一分量具有类型 A，第二分量具有类型 B。A ∧ B 的证明是一对证明——这正是类型 A × B 的项。析取 A ∨ B 对应和类型 A + B，也就是带标签的联合。A ∨ B 的证明要么是 A 的证明（左注入），要么是 B 的证明（右注入）——这正是类型 A + B 的项。蕴含 A → B 对应函数类型 A → B。A → B 的证明是一个函数，它接受 A 的证明并返回 B 的证明——这正是类型 A → B 的项。空类型 ⊥ 对应命题 False；空类型没有项，False 没有证明。
在依赖类型下，这种对应扩展到量词。全称量化 ∀(x : A). B(x) 对应依赖函数类型 Π(x : A). B(x)：∀(x : A). B(x) 的证明是一个函数，它给定任意类型 A 的元素 a，都产生 B(a) 的证明。存在量化 ∃(x : A). B(x) 对应依赖对类型 Σ(x : A). B(x)：∃(x : A). B(x) 的证明是一对东西，一个元素 a，以及 B(a) 成立的证明。
恒等类型 Id_A(a, b)——也就是 a 等于 b 的证明类型——是这个对应揭示最深内容的地方。在同伦类型论中，恒等类型不只是“是否有 a = b 的证明”，而是“a = b 有哪些所有方式？”——它是一个类型，其元素是相等性的证明；其元素的元素是这些证明彼此相等的证明；如此延展到所有维度。这个高维结构正是类型论连接到代数拓扑的地方，也使同伦类型论成为类型论与拓扑学的真正综合。
依赖类型作为规约语言
依赖类型允许类型表达简单类型无法表达的规约。长度为 n 的向量具有类型 Vec A n，其中 n 是一个普通值。连接两个向量的函数可以具有类型 (m n : Nat) → Vec A m → Vec A n → Vec A (m + n)——这个类型规定了输出长度等于输入长度之和。任何具有这个类型的项，只要通过类型检查，就可证明满足这一规约；类型检查器的验证就是函数正确性的证明。
这种表达力可以继续扩展。排序函数可以具有类型 (xs : List A) → Σ(ys : List A). Sorted ys × Permutation xs ys——返回类型是一个依赖对，由一个列表和一个证明构成，证明该列表已排序且是输入的一个排列。除法函数可以具有类型 (a b : Int) → b ≠ 0 → Int——这个类型要求提供除数非零的证明。解析器可以具有类型 (input : String) → Either ParseError (Σ(result : AST). parse input = Success result)——这个类型把解析结果与“解析成功”的证明绑定起来。
代价是 elaboration：在这个层级写程序，需要在值旁边提供显式证明，这会增加代码冗长度。在 Lean 和 Agda 中，证明义务常常可以由 tactics 自动完成，从而显著减轻负担。在 Idris 这种为类型驱动开发设计的语言中，交互式证明过程集成进编辑器，系统会生成证明义务，并接受 tactic 脚本来完成它们。
类型论谱系在表达力和可判定性之间进行取舍。简单类型具有可判定的类型检查和类型推断；它们只能表达结构性质。System F（多态类型）具有可判定类型检查，但一般情况下类型推断不可判定；它可以通过全称量化类型表达抽象性质。依赖类型在最一般情况下具有不可判定的类型检查；多数实践系统会施加限制，例如禁止涉及一般递归的类型层级计算，从而恢复可判定性。Martin-Löf 类型论和构造演算，是证明助手中使用的标准可判定依赖类型论。
构造性及其后果
类型论从根本上是构造性的：每个证明都是一个构造，数学对象的存在必须通过展示该对象来证明。这使类型论区别于经典数学，后者接受反证法——证明一个命题的否定会导致矛盾，而无需构造该命题所断言的东西——也接受选择公理——断言选择函数存在，而无需构造它们。
其后果是，经典结果——排中律（每个命题要么为真，要么为假）、双重否定消去（¬¬A 蕴含 A）、选择公理——在基础类型论中不可证明。它们可以作为公理添加进去，而实践中经常这样做（Lean 的 mathlib 使用经典逻辑；Agda 允许假设排中律），但添加它们会牺牲证明的计算内容。在 Curry-Howard 下，A ∨ ¬A 的证明应当是一个程序，它给定任意 A，都能判断 A 是否成立——而这一般并不可计算。
构造性约束有时会被体验为一种限制，但更好的理解是：它提供的是另一种信息。“存在一个 x 使得 P(x)” 的构造性证明，会提供一个 x 以及 P(x) 成立的证明——这是一个能够计算 witness 的程序。经典证明只提供存在性，而不提供 witness。构造性证明的计算内容，使它们能够在证明助手中执行，使它们连接到 program extraction（从证明中自动导出已验证程序），也使 Curry-Howard 对应成立。
学习这个主题会改变什么
类型论会产生其他 CS 主题无法提供的认知转变。
第一种转变，是统一编程与证明。内化 Curry-Howard 对应的实践者，会把写程序和构造数学证明看作穿着不同外衣的同一个活动。当他们写函数时，他们是在定义某个类型的元素；当他们证明定理时，他们是在构造一个项。这种双重视野会改变两种活动的方式：程序会带着证明论结构来写，证明会带着可见的计算内容来构造。稳定持有这种视角的实践者，通常会产出正确性更透明的代码，以及计算含义更清楚的论证。
第二种转变，是进入证明助手生态。Coq、Lean、Agda 和 Isabelle 是确立数学与计算产物正确性的最强工具；要在教程层级之外使用它们，就需要理解它们实现的类型论。学习过 Martin-Löf 类型论的实践者，可以导航 Lean 证明助手并阅读 mathlib 库；没有这种基础的人，则只能从教程中复制模式。证明助手生态正在快速增长，其对高保障软件和数学研究的重要性也随之增长。
第三种转变，是能够把规约表达为类型。当程序员只知道简单类型时，规约存在于文档中——注释、README 文件、单元测试。当他们知道依赖类型时，规约可以在类型系统中表达，由类型检查器强制，并且不可能在没有类型错误的情况下被违反。这不是边际改进，而是代码与其正确性论证之间关系的质变。代价是冗长，以及需要证明一些在非形式层面显而易见的东西；收益是正确性论证存在于代码中，并由机器检查。
第四种转变，是理解数学基础。多数数学家和计算机科学家把集合论当作数学的隐含基础，很少审视这意味着什么。学习类型论会揭示，基础选择是真实选择，并且有真实后果：类型论数学是构造性的、计算性的，并围绕程序—证明对应组织；集合论数学是经典的、非计算性的——在证明不会自动抽取程序的意义上——并围绕成员关系组织。比较二者，会让标准数学实践中的隐含前提变得可见，并提供一个真正替代方案。
资源
书籍与文本
Pierce 的 Types and Programming Languages（TAPL，MIT Press，2002）是多数读者的正确第一本书。它从零开始发展类型化 λ 演算——简单类型 λ 演算、子类型、递归类型、System F——并为每个系统证明类型可靠性，最后用一段简短的依赖类型概述引出本主题余下内容。TAPL 要求较高，但教学上很慷慨；在最后几章陈述 Curry-Howard 时，因为理解它所需的机器已经被搭建起来，所以这一遭遇会产生合适的力量。Pierce 的配套书 Advanced Topics in Types and Programming Languages（ATTAPL，MIT Press，2005）则把 TAPL 扩展到依赖类型、线性类型、效应系统和类型化汇编语言。
Martin-Löf 的 Intuitionistic Type Theory（Padua lecture notes，1980，可在网上找到多种免费扫描版）是支撑所有严肃证明助手的类型论的一手来源。它密集而简短，大约 100 页，以哲学逻辑习语写成，并且完全不同于编程语言理论论文。阅读它要求很高，也很必要：Martin-Löf 引入的四种判断（A 是类型，A 与 B 是相等类型，a 具有类型 A，a 与 b 是类型 A 中的相等元素）以及四类推理规则，是后续一切的概念核心。没有任何二手说明能够完全替代它。
Homotopy Type Theory Book（HoTT Book，2013，可在 homotopytypetheory.org 免费获取）是 IAS 特别年度产生的同伦类型论协作呈现。它覆盖 Martin-Löf 类型论、同伦论解释、单价公理，以及 synthetic homotopy theory 中的大量发展。它数学要求较高——预设读者熟悉抽象代数和部分拓扑学——但它是当代类型论前沿的正确参考。对拥有扎实 PLT 背景的读者而言，导论和前两章可以进入；后续章节要求更高。
对于 证明助手的动手学习，最佳结构化路径是：
- Software Foundations（Pierce 等，softwarefoundations.cis.upenn.edu 免费），使用 Coq——它是通过机械证明学习 PLT 和类型论的业界标准。第一卷教授 Coq 和逻辑；第二卷形式化操作语义、类型可靠性和 Hoare logic。
- Programming Language Foundations in Agda（Wadler、Kokke、Siek，plfa.inf.ed.ac.uk 免费）——覆盖与 Software Foundations 相同的 PLT 内容，但使用 Agda；Agda 更直接是一门依赖类型编程语言。适合那些觉得 Agda 编程风格更自然的读者。
- Theorem Proving in Lean 4（de Moura、Ullrich，lean-lang.org 免费）和 Mathematics in Lean（Avigad、Massot，leanprover-community.github.io/mathematics_in_lean 免费）——这是 Lean 证明助手的主要资源。Lean 4 已经成为数学形式化最活跃的平台。
对于 把依赖类型作为编程方法论，Brady 的 Type-Driven Development with Idris（Manning，2017，付费）是标准文本。Idris 是为类型驱动开发设计的语言；类型驱动开发就是用类型作为规约，并让类型检查器驱动实现。这本书可读且实践性强，适合想使用依赖类型、而不是从基础层面研究依赖类型的程序员。Friedman 和 Christiansen 的 The Little Typer（MIT Press，付费）是依赖类型更温和的概念入口，采用 Little Schemer 风格。它的严谨度不足以替代 TAPL、Martin-Löf 或 PLFA，但能降低进入核心直觉的门槛：类型可以描述程序和证明。
Nordström、Petersson 和 Smith 的 Programming in Martin-Löf’s Type Theory（1990，网上免费）是 Martin-Löf 类型论的系统教材式呈现。它比原始讲义要求更低，也更系统；对于想获得结构化呈现的学习者，它是 Padua 讲义的合适配套。
| 书籍 | 作用 | 类型 |
|---|---|---|
| Pierce，Types and Programming Languages（TAPL）中的类型论章节 | 类型化 λ 演算与 Curry-Howard 的入口 | 入门 |
| ATTAPL 中的高级类型系统章节 | 依赖类型、效应、线性类型 | 深入 |
| Martin-Löf，Intuitionistic Type Theory（Padua notes，免费） | 依赖类型论一手来源 | 深入 |
| The HoTT Book（免费） | 同伦类型论；当代前沿 | 深入 |
| Software Foundations Vols. 1-2（免费）中的类型论路线 | Coq 中的机制化 PLT 和类型论 | 实践 |
| Wadler 等，Programming Language Foundations in Agda（免费） | Agda 中的机制化 PLT | 实践 |
| de Moura 等，Theorem Proving in Lean 4（免费） | Lean 4 教程 | 实践 |
| Avigad & Massot，Mathematics in Lean（免费） | Lean 中的数学形式化 | 实践 |
| Brady，Type-Driven Development with Idris（付费） | 依赖类型作为编程方法论 | 深入 |
| Friedman & Christiansen，The Little Typer（付费） | 温和的依赖类型直觉入口 | 辅助 |
| Nordström、Petersson & Smith，Programming in Martin-Löf’s Type Theory（免费） | 系统化 Martin-Löf 类型论 | 深入 |
| Harper，PFPL 中的类型论基础（草稿免费） | 具有类型论基础的更广泛 PLT | 深入 |
| Chlipala，Certified Programming with Dependent Types（免费）中的依赖类型验证 | 基于 Coq 的已验证软件开发 | 深入 |
课程与讲座
Oregon Programming Languages Summer School（OPLSS） 在 YouTube 免费存档全部讲座。类型论内容稳定优秀：Frank Pfenning 关于证明论和逻辑框架的讲座，Robert Harper 关于类型论的讲座，Stephanie Weirich 关于类型推断的讲座。系统学习 OPLSS 讲座，可以获得这个主题的研究生级综览。
Carnegie Mellon 15-317（Constructive Logic，Harper）和 15-312（Principles of Programming Languages）课程材料均可免费获取，是从编程语言视角学习类型论的最佳结构化课程之一。Harper 的 15-317 讲义尤其以异常精确的方式发展 Curry-Howard 对应。
Lean 4 community 位于 leanprover-community.github.io，维护大量教程、Zulip 聊天和面向编程与数学形式化的结构化学习路径。对于一个偏研究的数学工具而言，这个共同体异常友好。
Agda community resources 位于 agda.readthedocs.io，并通过 PLFA 一书提供结构化学习路径。Agda Zulip 也很活跃。
| 课程 | 平台 | 类型 |
|---|---|---|
| OPLSS 讲座——Pfenning、Harper、Weirich（免费） | YouTube / OPLSS 网站 | 参考 |
| CMU 15-317 Constructive Logic（Harper，免费） | CMU 课程网站 | 入门 |
| CMU 15-312 Principles of PL 中的类型论序列（Harper，免费） | CMU 课程网站 | 深入 |
| Lean 4 community tutorials（免费） | leanprover-community.github.io | 实践 |
实践、工具与当前来源
在证明助手中工作，是接触材料的主要方式。没有任何类型论可视化能替代在 Coq 或 Lean 中构造证明，并让系统接受它——或用错误信息拒绝它、迫使你重新审查证明结构——这种经验。下面列出的工具就是工具；直接使用它们。
Lean 4 搭配 mathlib，是目前最活跃的平台。通过 elan（Lean 版本管理器）安装，并完成 Mathematics in Lean 的前半部分。github.com/leanprover-community/mathlib4 上的 mathlib4 仓库本身也是学习资源——阅读你已经熟悉结果的源码证明，可以展示 Lean 证明风格是什么样的。
Agda 搭配 PLFA：通过 GHCup 或 Nix 安装 Agda，完成 PLFA 书的第一部分。结构化练习有难度分级，并能提供即时反馈。
Coq 搭配 Software Foundations：通过 opam 安装，完成第二卷 Programming Language Foundations。其中 PLT 专属内容——操作语义、类型可靠性、Hoare logic——与 §3.4 最直接相关。
Proof General（Emacs）或 VSCoq（VS Code）提供交互式证明开发界面，能够在每一步 tactic 后显示证明状态——这对于理解证明构造中发生了什么是必要的。
| 资源 | 平台 | 类型 |
|---|---|---|
| Lean 4 + mathlib（免费） | elan / github.com/leanprover | 实践 |
| Agda + PLFA（免费） | agda.readthedocs.io | 实践 |
| Coq + Software Foundations（免费） | coq.inria.fr / softwarefoundations.cis.upenn.edu | 实践 |
| Lean Zulip（免费） | leanprover.zulipchat.com | 参考 |
| mathlib4 source（免费） | github.com/leanprover-community/mathlib4 | 参考 |
陷阱
| 陷阱 | 为什么会误导 | 更好的回应 |
|---|---|---|
| 通过语言特性而不是通过对应本身进入类型论 | 许多实践者是通过自己主要语言中的 generics、类型推断或代数数据类型接触类型论的。这会产生一种碎片化视角：类型论看起来像一组特性的集合，而不是一门围绕“命题即类型”对应组织起来的连贯学科。这个对应不是众多事实中的一个；它是其他一切由之展开的组织原则。 | 顺序阅读 TAPL，而不是直接跳到某些特性。简单类型 λ 演算、System F、依赖类型的发展路径，遵循这个对应的逻辑结构；按这个顺序阅读，会让对应逐渐加深的过程变得可见。 |
| 只待在证明助手中，而不读理论 | 证明助手是强大的学习工具，但只会 Lean 或 Coq、却不理解 Martin-Löf 类型论，会产生证明工程能力，却不会产生类型论理解。只有看到底层类型论，证明助手的错误信息和行为才变得可解释。 | 在阅读理论（Martin-Löf 讲义、TAPL 类型论章节）和使用证明助手之间交替。每学一个理论概念，就在证明助手中形式化一个小例子；每做完一个证明助手练习，就回头读它对应的理论结果。 |
| 未掌握简单类型就尝试依赖类型 | 依赖类型要求熟悉普通类型化 λ 演算、Curry-Howard 对应，以及对推导树做归纳证明。跳到依赖类型的学习者，会同时遇到所有这些前提，而且是在最困难的形式中遇到。 | 在进入依赖类型之前，先完成 TAPL 第 1–23 章。简单类型演算、System F 和类型重建算法都是前置知识，不是可选内容。急着进入依赖，会让人分不清哪些困难是类型论本身的，哪些只是准备不足造成的。 |
| 把构造性看作限制 | 经典逻辑更熟悉，并且对某些结果允许更短证明。把类型论看作“带着不必要限制的逻辑”的学习者，会错过重点：构造性不是限制，而是另一种信息。构造性证明是程序；经典证明不是。 | 学习具体例子，看构造性证明和经典证明在哪里分歧。介值定理、良序原理、Bolzano-Weierstrass 定理都有非构造性的经典证明，以及能够抽取算法的构造性版本。理解这种差异——以及构造性版本提供了经典版本没有提供的什么——是重视构造性而不是抗拒它的关键。 |
| 期待立即获得实践回报 | 类型论的工业应用虽然增长很快，但仍然集中在专门领域：验证编译器、证明助手、高保障系统。多数程序员在未来几年内都不会在日常工作中使用依赖类型。期待马上获得可应用技能的学习者，会因为理论与当前主流实践之间的距离而失望。 | 正确设定这项投入：类型论是长期认知投资，不是短期技能获取。它提供的理解——类型能表达什么、为什么编程和证明是同一回事、如何以形式精确性推理程序——会在职业生涯尺度上回报，而不是季度尺度上回报。工具正在迅速改进；今天的高级研究应用，就是明天的语言特性。 |
| 跳过 Curry-Howard 对应本身 | 有些学习者完成了 TAPL 的类型可靠性证明，有些学会了 Coq tactics，有些学习了 Martin-Löf 类型论——却从未停下来把 Curry-Howard 对应看作连接这一切的单一组织性洞见。结果是技术积累了，但没有综合。 | 在学习过程中的某个时刻——最好是在完成 TAPL 核心之后、进入依赖类型之前——停下来，对每个逻辑连接词及其对应类型明确写出 Curry-Howard 对应。把对应写出来。把一个简单逻辑重言式同时作为证明和程序来证明。综合时刻一旦发生，会重新组织此前学习的一切。 |