Type Checking With Open Type Functions

The authors report on an extension of Haskell with open type-level functions and equality constraints that unifies earlier work on GADTs, functional dependencies, and associated types. The contribution of the paper is that they identify and characterize the key technical challenge of entailment checking; and they give a novel, decidable, sound, and complete algorithm to solve it, together with some practically-important variants. Their system is implemented in GHC, and is already in active use. Dependently-typed languages, such as ATS (Chen and Xi 2005), Cayenne (Augustsson 1998), and Epigram (McBride), enable the programmer to encode complex properties in types.