GHC/Type families

Indexed types families in GHC

Indexed type families are a new addition to GHC's type extensions. They are currently an experimental feature and so their design may still change to some degree. The current implementation covers indexed data types and indexed newtypes, which can either be on the toplevel or inside class declarations, in the form of associated data types. Please not that indexed type synonyms (and hence also associated type synonyms) are not fully implemented yet. Any attempt to use them will lead to strange error messages.

What do I need to use indexed type families?

Indexed type families are implemented in GHC's HEAD (from version 6.7), which you can obtain in binary form from the nightly snapshots or in source form from the source repository. To enable indexed type families in GHC 6.7, you need to supply the compiler option -findexed-types (or -fglasgow-exts, which implies it).

An example

As an example, consider Ralf Hinze's generalised tries, a form of generic finite maps. We define a type class whose instances are the types that we can use as keys in our generic maps:

class GMapKey k where
  data GMap k :: * -> *
  empty       :: GMap k v
  lookup      :: k -> GMap k v -> Maybe v
  insert      :: k -> v -> GMap k v -> GMap k v

The interesting part is the associated data family declaration of the class. It gives a kind signature (here * -> *) for the associated data type GMap k - analog to how methods receive a type signature in a class declaration.

What it is important to notice is that the first parameter of the associated type GMap coincides with the class parameter of GMapKey. This indicates that also in all instances of the class, the instances of the associated data type need to have their first argument match up with the instance type. In general, the type arguments of an associated type can be a subset of the class parameters (in a multi-parameter type class) and they can appear in any order, possibly in an order other than in the class head. The latter can be useful if the associated data type is partially applied in some contexts.

The second important point is that as GMap k has kind <tt* -> * and k (implicitly) has kind *, the type constructor GMap (without an argument) has kind * -> * -> *. Consequently, we see that GMap is applied to two arguments in the signatures of the methods empty, lookup, and insert.

If you want to play with this example without copying it off the wiki, just download the source code for GMap from GHC's test suite.