[4] The GHC implementation provides support for existentially quantified type parameters and for local constraints.
An early version of generalized algebraic data types were described by Augustsson & Petersson (1994) and based on pattern matching in ALF.
[9] This major update of Scala introduced the possibility to write GADTs[10] with the same syntax as algebraic data types, which is not the case in other programming languages according to Martin Odersky.
[11] Applications of GADTs include generic programming, modelling programming languages (higher-order abstract syntax), maintaining invariants in data structures, expressing constraints in embedded domain-specific languages, and modelling objects.
[12] An important application of GADTs is to embed higher-order abstract syntax in a type safe fashion.