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.

The class declaration

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.

An Int instance

To use Ints as keys into generic maps, we declare an instance that simply uses Data.Map, thusly:

instance GMapKey Int where
  data GMap Int v        = GMapInt (Data.Map.Map Int v)
  empty                  = GMapInt Data.Map.empty
  lookup k (GMapInt m)   = Data.Map.lookup k m
  insert k v (GMapInt m) = GMapInt (Data.Map.insert k v m)

The Int instance of the associated data type GMap needs to have both of its parameters, but as only the first one corresponds to a class parameter, the second needs to be a type variable (here v). As mentioned before any associated type parameter that corresponds to a class parameter must be identical to the class parameter in each instance. The right hand side of the associated data declaration is like that of any other data type.

NB: At the moment, GADT syntax is not allowed for associated data types (or other indexed types). This is not a fundemental limitation, but just a shortcoming of the current implementation, which we expect to lift in the future.

Download the code

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.