Dependent types - Ciallo Wiki

1 Foundations

Dependent types are types that can refer to values, allowing a program or mathematical object to carry extra information in its type. Instead of classifying items only by broad categories such as “integer” or “list,” a dependent type can encode finer details, such as the exact length of a list or the fact that a number lies within a certain range. This makes types more expressive and gives the type system a stronger role in describing and checking behavior.

The idea is central to type theory and to several programming and proof systems. It supports precise specifications, helps prevent classes of errors before execution, and enables a close relationship between programs and mathematical proofs.

1.1 Basic definition

A dependent type is a type whose form depends on a term. In an ordinary type system, the type of an expression is usually fixed independently of runtime values. In a dependent type system, a type can vary according to an input value, so the type itself can encode data-dependent properties.

A simple example is a type of lists indexed by their length. Rather than using one generic list type, one may define a family of types, each representing lists of a particular size. The index is part of the type, so operations can express and preserve size information precisely.

1.2 Types as families

Dependent types are often described as families of types indexed by values. For each index, there is a corresponding type in the family. This view makes the structure easier to understand: a single definition can generate many related types, one for each value of the index.

This family-based perspective is useful in both programming and logic. It allows one to model structures whose shape depends on a parameter, and it provides a natural way to express properties that change with input.

1.2.1 Indexing by values

Indexing by values means that a type constructor takes a term-level argument and produces a type specialized to that argument. For example, a finite set type may be indexed by a natural number indicating how many elements are permitted. A value of the resulting type then carries not only its content but also a proof that it fits the index.

This approach is especially common when the property of interest is numerical, structural, or relational. By putting the index in the type, the compiler or proof checker can enforce constraints that would otherwise require separate runtime checks.

1.2.2 Type dependency on terms

Type dependency on terms is the defining feature of dependent type systems. Terms may appear in types, and those terms can influence what values are admissible. This makes the boundary between data and specification much thinner than in simpler systems.

The dependency can be direct, as when a type explicitly mentions a particular value, or indirect, as when a type is parameterized by a term and instantiated later. In either case, the type system tracks relationships that ordinary static typing cannot express.

1.3 Relationship to simple type systems

Simple type systems classify expressions without allowing types to vary with values. They are easier to implement and understand, but they are less expressive. Dependent types extend this framework by permitting richer statements about programs, often at the cost of greater complexity in type checking and inference.

Many features familiar from ordinary type systems still exist in dependent settings, but their behavior becomes more precise. Nondependent function types, product types, and sum types can often be seen as special cases of dependent constructions.

1.4 Motivation and uses

Dependent types are motivated by the desire to represent correctness information directly in programs. They are used to encode invariants, refine data structures, and ensure that functions are applied only in valid ways. This can reduce the need for external documentation or ad hoc runtime assertions.

They are also valuable in formal verification and mathematics. Proof assistants based on dependent type theory can represent logical statements as types and proofs as terms, allowing machine-checked reasoning about algorithms, specifications, and theorems.

2 Formal theory

The formal study of dependent types arises in type theory, where terms, types, and proofs are treated within a single symbolic framework. Dependent type theory extends the usual treatment by allowing types to vary with terms, creating a system expressive enough for both programming and logic.

The theory includes function spaces, pair types, equality types, and rules governing how expressions are formed and transformed. These components provide the foundation for dependent programming languages and proof assistants.

2.1 Type theory background

Type theory provides a language for describing expressions together with the kinds of values they may denote. In a dependent setting, the typing rules must account for the possibility that a type refers to a term already present in the context.

The result is a structured system of judgments that track which terms are well formed, which types they inhabit, and how substitutions or reductions affect them.

2.1.1 Lambda calculus and type constructors

The lambda calculus supplies the basic notation for functions and application. Dependent type theory builds on this by adding type constructors that may depend on terms. A function can therefore produce not just a value but a value whose type reflects earlier arguments.

This combination makes the formal system highly expressive. It can describe computations, specifications, and proofs in a uniform syntax.

2.1.2 Judgments and contexts

A judgment states that a term has a type, that two expressions are equal, or that a type is well formed. Contexts list variables and assumptions available at a given point in a derivation. In a dependent system, the context is especially important because later types may refer back to earlier variables.

