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.