Type Theory

Type theory studies formal languages where expressions are classified by types and valid reasoning is generated by rules. It is a foundation for programming languages, constructive mathematics, proof assistants, and many forms of theorem proving. At its most practical, a type system prevents certain bad programs from running. At its most foundational, propositions can be treated as types and proofs as programs.

The subject sits between semantics, logic, category theory, topology, and software engineering. It asks what expressions mean, which programs are valid, which proofs construct evidence, and how much reasoning can be checked mechanically.

The useful mental model is simple: a type is a named space of allowable evidence. A value inhabits a type when it satisfies the rules for that space. A program is safe only relative to the meaning of the types and the assumptions made outside the type system.

Type theory is usually written as a system of judgments. A judgment might say that an expression has a type, that two expressions are definitionally equal, that a type is well formed, or that a context of assumptions is valid. Rules explain how valid judgments can be derived from other valid judgments.

The notation Gamma |- t : A reads roughly as "under assumptions Gamma, term t has type A." The context matters because most expressions are only meaningful relative to named variables, hypotheses, or parameters.

This gives type theory its double life:

• in programming, rules define what the compiler accepts;
• in logic, rules define how proofs are constructed;
• in mathematics, rules define objects, equalities, and legitimate constructions;
• in knowledge systems, rules clarify when a claim is merely tagged, when it is schema-valid, and when it has proof-like support.

The design of the rules determines the behavior of the system: whether every program terminates, whether equality is decidable, whether inference is practical, whether effects can be tracked, and whether the system is expressive enough for real mathematics.

Lambda calculus is the small language at the center of many type theories. Untyped lambda calculus studies functions, application, substitution, and reduction without a type discipline. Typed lambda calculi add structure: simple types, product types, sum types, polymorphism, dependent types, linear types, and effects.

The lambda calculus matters because it makes function abstraction precise. A function is not just a box with inputs and outputs. It has binding structure, substitution behavior, evaluation rules, and equivalence rules. Those details are what let semantics connect source code to mathematical meaning.

Simply typed lambda calculus is the usual first stop. It introduces base types and function types. From there, System F adds polymorphism, dependent type theory lets types mention values, and effectful calculi add controlled ways to reason about state, exceptions, IO, concurrency, or resource use.

The Curry-Howard correspondence is the bridge between logic and programs: propositions correspond to types, and proofs correspond to programs. A function type can be read as implication, a product type as conjunction, a sum type as disjunction, and an uninhabited type as falsehood.

This is not just a slogan. It explains why a proof assistant can store a proof as a term and check it with a small kernel. It also explains why some programming patterns feel logical: returning a pair provides both pieces of evidence, returning one branch of a sum provides a case distinction, and writing a function from A to B provides a method for turning evidence of A into evidence of B.

The correspondence also clarifies the limits. A program that typechecks is only a proof of the proposition encoded by its type. If the type is too weak, the proof is too weak. If the domain model is wrong, the checker can faithfully verify the wrong thing.

Most type theories are built from a small set of constructors:

• unit types, which have one trivial inhabitant;
• empty types, which have no inhabitants and correspond to contradiction;
• product types, which combine pieces of evidence;
• sum types, which represent alternatives;
• function types, which transform evidence of one type into evidence of another;
• recursive types, which describe lists, trees, syntax, and other self-similar structures;
• polymorphic types, which express code or proofs that work uniformly across many types;
• dependent pairs and dependent functions, which let types refer to values.

These constructors appear in different clothing across Rust, TypeScript, Haskell, OCaml, Swift, Lean, Rocq, Agda, Idris, and many specification languages. The surface syntax changes, but the underlying question remains: what evidence is allowed, and what can be computed from it?

Dependent types allow types to depend on values. That means a type can express richer specifications: a vector of length n, a sorted list, a matrix whose dimensions line up, a parser that returns a syntax tree for a particular grammar, or a function that returns evidence of a property.

This is where type theory becomes visibly useful for linear algebra, number theory, protocols, parsers, and data pipelines. A dimension, modulus, version, state transition, or schema profile can move from a comment into a checked boundary.

The cost is design complexity. Dependent types make more invariants expressible, but they can also make inference harder, error messages stranger, and termination checking more important. The best dependent-type work chooses the right proof obligation, not the largest possible one.

Equality is one of the deepest design choices in type theory. Some equalities are definitional: the checker can see them by reducing terms. Other equalities are propositional: they require explicit evidence. This distinction controls how much the machine can simplify automatically and how much the user must prove.

Identity types make equality itself a subject of proof. They allow a theory to talk about paths between terms and about when two constructions should count as the same. This is one route into topology and homotopy type theory, where types behave like spaces, terms behave like points, and equalities behave like paths.