Well-formedness depends on the order of declarations. A type may only mention values that have already been introduced, which preserves consistency in the logical structure of the system.

2.2 Dependent function types

Dependent function types generalize ordinary function types by allowing the result type to depend on the input. They are among the most important constructs in dependent type theory and are used to model functions whose outputs are constrained by their arguments.

They are often written using Pi notation, reflecting their role as generalized universal quantification in logic.

2.2.1 Pi types

Pi types represent functions where the return type varies with the argument. For each input value, there is a possibly different output type. This is essential when the result must preserve or reflect information about the input.

A dependent function can be seen as a family of functions, one for each possible argument. The typing rules ensure that the output is well formed for every allowed input.

2.2.2 Non-dependent versus dependent functions

A nondependent function type has a fixed codomain, regardless of the argument. By contrast, a dependent function type can change its codomain according to the supplied value. Ordinary functions are thus a special case of dependent functions in which the result type does not actually vary.

This distinction is important in practice. A generic mapping function may be nondependent, while a function that returns a proof about its input typically requires a dependent type.

2.3 Dependent pair types

Dependent pair types model pairs in which the type of the second component depends on the first. They are used to package data together with evidence or with information that is linked to that data.

These types are especially useful when the existence of some object is known, but the object must come with a witness or proof of a property.

2.3.1 Sigma types

Sigma types formalize dependent pairs. The first component is a value, and the second component has a type determined by that value. This structure allows one to combine data and proof in a single object.

Sigma types are the dependent analogue of ordinary product types. They are often used to encode records, subsets, and existence statements.

2.3.2 Existential interpretation

Sigma types have a natural existential interpretation in logic. A term of a Sigma type asserts that there exists a value with a certain property, and the term itself provides the witness. The second component serves as evidence that the property holds for the chosen witness.

This interpretation is one reason dependent type theory is closely connected to constructive mathematics. Existence is not merely asserted; it is demonstrated by an explicit construction.

2.4 Equality and identity types

Equality types express that two terms are equal in the sense relevant to the type theory. In dependent settings, equality is not only a relation between values but also a tool for moving information across types that depend on those values.

Identity types are central to reasoning about substitution, transport, and the coherence of dependent constructions.

2.4.1 Propositional equality

Propositional equality treats equality as a type whose inhabitants are proofs that two terms are equal. This is distinct from definitional or judgmental equality, which is handled by the type checker through computation and simplification.

Propositional equality allows explicit reasoning about equalities that are not immediate from syntax or reduction. It is a key ingredient in formal proofs involving dependent data.

2.4.2 Transport and substitution

Transport is the process of moving a term from one type to another along a proof of equality. If a property depends on a value and that value is shown equal to another, transport transfers the corresponding evidence across the equality.

Substitution plays the same conceptual role at the level of terms and types. It is essential for working with dependent families, where replacing equal terms must preserve correctness.

3 Syntax and semantics

Dependent type systems require a precise syntax for expressing terms and types, along with semantics describing how expressions are interpreted and evaluated. Because types may mention terms, the system must also manage universes and ensure that the theory remains coherent.

The syntax and semantics together determine how programs are checked, reduced, and executed, and they shape the practical behavior of dependent languages and proof assistants.

3.1 Terms, types, and universes

In dependent type theory, the same formal language often contains both terms and types. To avoid logical paradoxes, many systems organize types into universes, which are types of types arranged in levels.

This hierarchy allows the system to talk about types without collapsing the distinction between an object and the collection that classifies it.

3.1.1 Universe hierarchies

Universe hierarchies separate types into layers, such as a type of small types and a larger type that contains it. This stratification helps maintain consistency when types are themselves treated as objects.

Hierarchies are particularly important in expressive systems that quantify over types or construct types of types. They provide a disciplined way to avoid self-reference problems.

3.1.2 Type-in-type issues

Type-in-type occurs when a single universe is allowed to contain itself. While convenient for notation, this can lead to inconsistency in sufficiently powerful systems. For this reason, practical theories usually avoid unrestricted self-containment.

A carefully designed universe structure preserves expressiveness while preventing paradoxical constructions. This is one of the main technical concerns in the foundations of dependent type theory.

3.2 Type checking

