We 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 we identify and characterise the key technical challenge of entailment; and we give a novel, decidable, sound, and complete algorithm to solve it, together with some practically-important variants. Our system is implemented in GHC, and is already in active use.
We report on an extension of Haskell with type(-level) functions and equality constraints. We illustrate their usefulness in the context of phantom types, GADTs and type classes. Problems in the context of type checking are identified and we sketch our solution: a decidable type checking algorithm for a restricted class of type functions. Moreover, functional dependencies are now obsolete: we show how they can be encoded as type functions.
Haskell programmers often use a multi-parameter type class in which one or more type parameters are functionally dependent on the first. Although such functional dependencies have proved quite popular in practice, they express the programmer's intent somewhat indirectly. Developing earlier work on associated data types, we propose to add functionally-dependent types as type synonyms to type-class bodies. These associated type synonyms constitute an interesting new alternative to explicit functional dependencies.
In this paper, we explore an extension to Haskell type classes that allows a type class declaration to define data types as well as values (or methods). Similarly, an instance declaration gives a witness for such data types, as well as a witness for each method. It turns out that this extension directly supports the idea of a type-indexed type, and is useful in many applications, especially for self-optimising libraries that adapt their data representations and algorithms in a type-directed manner.Crucially, just as Haskell's existing type-class mechanism can be explained by translation into System F, so we can explain our extension by translation into System F, and we do so in full detail. This is a valuable property since it ensures that the addition of associated data types to an existing Haskell compiler leads to changes in the front end only.