Pointwise generalized algebraic data types
Chuan-kai Lin, Tim Sheard · 2010
In the GADT (Generalized Algebraic Data Types) type system, a pattern-matching branch can draw type information from both the scrutinee type and the data constructor type. Even though the type system can handle complex interactions between the two types, most programs require only simple interactions in the form of parametric instantiation and type indexing.