Type checking determines whether expressions are well typed under the rules of the system. In dependent type theory, this process is more involved than in simpler systems because checking may require evaluating terms and comparing expressions that are definitionally equal.

The added expressiveness often comes with greater algorithmic complexity, especially when terms occur inside types.

3.2.1 Decidability concerns

Decidability asks whether there is always an algorithm that can determine if a term has a given type. In many dependent systems, full inference is not fully automatic, and some parts of type reconstruction must be supplied by the programmer or proof author.

Designers of dependent languages balance expressiveness against the need for predictable checking. Restrictions on recursion, equality, or universe formation are often introduced to preserve decidability.

3.2.2 Normalization and conversion

Normalization reduces expressions to simpler forms, and conversion checks whether two expressions are equivalent after reduction. In dependent systems, conversion is frequently used during type checking because a type may mention a term whose simplified form determines compatibility.

Normalization properties also support trust in the theory. If every well-typed term reduces in a controlled way, then the system is less likely to admit contradictory or ill-behaved definitions.

3.3 Operational meaning

Operational meaning describes how expressions compute. Even in a proof-oriented setting, dependent type theory usually has a notion of evaluation that explains how terms reduce and how programs execute.

The operational rules interact with typing, so computation must preserve correctness while allowing meaningful reduction.

3.3.1 Reduction rules

Reduction rules specify how function application, pattern matching, and other constructs simplify. In a dependent theory, reduction may also affect types indirectly, since types can contain reducible terms.

These rules are important both for execution and for definitional equality. They define the computational behavior that the type checker may rely on when comparing expressions.

3.3.2 Evaluation strategies

Evaluation strategies determine the order in which reductions occur. Different systems may use call-by-name, call-by-value, or variants adapted to proof checking and normalization. The chosen strategy can affect efficiency, readability, and the handling of infinite or partially defined objects.

In dependent systems, evaluation must be compatible with type checking. This often leads to conservative strategies that preserve logical soundness.

4 Programming with dependent types

Dependent types make it possible to write programs whose types state detailed correctness properties. This can improve safety, documentation, and maintainability by embedding invariants directly in code.

The programming style is often more explicit than in ordinary languages, but the payoff is stronger guarantees about program behavior.

4.1 Indexed data structures

Indexed data structures are collections whose types record properties such as size, ordering, or bounds. By carrying this information in the type, many mistakes can be detected at compile time rather than during execution.

Such structures are widely used in verified programming because they align data layout with formal constraints.

4.1.1 Vectors with length indices

A vector type indexed by length distinguishes between lists of different sizes. A function operating on vectors can then declare exactly how the length changes, making it impossible to accidentally treat a short vector as a long one.

This is useful for algorithms that require nonempty inputs, exact dimension matching, or size-preserving transformations.

4.1.2 Finite sets and bounded numbers

Finite sets and bounded numbers are natural dependent types. A bounded natural number can be typed by the upper limit it does not exceed, while a finite set type can represent the range of valid indices for a structure of a given size.

These encodings help prevent out-of-range access and similar errors. They are common in safe array handling and in verified combinatorial algorithms.

4.2 Specification in types

Dependent types allow programmers to express specifications directly in type signatures. A type may state what a function requires, what it returns, and what relationship holds between input and output.

This turns type checking into a form of specification checking, with the compiler or proof assistant verifying the intended contract.

4.2.1 Preconditions and postconditions

Preconditions describe what must be true before a function is used, while postconditions describe what is guaranteed afterward. In a dependent type system, both can be encoded in the type, often by taking arguments that represent evidence of the precondition or by returning evidence of the postcondition.

This makes invalid calls impossible in well-typed code. The result is a strong static guarantee that functions are used only in permitted ways.

Dependent types can provide guarantees similar to refinement types, but often with greater expressiveness. They can express that a returned value satisfies a precise property, or that a computation transforms one valid state into another.

Such guarantees are useful for APIs, protocol handlers, and data-processing pipelines. They help ensure that logic embedded in the program is consistent with its specification.

4.3 Pattern matching and recursion

Pattern matching and recursion are key programming tools in dependent systems. Because types may depend on the shape of data, matching on constructors can refine the type information available in each branch.

This refinement makes it possible to write functions that preserve invariants while analyzing structured inputs.

4.3.1 Totality checking

