GADTs

Generalized Algebraic Data Types (GADTs) are an extension of algebraic data types in which the return type of a constructor can be specified explicitly and may vary from the type being defined. In a conventional algebraic data type, a constructor for 'Expr Int' must return 'Expr Int'; in a GADT, the constructor 'Lit' might return 'Expr Int' while 'Add' returns 'Expr Int' and 'IsZero' returns 'Expr Bool'. The type parameter of the GADT is determined by the constructor used, not merely by the type definition, allowing the compiler to track type information at the level of individual values.

GADTs are not a full dependent type system, but they capture a significant fragment of dependent typing's power within conventional languages. They enable the compiler to verify that pattern matches are exhaustive, that certain operations are type-safe, and that invariants are maintained by construction. In Haskell, GADTs are used to embed domain-specific languages, to write typed interpreters, and to enforce correctness properties that would otherwise require runtime checks. They are a stepping stone between the simple type systems of mainstream languages and the full dependent types of Agda and Coq, and they demonstrate that much of dependent typing's practical benefit can be obtained without accepting its full complexity.

The connection to type theory is direct: GADTs are the practical programming language manifestation of indexed inductive types, a concept from the family of formal systems that includes the Calculus of Inductive Constructions and Martin-Löf type theory. The fact that GADTs have been adopted in mainstream languages — Haskell, OCaml, and even extensions of C++ — suggests that the software industry is ready for more expressive type systems, provided they arrive in digestible increments rather than as wholesale paradigm shifts.

GADTs as Constraint Systems

The systems-theoretic significance of GADTs lies in their treatment of type indices as constraints. In a conventional algebraic data type, all constructors produce values of the same type; the type is a fixed container, and the constructors fill it. In a GADT, the type itself varies with the constructor, meaning that the set of permissible operations on a value is determined by how the value was constructed. The constructor is not merely a data producer; it is a constraint propagator, carrying information forward from construction to use.

This is structurally analogous to how constraint closure operates in biological and organizational systems. In a cell, the set of reactions that can occur is constrained by the enzymes that are present, and the enzymes that are present are determined by which genes were expressed during development. The developmental history — the 'constructor' — determines the 'type' of the cell (neuron, hepatocyte, cardiomyocyte) and therefore the operations that the cell can perform. A GADT encodes this same pattern: the constructor (gene expression program) determines the type (cell type), and the type determines the permissible operations (metabolic reactions).

The parallel is not merely metaphorical. Both GADTs and biological differentiation rely on indexed typing: the properties of an entity are not global but depend on a parameter (the type index, the developmental stage, the organizational role) that is fixed at construction time and propagated through all subsequent operations. The type checker is, in this reading, a static verification system that ensures no operation is performed on an entity for which it is not licensed — exactly the function performed by cellular checkpoints, immune surveillance, and organizational protocols.

The Compiler as Proof Assistant

GADTs make visible a connection that is usually implicit: the compiler is a proof assistant for a fragment of logic. When a Haskell programmer writes a GADT for a typed expression language — where 'Lit' constructs 'Expr Int', 'Add' constructs 'Expr Int', and 'IsZero' constructs 'Expr Bool' — they are writing a logical specification of what expressions mean and what operations are valid. The compiler checks this specification. If the programmer attempts to add a boolean expression to an integer expression, the compiler rejects the program not because of a runtime error but because the program violates the logical specification.

This is the Curry-Howard correspondence in action: types are propositions, programs are proofs, and compilation is proof verification. GADTs extend this correspondence from simple propositional logic to a fragment of predicate logic with equality constraints. The type index is a term; the GADT definition is a predicate over terms; pattern matching is case analysis over the proof that the predicate holds.

The systems implication is that GADTs provide a methodology for specifying and verifying invariants at the language level. In safety-critical systems — avionics, medical devices, financial infrastructure — the cost of runtime errors is catastrophic. GADTs do not prevent all errors, but they prevent an important class: the class of errors that arise from applying an operation to data of the wrong 'kind,' where 'kind' is determined by structural properties that are knowable at compile time.

From Types to Processes

The limitation of GADTs is that they capture only static invariants — properties that are determined at construction and never change. They cannot express dynamic invariants that depend on runtime state: a file handle that is open at one moment and closed the next, a network connection that transitions from connected to disconnected, a transaction that moves from pending to committed. These are stateful invariants that require not indexed types but session types, linear types, or effect systems.

The progression from simple types to GADTs to dependent types to session types traces an arc of increasing expressive power for specifying system behavior. Simple types guarantee that functions are applied to arguments of the right shape. GADTs guarantee that operations are applied to values of the right kind. Dependent types guarantee that operations satisfy arbitrary logical specifications. Session types guarantee that processes follow valid communication protocols. Each step adds power; each step adds complexity; and each step finds application in domains where the cost of the complexity is justified by the value of the guarantee.

The systems view is that this progression is not merely a technical advance in programming languages. It is a shift in how we specify the behavior of complex systems: from informal documentation, through unit testing, to property-based testing, to formal verification, to type-level specification. GADTs occupy a sweet spot in this progression: they provide genuine guarantees (not merely probable correctness) at a cost (type system complexity) that is manageable for many applications. They are, in effect, a bounded formal method: a restricted but usable form of program verification that does not require expertise in theorem proving.

See also

• Type Theory — the logical and mathematical foundations of type systems
• Algebraic Data Type — the simpler construct that GADTs generalize
• Dependent Type — the full theoretical framework that GADTs approximate
• Curry-Howard Correspondence — the isomorphism between types and propositions
• Constraint Closure — self-maintaining constraint networks in biological systems
• Formal Verification — the broader program of proving program correctness
• Haskell — the language in which GADTs are most widely used