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.
As an exercise, implement an instance for Char that maps back to the Int instance using the conversion functions Char.ord and Char.chr.
A unit instance
Generic definitions, apart from elementary types, typically cover units, products, and sums. We start here with the unit instance for GMap:
instance GMapKey () where
data GMap () v = GMapUnit (Maybe v)
empty = GMapUnit Nothing
lookup () (GMapUnit v) = v
insert () v (GMapUnit _) = GMapUnit $ Just v
For unit, the map is just a Maybe value.
Product and sum instances
Nest, let us define the instances for pairs and sums (i.e., Either):
instance (GMapKey a, GMapKey b) => GMapKey (a, b) where
data GMap (a, b) v = GMapPair (GMap a (GMap b v))
empty = GMapPair empty
lookup (a, b) (GMapPair gm) = lookup a gm >>= lookup b
insert (a, b) v (GMapPair gm) = GMapPair $ case lookup a gm of
Nothing -> insert a (insert b v empty) gm
Just gm2 -> insert a (insert b v gm2 ) gm
instance (GMapKey a, GMapKey b) => GMapKey (Either a b) where
data GMap (Either a b) v = GMapEither (GMap a v) (GMap b v)
empty = GMapEither empty empty
lookup (Left a) (GMapEither gm1 _gm2) = lookup a gm1
lookup (Right b) (GMapEither _gm1 gm2 ) = lookup b gm2
insert (Left a) v (GMapEither gm1 gm2) = GMapEither (insert a v gm1) gm2
insert (Right a) v (GMapEither gm1 gm2) = GMapEither gm1 (insert a v gm2)
If you find this code algorithmically surprising, I'd suggest to have a look at Ralf Hinze's paper. The only novelty concerning associated types, in these two instances, is that the instances have a context (GMapKey a, GMapKey b). Consequently, the right hand sides of the associated type declarations can use GMap recursively at the key types a and b - not unlike the method definitions use the class methods recursively at the types for which the class is given in the instance context.
Using a generic map
Finally, some code building and quering a generic map:
myGMap :: GMap (Int, Either Char ()) String
myGMap = insert (5, Left 'c') "(5, Left 'c')" $
insert (4, Right ()) "(4, Right ())" $
insert (5, Right ()) "This is the one!" $
insert (5, Right ()) "This is the two!" $
insert (6, Right ()) "(6, Right ())" $
insert (5, Left 'a') "(5, Left 'a')" $
empty
main = putStrLn $ maybe "Couldn't find key!" id $ lookup (5, Right ()) myGMap
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.
Definition of the type system extension
Detailed description to come.