Totality checking verifies that a function is defined for every valid input. In dependently typed settings, totality is often essential because partial functions can undermine the logical interpretation of programs as proofs.

A totality checker can reject functions with missing cases or definitions that may fail to produce a result for some input.

4.3.2 Termination and structural recursion

Termination ensures that recursive definitions eventually finish. Many dependent systems require recursion to be structurally decreasing or otherwise well founded, so that every accepted definition is guaranteed to terminate.

This restriction supports consistency when programs are interpreted as proofs. It also gives users confidence that verified functions do not hide nonterminating behavior.

5 Dependent type theory in logic

Dependent type theory has a close relationship with logic, especially constructive logic. Types can represent propositions, and terms can represent proofs, turning logical reasoning into a form of program construction.

This perspective is especially influential in proof assistants, where proving a theorem often amounts to building a term of the appropriate type.

5.1 Curry–Howard correspondence

The Curry–Howard correspondence identifies propositions with types and proofs with programs. In this view, proving a statement means constructing a term inhabiting the corresponding type.

Dependent types enrich this correspondence by allowing propositions to mention values, making logical statements more precise and expressive.

5.1.1 Propositions as types

When propositions are treated as types, a statement is considered true if its type is inhabited. Logical connectives correspond to type constructors, and proof rules correspond to typing rules.

This interpretation provides a unified language for mathematics and computation. It also clarifies why a proof assistant can check proofs in much the same way a compiler checks programs.

5.1.2 Proofs as programs

Proofs as programs means that a proof object is not just a justification but a concrete piece of syntax that can be manipulated and checked. Constructing a proof often resembles writing a program that produces evidence of a claim.

This viewpoint encourages a constructive style of reasoning. Rather than relying on abstract existence claims, one builds explicit witnesses and transformations.

5.2 Constructive reasoning

Constructive reasoning requires explicit evidence for claims, especially existential ones. Dependent type theory naturally supports this style because types can demand concrete witnesses and proof terms.

The resulting proofs are often computational, meaning that they can produce data as well as certify facts.

5.2.1 Witness extraction

Witness extraction refers to the fact that an existential proof in a dependent type system often contains the object whose existence is asserted. If a type states that some value satisfies a property, a term inhabiting that type provides the value itself.

This is valuable in verified search, algorithm design, and program synthesis. The proof does double duty as both certification and data.

5.2.2 Formal proof development

Formal proof development uses dependent type theory to build long chains of verified reasoning. Proofs can be structured as scripts or terms, depending on the system, and they are checked mechanically for correctness.

This approach is especially useful for complex arguments involving many intermediate lemmas. The type system helps manage dependencies and ensures that each step follows from the previous ones.

5.3 Quantification and predicates

Dependent type theory provides a direct interpretation of quantifiers and predicates. Universal and existential statements become function and pair types, often with explicit dependence on values.

This yields a precise framework for stating and proving properties about all or some members of a domain.

5.3.1 Universal quantification

Universal quantification corresponds to dependent function types. A statement asserting that a property holds for every element of a domain can be represented as a function that, for each element, produces a proof of the property.

This interpretation mirrors ordinary mathematical practice while making the proof term explicit. It is a standard way to encode general theorems.

5.3.2 Existential quantification

Existential quantification corresponds to dependent pair types. A statement that there exists an element with a property is represented by a value together with evidence that the property holds for that value.

This encoding is constructive by nature. It aligns existential claims with actual data and proofs rather than abstract assertion.

6 Implementations and languages

Dependent types appear in both proof assistants and programming languages. Some systems are designed primarily for theorem proving, while others aim to support practical software development with strong static guarantees.

These implementations vary in automation, syntax, and inference power, but they share the core idea that types may depend on values.

6.1 Proof assistants

Proof assistants use dependent types to represent propositions and proofs in a machine-checkable form. They are widely used for verifying mathematical results, software properties, and formal specifications.

Their design emphasizes soundness and expressiveness, often at the expense of requiring more explicit user guidance than conventional programming environments.

6.1.1 Coq

Coq is a widely used proof assistant based on dependent type theory. It supports interactive theorem proving, inductive definitions, and extraction of executable code from verified developments.

Its ecosystem has made it a major platform for formalized mathematics and certified software proofs.

