Indexed type families

These papers explore the consequences of extending Haskell's type-classes with the ability to define indexed families of data types and type synonyms. See also papers about GADTs and about type inference with constraints.

Fun with type functions

Fun with type functions, Oleg Kiselyov, Simon Peyton Jones, Chung-chieh Shan, presented at Tony Hoare's 75th birthday celebration, Cambridge, 17 April 2009.

Abstract. Tony Hoare has always been a leader in writing down and proving properties of programs. To prove properties of programs automatically, the most widely used technology today is by far the ubiquitous type checker. Alas, static type systems inevitably exclude some good programs and allow some bad ones. This dilemma motivates us to describe some fun we've been having with Haskell, by making the type system more expressive without losing the benefits of automatic proof and compact expression.

Haskell's type system extends Hindley-Milner with two distinctive features: polymorphism over type constructors and overloading using type classes. These features have become integral to Haskell, and they are widely used and appreciated. More recently, Haskell has been enriched with type families, which allows functions on types to be expressed as straightforwardly as functions on values. This facility makes it easier for programmers to effectively extend the compiler by writing functional programs that execute during type-checking.

This paper gives a programmer's tour of type families as they are supported in GHC today.


Type Checking with Open Type Functions

Type Checking with Open Type Functions Tom Schrijvers, Simon Peyton Jones, Manuel Chakravarty, and Martin Sulzmann. ICFP 2008.
Abstract. 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.


Towards open type functions for Haskell

Towards open type functions for Haskell Tom Schrijvers, Martin Sulzmann, Simon Peyton Jones, and Manuel Chakravarty, presented at the Implementing Functional Languages workshop, Sept 2007 (IFL07), but not part of its post-refereed proceedings.
Abstract. 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.


Associated type synonyms

Associated type synonyms, Manuel Chakravarty, Gabrielle Keller, Simon Peyton Jones, ACM SIGPLAN International Conference on Functional Programming (ICFP'05), 2005, Tallinn, Estonia.
Abstract. 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.


Associated types with class

Associated types with class, Manuel Chakravarty, Gabrielle Keller, Simon Peyton Jones, and Simon Marlow, ACM Conference on Principles of Programming Languages, Long Beach, California, Jan 2005, pp1-13.
Abstract. 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.