Chuan-kai Lin and Tim Sheard, Portland State University
Submitted to TLDI 2010.
Paper,
Nano Poster
GADTs (Generalized Algebraic Data Types) are a type system feature that allows programmers to index data constructors of an algebraic data type by type arguments. GADTs have a wide range of applications, including length-indexed lists, tagless interpreters, generic programming, and balanced trees. Type inference for GADTs is an open problem under active research.
In this paper we argue that GADTs as they currently exist are too expressive, by presenting functions whose pattern-matching branches can make arbitrarily different assumptions about the type environment. Such functions are problematic for any type inference algorithm because the inference algorithm can make arbitrary choices about the type of case branches.
We propose a restricted version of GADTs which we call Pointwise GADTs. We introduce the notion of pointwise unifier to regulate type information flow in pattern matching. The Pointwise GADT type system rejects the aforementioned ill-behaved functions. We studied a wide range of applications that use GADTs, and they all can be written as well-typed Pointwise GADT programs. This result suggests that Pointwise GADTs remain expressive enough for typical programming tasks.
Pointwise GADTs represent a compelling middle ground between simple algebraic data types (ADTs) and full GADTs. Practical programmers can use Pointwise GADTs, which have essentially the same expressiveness as GADTs, as a drop-in replacement. Researchers working on the type inference problem for GADTs can recast the problem in terms of Pointwise GADTs. This allows them to avoid a significant source of incidental complexity, so they can focus on the core issues with fewer distractions.
We conducted case studies in July 2009 to gauge the expressiveness of the Pointwise GADT type system. The corpus of our studies come from the following papers:
Here are the programs we used in our study. We annotated each GADT pattern with a comment stating the pattern type, the constructor range type, and their pointwise unifier, so we can check manually that each program is well-typed in the Pointwise GADT type system.