The practical lesson is modest but important: "same" is not a single idea. The same record identifier, the same value after normalization, the same API behavior, and the same mathematical object may need different equality notions.

Many type theories organize types into universes: types whose inhabitants are themselves types. Universes let a system talk about families of types without collapsing into paradox. Their design affects polymorphism, formalized mathematics, metaprogramming, and proof assistant ergonomics.

Constructive type theory differs from classical set-theoretic foundations in tone. To prove that something exists, it usually asks for a construction. That makes it naturally computational: proof content can often be extracted, normalized, or checked by a kernel.

Homotopy type theory extends this foundation by taking equality and higher paths seriously. The HoTT Book (opens in new tab) made that program accessible as a shared reference. Cubical type theory later gave computational interpretations to univalence and higher-dimensional equality, making some of the topology connection usable inside proof assistants.

Type theory is not only about static classification. It also needs a story about computation. Reduction rules say how terms evaluate. A good type system should be compatible with those rules.

Two classic safety properties are progress and preservation. Progress says a well-typed closed term is either a value or can take a step. Preservation says evaluation preserves type. Together they say that well-typed programs do not get stuck for the errors the type system is designed to exclude.

Those properties connect type theory to semantics. The type rules, evaluation rules, and equivalence rules must describe one coherent language, or the formal story becomes decoration.

Type systems balance safety, expressiveness, inference, error messages, performance, interoperability, and implementation complexity. A more expressive system can state stronger invariants, but it may also make compilation slower, errors harder to explain, or inference undecidable.

Important design ideas include:

• parametric polymorphism, where code works uniformly for many types;
• subtyping, where one type can be used where another is expected;
• row types, useful for records and extensible data;
• linear types, which track resource use;
• effect systems, which classify side effects;
• gradual typing, which mixes typed and untyped code;
• refinement types, which enrich ordinary types with predicates.

Production languages rarely maximize proof power. They pick tradeoffs that programmers can learn, compilers can implement, and ecosystems can maintain. That is why Rust makes ownership and borrowing central, while Python uses optional typing and validation libraries to make dynamic boundaries less mysterious.

In everyday software, type theory shows up as boundary design. Parse unknown data into validated types, make impossible states unrepresentable, keep effects explicit where the language allows it, and name domain concepts instead of passing strings and numbers everywhere. A small algebraic data type can often replace a pile of comments about allowed states.

Typed discipline is most useful at trust boundaries: API clients, file parsers, CLI arguments, environment variables, database rows, model outputs, and generated content. Inside the core logic, richer types can preserve meaning that would otherwise disappear into loosely named dictionaries or arrays.

The rule of thumb is to make the illegal state expensive to express and the intended state easy to use. That is a practical version of a formal idea: the shape of the type should guide the shape of the program.

Type theory is powerful because it can move claims into syntax, but a type only proves what it states. A vector length in the type can prevent dimension mismatches; it does not prove that the data came from the right sensor. A parser type can ensure a syntax tree is well formed; it does not prove that the standard was modeled correctly. A validated source record can preserve provenance fields; it does not prove that the source is truthful.

This is why type theory connects to standards, data sources, philosophy, and theorem proving. A type system helps when the domain has crisp invariants, but the domain still needs careful modeling, authority, provenance, and judgment.

Proof assistants use type theory to state and check claims about programs, protocols, hardware, cryptography, and mathematics. A proof assistant does not make the hard thinking vanish. It turns the final proof object into something small enough for a kernel to check.

Important systems include Lean (opens in new tab), Rocq (opens in new tab), Agda (opens in new tab), and Idris (opens in new tab). They differ in automation, library culture, extraction story, syntax, tactics, and foundation. The common pattern is that a small trusted core checks terms against types while humans and automation build those terms.

For compendium purposes, proof assistants are the place where type theory becomes an operational artifact. A theorem is not only described; it is encoded, checked, imported, refactored, and connected to other formal objects.

Category theory gives type theory a language of structure-preserving maps. Products, sums, functions, monads, adjunctions, and initial algebras all have categorical readings that help compare programming language features with mathematical structure.

Topology enters through homotopy type theory and identity types. Instead of treating equality as a flat yes-or-no relation, higher-dimensional type theories can track paths, paths between paths, and invariants under deformation.

These views are valuable when they explain behavior. They become noise when used as vocabulary alone. A categorical or topological claim should say which construction is being preserved, which equality is being used, and what the reader gains by changing perspective.

Typed invariants are not limited to theorem proving. Data work benefits from explicit schemas, units, dimensions, coordinate systems, identifier namespaces, and versioned source contracts. A dataset whose fields are typed and whose provenance is preserved is easier to join, visualize, refresh, and audit.

