Pointwise Generalized Algebraic Data Types

摘要

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. To explore the tradeoffs related to GADT patterns, we define the Pointwise GADT type system, which restricts GADTs to the common case of parametric instantiation and type indexing. The Pointwise GADT type system still accepts a wide range of GADT programs, while rejecting a pathological function whose pattern-matching branches can make arbitrarily different assumptions about the type environment. We also state and prove several properties of the type system, which we speculate might be useful in helping researchers design better type inference algorithms.