6.1.2 Agda

Agda combines dependent types with a programming-language-like syntax. It is often used both as a proof assistant and as a dependently typed programming language, with a strong emphasis on expressiveness and direct manipulation of proof terms.

Its style is close to functional programming, which makes it attractive for users who want to write programs and proofs in a unified setting.

6.1.3 Lean

Lean is a proof assistant with a modern language design and extensive support for mathematical formalization. It uses dependent types to encode propositions and proofs, and it includes automation aimed at easing proof construction.

It is notable for combining a theorem-proving environment with features that appeal to both mathematicians and programmers.

6.2 Dependently typed programming languages

Some languages are built to support general programming with dependent types, not only theorem proving. They aim to let developers write ordinary software while benefiting from stronger compile-time guarantees.

These languages often provide a compromise between expressiveness and usability.

6.2.1 Idris

Idris is a dependently typed functional programming language designed to make dependent types practical for general programming. It allows programmers to state rich invariants in types and to use those invariants in everyday code.

The language is known for its emphasis on expressive type annotations and the close integration of programming and proving.

F* is a verification-oriented language with dependent types and strong support for program specification. It is often used to write code together with proofs of correctness, especially in security-sensitive or high-assurance settings.

Related systems explore similar ideas, blending dependent typing with automation, refinement checking, or proof-oriented programming.

6.3 Practical limitations

Despite their power, dependent types can be demanding to use. Their expressiveness often requires more explicit annotations, more careful design of definitions, and a deeper understanding of the underlying theory.

Tooling and automation continue to improve, but practical use still involves trade-offs between precision and convenience.

6.3.1 Complexity of type inference

Type inference is harder in dependent systems because types may require information that is not apparent from syntax alone. The checker may need to solve equations, reduce expressions, or infer missing values from context.

As a result, programmers often supply more annotations than they would in a simpler language. This can improve clarity but also increases verbosity.

6.3.2 Usability and annotation burden

The need for explicit proofs and type annotations can make dependently typed programming feel less lightweight than conventional programming. Users must often guide the checker through arguments that are obvious to humans but not easily inferred by the machine.

Language designers attempt to reduce this burden through tactics, automation, and better notation. Even so, the cost of precision remains an important consideration.

7 Advanced topics

Advanced research on dependent types examines extensions that increase expressive power or improve the connection to logic and mathematics. These topics often address issues of universes, inductive reasoning, equality, and higher-dimensional structure.

They are especially prominent in modern proof assistants and in homotopy type theory.

7.1 Universe polymorphism

Universe polymorphism allows definitions to work uniformly across different universe levels. This avoids duplicating the same concept at multiple sizes and improves reusability in large formal developments.

It is an important refinement of the basic universe hierarchy.

7.1.1 Cumulativity

Cumulativity permits smaller universes to be treated as members of larger ones. This makes it easier to write general definitions and avoid unnecessary coercions between levels.

The feature improves convenience, but it must be managed carefully to preserve consistency and avoid ambiguities in universe assignment.

7.1.2 Predicative and impredicative systems

Predicative systems restrict a definition so that it cannot quantify over a universe that contains it in a problematic way. Impredicative systems allow some broader forms of quantification, which can be powerful but also technically delicate.

Different systems choose different balances between strength and safety. The choice affects what can be expressed and how the logic behaves.

7.2 Inductive and coinductive types

Inductive and coinductive types extend the language of data definitions. Inductive types describe finitely generated structures, while coinductive types represent potentially infinite objects or processes.

Dependent versions of these notions allow the shape and properties of the data to vary with indices.

7.2.1 Families of inductive types

Families of inductive types are inductive definitions indexed by values. Examples include vectors indexed by length and trees indexed by height or shape. These families allow rich invariants to be built into recursive data.

The elimination principles for such types are carefully designed to respect the index information. This makes pattern matching both powerful and type safe.

7.2.2 Coinductive reasoning

Coinductive reasoning concerns infinite data structures or ongoing computations, such as streams. In dependently typed settings, coinduction can be used to specify and verify systems that produce data endlessly or react over time.

Such reasoning relies on productivity rather than termination. The system must ensure that each observable step of a coinductive object is well defined.

7.3 Higher inductive types

