In a GADT, the product constructors (called data constructors in Haskell) can provide an explicit instantiation of the ADT as the type instantiation of their return value. This allows defining functions with a more advanced type behaviour. For a data constructor of Haskell 2010, the return value has the type instantiation implied by the instantiation of the ADT parameters at the constructor's application.
-- A parametric ADT that is not a GADTdataLista=Nil|Consa(Lista)integers::ListIntintegers=Cons12(Cons107Nil)strings::ListStringstrings=Cons"boat"(Cons"dock"Nil)-- A GADTdataExprawhereEBool::Bool->ExprBoolEInt::Int->ExprIntEEqual::ExprInt->ExprInt->ExprBooleval::Expra->aevale=caseeofEBoola->aEInta->aEEqualab->(evala)==(evalb)expr1::ExprBoolexpr1=EEqual(EInt2)(EInt3)ret=evalexpr1-- False
They are currently implemented in the GHC compiler as a non-standard extension, used by, among others, Pugs and Darcs. OCaml supports GADT natively since version 4.00.[4]
The GHC implementation provides support for existentially quantified type parameters and for local constraints.
In spring 2021, Scala 3.0 is released.[9] This major update of Scala introduce the possibility to write GADTs[10] with the same syntax as ADTs, which is not the case in other programming languages according to Martin Odersky.[11]
We would have run into problems using regular algebraic data types. Dropping the type parameter would have made the lifted base types existentially quantified, making it impossible to write the evaluator. With a type parameter we would still be restricted to a single base type. Furthermore, ill-formed expressions such as App (Lam (\x -> Lam (\y -> App x y))) (Lift True) would have been possible to construct, while they are type incorrect using the GADT. A well-formed analogue is App (Lam (\x -> Lam (\y -> App x y))) (Lift (\z -> True)). This is because the type of x is Lam (a -> b), inferred from the type of the Lam data constructor.
Sulzmann, Martin; Schrijvers, Tom; Stuckey, Peter J. (2006). "Principal Type Inference for GHC-Style Multi-Parameter Type Classes". In Kobayashi, Naoki (ed.). Programming Languages and Systems: 4th Asian Symposium (APLAS 2006). Lecture Notes in Computer Science. Vol. 4279. pp. 26–43.