Pointwise generalized algebraic data types

14 years 2 months ago
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. Categories and Subject Descriptors D.3.3 [PROGRAMMING S]: Language Construc...
Chuan-kai Lin, Tim Sheard
Added 17 Mar 2010
Updated 17 Mar 2010
Type Conference
Year 2010
Where TLDI
Authors Chuan-kai Lin, Tim Sheard
Comments (0)