Generalized Algebraic Data Types, GADTs, are algebraic data types which include both (a) existential types and (b) type equalities. The combination allows for a

Generalized Algebraic Data Types, GADTs, are algebraic data types which include both (a) existential types and (b) type equalities. The combination allows for a certain kind of interaction between the specific kind of value within a type and the type itself. For instance, we might have a little expression language using normal ADTs [0] type exp = | Int of int -- integer constants | Bool of bool -- bool constants | Add of exp * exp -- addition | Neg of exp -- negation | Ifte of exp * exp * exp -- if then else | Lte of exp * exp -- less than or equal to but there's no particular guarantee that a value of `exp` is well-typed. For instance, the following is a valid value of `exp` let x : exp = Add (Int 3, Bool true) GADTs allow us to fix this situation by reflecting the type of the expression value into the type of the expression. Here's some syntax type _ exp = | Int : int -> int exp | Bool : bool -> bool exp | Add : int exp * int exp -> int exp | Neg : int exp * int exp | Ifte : bool exp * 'a exp * 'a exp -> 'a exp | Lte : int exp * int exp -> bool exp The way to read this syntax is to see it as giving the "type" of each constructor. Not only do we now parameterize the `exp` type with an index type corresponding to the type of the value this expression denotes, we also create very non-trivial type equations like Ifte : bool exp -> 'a exp -> 'a exp -> 'a exp and Lte : int exp -> int exp -> bool exp The upshot is that while the type of an interpreter for the first exp would have to look like type value = VInt of int | VBool of bool val interpret : exp -> value option the type of the second `exp` is so constrained as to eliminate (a) the need for the separate `value` type and (b) the possibility of failure: val interpret : 'a exp -> 'a let interpret = function | Int i -> i | Bool b -> b | Add (i1, i2) -> interpret i1 + interpret i2 | Neg i -> - (interpret i) | Ifte (c, t, e) -> if interpret c then interpret t else interpret e | Lte (i1, i2) -> interpret i1 <= interpret i2 Such a construction is known to be type-error free because GADTs allow us to ensure that type constructors follow certain type equations and it's possible to write such a clean evaluator because GADTs keep around enough type information so that the compiler can "trust" them. Finally, the short answer of how they work is something like they interpret a constructor like Ifte : bool exp * 'a exp * 'a exp -> 'a exp as one with some existential types Ifte : ... | 'x exp * 'a exp * 'a exp 'a ex and some type equalities Ifte : 'x == int | ... then when typechecking it just has to collect all the unique new type variables and solve the system of equalities which arises. [0] Yeah, the author pooh poohs at examples like this, but I think they're really particularly clear.