Higher inductive types extend inductive definitions by allowing not only points but also paths or identifications to be generated. This gives the type theory a way to build spaces and equality structure directly.

They are a major feature in homotopy type theory and related research.

7.3.1 Paths and homotopical interpretation

Paths represent equalities or identifications between points in a type. In the homotopical interpretation, types behave like spaces and equalities like continuous paths between points.

This viewpoint enriches the meaning of dependent types and connects them with concepts from topology and higher category theory.

7.3.2 Connections to homotopy type theory

Homotopy type theory uses dependent type theory with a homotopical interpretation, emphasizing equality, paths, and equivalences. It has influenced modern foundations of mathematics and led to new ways of thinking about identity and structure.

The theory extends the classical role of dependent types by giving equalities their own geometric and computational significance.

7.4 Extensionality principles

Extensionality principles strengthen the theory by identifying objects that behave the same in relevant respects. They can simplify reasoning, especially when one wants to treat functions or types as equal based on their observable behavior.

Such principles are often studied carefully because they may alter the strength or consistency profile of a system.

7.4.1 Function extensionality

Function extensionality states that two functions are equal if they give equal outputs for equal inputs. This principle aligns formal equality with the intuitive idea that functions are determined by their behavior.

It is often desirable in proofs involving dependent functions, though it may need to be added as an explicit axiom or derived from stronger assumptions.

Univalence relates equality of types to equivalence between them. It is a prominent idea in modern type theory and provides a powerful bridge between structural sameness and formal identity.

In systems influenced by univalence, dependent types interact with equivalence in especially rich ways, supporting abstract but precise reasoning about mathematical structures.

8 Applications

Dependent types are used wherever precise static guarantees are valuable. Their applications range from software verification to formal mathematics, and from specification-heavy development to security-sensitive systems.

They are particularly effective when properties are difficult to test exhaustively but can be stated clearly in advance.

8.1 Program verification

Program verification uses dependent types to prove that code satisfies a specification. The type system can rule out incorrect states, invalid inputs, and logic errors before the program runs.

This makes dependent typing attractive for high-assurance software and safety-critical components.

8.1.1 Safety properties

Safety properties include absence of out-of-bounds access, invalid states, and certain classes of runtime failure. By encoding these conditions in types, a programmer can make illegal operations unrepresentable.

This approach shifts effort from testing individual cases to proving general properties about the code.

8.1.2 Certified algorithms

Certified algorithms are algorithms accompanied by proofs of correctness. Dependent types are well suited to expressing both the algorithm and the claim that it behaves as intended.

Such certification is useful in sorting, parsing, arithmetic, and data-structure libraries, where correctness can be stated in precise formal terms.

8.2 Mathematics formalization

Dependent type theory is a major foundation for machine-checked mathematics. It allows definitions, theorems, and proofs to be represented in a form that a computer can verify.

This has made it possible to formalize substantial parts of modern mathematics with high reliability.

8.2.1 Machine-checked theorems

Machine-checked theorems are results whose proofs have been verified by a proof assistant. Dependent types provide the language in which these proofs are written, ensuring that each step follows from the rules of the system.

This reduces the risk of hidden mistakes and can reveal gaps in informal arguments.

8.2.2 Formalized algebra and analysis

Algebra and analysis have both been formalized using dependent type theory. Structures such as groups, rings, metrics, and sequences can be defined precisely, and theorems about them can be proved in a modular way.

The precision of dependent types helps organize assumptions and track hypotheses throughout long proofs.

8.3 Secure and reliable software

Dependent types can improve software reliability in systems where correctness and data integrity are especially important. They can describe protocols, enforce invariants, and help maintain consistency across components.

This is useful in domains where failures are costly or where specifications must be followed exactly.

8.3.1 Protocol specifications

Protocol specifications describe the allowed sequence of interactions between components. Dependent types can model these sequences so that only valid transitions are representable.

This helps prevent mismatched messages, illegal states, and certain communication errors in structured software systems.

8.3.2 Data integrity constraints

Data integrity constraints ensure that stored or transmitted information satisfies required conditions. A dependent type may encode constraints such as valid ranges, nonempty collections, or relationships between fields in a record.

By checking these constraints at compile time or through formal verification, a system can reduce the chance of corrupted or inconsistent data.