The same habit matters in numerical work. A matrix shape, vector dimension, coordinate basis, dtype, sparsity pattern, normalization, or solver tolerance can be treated as disposable metadata or as part of the object being reasoned about. Type theory supplies vocabulary for moving some of those constraints closer to the code.

Standards and protocols are informal type systems for networks of independent implementers. They define message shapes, conformance classes, registries, processing rules, error behavior, and version boundaries. Type theory cannot replace that social agreement, but it can make parts of the agreement executable.

A good specification separates syntax from semantics, examples from requirements, and validated structure from trusted meaning. That separation is shared ground between type theory, semantic web vocabularies, API schemas, and conformance tests.

The most practical type-theory habit is to turn hidden assumptions into boundary objects: schema, judgment, constructor, invariant, unit, effect, permission, or proof obligation. Once named, the boundary can be checked, documented, searched, and connected to code or standards.

That makes type theory useful even outside proof assistants. It gives the compendium a vocabulary for when a claim is merely tagged, structurally validated, semantically interpreted, or formally proved.

A useful type-theory record should name more than the type constructor. It should say what judgment is being made, what context supplies the assumptions, what equality notion is being used, and which external boundary still has to be trusted. A record like "vector length is typed" is weaker than "this function accepts a vector indexed by dimension n, preserves that dimension, and assumes the input parser already validated the source units."

That distinction makes type theory practical for the rest of the compendium. In data sources, a schema type may guarantee that a field exists while leaving source authority unresolved. In standards, a conformance type may guarantee message shape while leaving semantic interpretation to prose and tests. In theorem proving, a proposition-as-type may carry a proof object whose kernel checks the derivation. In Rust, ownership and lifetimes can enforce resource discipline while unsafe blocks and foreign-function boundaries remain explicit trust zones.

The graph should therefore separate type, proposition, proof, schema, invariant, effect, unit, capability, and validation result. Those objects are adjacent, but they are not interchangeable. A type can reject malformed data; a proof can show a theorem follows; a runtime validator can inspect an untrusted boundary; a semantic model can explain what the term means. Search is more useful when these roles are preserved.

Good display follows the same pattern: show the informal intent, then the checked boundary, then the unmodeled assumption. That keeps type theory from sounding like magic and makes it easier for readers to move between programming practice, formal semantics, and machine-checked mathematics.

Type theory gives the compendium a vocabulary for checked meaning: terms, types, judgments, contexts, reductions, equivalences, universes, constructors, proof objects, and trusted kernels. Those concepts connect pages about programming languages, formal mathematics, standards, data sources, and category theory. They also clarify the difference between a tag, a schema, a type, a proposition, a claim, and a proof.

Useful graph fields include formal system, judgment form, proof assistant, related language, semantic model, equality notion, type constructor, trusted kernel, encoded invariant, source assumption, and implementation tradeoff. Capturing those relationships helps readers move from practical programming pages to deeper foundations without collapsing everything into generic "logic."

• Treating "type safe" as a universal safety claim rather than a property relative to a language, runtime, and model.
• Encoding an invariant in a type while forgetting the external assumption that makes the invariant meaningful.
• Choosing an expressive type system without considering inference, error messages, build time, and maintainability.
• Confusing a schema-valid record with a true record.
• Using category, topology, or proof language decoratively without stating the preserved structure.
• Letting dynamic boundaries leak into typed cores without validation.

Start with simply typed lambda calculus, substitution, structural rules, progress, preservation, and normalization. Then study products, sums, polymorphism, algebraic data types, dependent pairs, dependent functions, identity types, universes, and proof assistants. From there, branch into programming language semantics, formalized mathematics, category-theoretic semantics, or homotopy type theory.

For practice, encode small invariants: non-empty lists, finite maps with explicit key spaces, vectors with dimensions, parser results with error types, or source records with provenance. The point is not to formalize everything. The point is to feel where checked meaning helps and where the world still has to be modeled carefully.

Useful references include Types and Programming Languages (opens in new tab), Practical Foundations for Programming Languages (opens in new tab), Software Foundations (opens in new tab), Programming Language Foundations in Agda (opens in new tab), nLab on type theory (opens in new tab), The HoTT Book (opens in new tab), Lean's documentation (opens in new tab), Coq documentation (opens in new tab), Agda documentation (opens in new tab), and the TYPES mailing list (opens in new tab).

• Theorem Proving for proof assistants and formal verification.
• Semantics for meaning in logic and programming languages.
• Category Theory for categorical models of types and programs.
• Topology for homotopy type theory and higher equality.
• Rust for a production language shaped by ownership and type discipline.
• Python for optional typing and runtime validation at dynamic boundaries.
• Standards for formalizing protocols and data formats.
• Data Sources for schema, provenance, and typed source records.