7.7. Type families

Indexed type families form an extension to facilitate type-level programming. Type families are a generalisation of associated data types (“Associated Types with Class”, M. Chakravarty, G. Keller, S. Peyton Jones, and S. Marlow. In Proceedings of “The 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'05)”, pages 1-13, ACM Press, 2005) and associated type synonyms (“Type Associated Type Synonyms”. M. Chakravarty, G. Keller, and S. Peyton Jones. In Proceedings of “The Tenth ACM SIGPLAN International Conference on Functional Programming”, ACM Press, pages 241-253, 2005). Type families themselves are described in the paper “Type Checking with Open Type Functions”, T. Schrijvers, S. Peyton-Jones, M. Chakravarty, and M. Sulzmann, in Proceedings of “ICFP 2008: The 13th ACM SIGPLAN International Conference on Functional Programming”, ACM Press, pages 51-62, 2008. Type families essentially provide type-indexed data types and named functions on types, which are useful for generic programming and highly parameterised library interfaces as well as interfaces with enhanced static information, much like dependent types. They might also be regarded as an alternative to functional dependencies, but provide a more functional style of type-level programming than the relational style of functional dependencies.

Indexed type families, or type families for short, are type constructors that represent sets of types. Set members are denoted by supplying the type family constructor with type parameters, which are called type indices. The difference between vanilla parametrised type constructors and family constructors is much like between parametrically polymorphic functions and (ad-hoc polymorphic) methods of type classes. Parametric polymorphic functions behave the same at all type instances, whereas class methods can change their behaviour in dependence on the class type parameters. Similarly, vanilla type constructors imply the same data representation for all type instances, but family constructors can have varying representation types for varying type indices.

Indexed type families come in three flavours: data families, open type synonym families, and closed type synonym families. They are the indexed family variants of algebraic data types and type synonyms, respectively. The instances of data families can be data types and newtypes.

Type families are enabled by the flag -XTypeFamilies. Additional information on the use of type families in GHC is available on the Haskell wiki page on type families.

7.7.1. Data families

Data families appear in two flavours: (1) they can be defined on the toplevel or (2) they can appear inside type classes (in which case they are known as associated types). The former is the more general variant, as it lacks the requirement for the type-indexes to coincide with the class parameters. However, the latter can lead to more clearly structured code and compiler warnings if some type instances were - possibly accidentally - omitted. In the following, we always discuss the general toplevel form first and then cover the additional constraints placed on associated types.

7.7.1.1. Data family declarations

Indexed data families are introduced by a signature, such as

data family GMap k :: * -> *

The special family distinguishes family from standard data declarations. The result kind annotation is optional and, as usual, defaults to * if omitted. An example is

data family Array e

Named arguments can also be given explicit kind signatures if needed. Just as with [http://www.haskell.org/ghc/docs/latest/html/users_guide/gadt.html GADT declarations] named arguments are entirely optional, so that we can declare Array alternatively with

data family Array :: * -> *

7.7.1.2. Data instance declarations

Instance declarations of data and newtype families are very similar to standard data and newtype declarations. The only two differences are that the keyword data or newtype is followed by instance and that some or all of the type arguments can be non-variable types, but may not contain forall types or type synonym families. However, data families are generally allowed in type parameters, and type synonyms are allowed as long as they are fully applied and expand to a type that is itself admissible - exactly as this is required for occurrences of type synonyms in class instance parameters. For example, the Either instance for GMap is

data instance GMap (Either a b) v = GMapEither (GMap a v) (GMap b v)

In this example, the declaration has only one variant. In general, it can be any number.

Data and newtype instance declarations are only permitted when an appropriate family declaration is in scope - just as a class instance declaration requires the class declaration to be visible. Moreover, each instance declaration has to conform to the kind determined by its family declaration. This implies that the number of parameters of an instance declaration matches the arity determined by the kind of the family.

A data family instance declaration can use the full expressiveness of ordinary data or newtype declarations:

  • Although, a data family is introduced with the keyword "data", a data family instance can use either data or newtype. For example:

    data family T a
    data    instance T Int  = T1 Int | T2 Bool
    newtype instance T Char = TC Bool
    

  • A data instance can use GADT syntax for the data constructors, and indeed can define a GADT. For example:

    data family G a b
    data instance G [a] b where
       G1 :: c -> G [Int] b
       G2 :: G [a] Bool
    

  • You can use a deriving clause on a data instance or newtype instance declaration.

Even if data families are defined as toplevel declarations, functions that perform different computations for different family instances may still need to be defined as methods of type classes. In particular, the following is not possible:

data family T a
data instance T Int  = A
data instance T Char = B
foo :: T a -> Int
foo A = 1             -- WRONG: These two equations together...
foo B = 2             -- ...will produce a type error.

Instead, you would have to write foo as a class operation, thus:

class Foo a where
  foo :: T a -> Int
instance Foo Int where
  foo A = 1
instance Foo Char where
  foo B = 2

(Given the functionality provided by GADTs (Generalised Algebraic Data Types), it might seem as if a definition, such as the above, should be feasible. However, type families are - in contrast to GADTs - are open; i.e., new instances can always be added, possibly in other modules. Supporting pattern matching across different data instances would require a form of extensible case construct.)

7.7.1.3. Overlap of data instances

The instance declarations of a data family used in a single program may not overlap at all, independent of whether they are associated or not. In contrast to type class instances, this is not only a matter of consistency, but one of type safety.

7.7.2. Synonym families

Type families appear in three flavours: (1) they can be defined as open families on the toplevel, (2) they can be defined as closed families on the toplevel, or (3) they can appear inside type classes (in which case they are known as associated type synonyms). Toplevel families are more general, as they lack the requirement for the type-indexes to coincide with the class parameters. However, associated type synonyms can lead to more clearly structured code and compiler warnings if some type instances were - possibly accidentally - omitted. In the following, we always discuss the general toplevel forms first and then cover the additional constraints placed on associated types. Note that closed associated type synonyms do not exist.

7.7.2.1. Type family declarations

Open indexed type families are introduced by a signature, such as

type family Elem c :: *

The special family distinguishes family from standard type declarations. The result kind annotation is optional and, as usual, defaults to * if omitted. An example is

type family Elem c

Parameters can also be given explicit kind signatures if needed. We call the number of parameters in a type family declaration, the family's arity, and all applications of a type family must be fully saturated w.r.t. to that arity. This requirement is unlike ordinary type synonyms and it implies that the kind of a type family is not sufficient to determine a family's arity, and hence in general, also insufficient to determine whether a type family application is well formed. As an example, consider the following declaration:

type family F a b :: * -> *   -- F's arity is 2,
                              -- although its overall kind is * -> * -> * -> *

Given this declaration the following are examples of well-formed and malformed types:

F Char [Int]       -- OK!  Kind: * -> *
F Char [Int] Bool  -- OK!  Kind: *
F IO Bool          -- WRONG: kind mismatch in the first argument
F Bool             -- WRONG: unsaturated application

7.7.2.2. Type instance declarations

Instance declarations of type families are very similar to standard type synonym declarations. The only two differences are that the keyword type is followed by instance and that some or all of the type arguments can be non-variable types, but may not contain forall types or type synonym families. However, data families are generally allowed, and type synonyms are allowed as long as they are fully applied and expand to a type that is admissible - these are the exact same requirements as for data instances. For example, the [e] instance for Elem is

type instance Elem [e] = e

Type family instance declarations are only legitimate when an appropriate family declaration is in scope - just like class instances require the class declaration to be visible. Moreover, each instance declaration has to conform to the kind determined by its family declaration, and the number of type parameters in an instance declaration must match the number of type parameters in the family declaration. Finally, the right-hand side of a type instance must be a monotype (i.e., it may not include foralls) and after the expansion of all saturated vanilla type synonyms, no synonyms, except family synonyms may remain.

7.7.2.3. Closed type families

A type family can also be declared with a where clause, defining the full set of equations for that family. For example:

type family F a where
  F Int  = Double
  F Bool = Char
  F a    = String

A closed type family's equations are tried in order, from top to bottom, when simplifying a type family application. In this example, we declare an instance for F such that F Int simplifies to Double, F Bool simplifies to Char, and for any other type a that is known not to be Int or Bool, F a simplifies to String. Note that GHC must be sure that a cannot unify with Int or Bool in that last case; if a programmer specifies just F a in their code, GHC will not be able to simplify the type. After all, a might later be instantiated with Int.

A closed type family's equations have the same restrictions as the equations for an open type family instances.

7.7.2.4. Type family examples

Here are some examples of admissible and illegal type instances:

type family F a :: *
type instance F [Int]              = Int         -- OK!
type instance F String             = Char        -- OK!
type instance F (F a)              = a           -- WRONG: type parameter mentions a type family
type instance F (forall a. (a, b)) = b           -- WRONG: a forall type appears in a type parameter
type instance F Float              = forall a.a  -- WRONG: right-hand side may not be a forall type
type family H a where                            -- OK!
  H Int  = Int
  H Bool = Bool
  H a    = String
type instance H Char = Char       -- WRONG: cannot have instances of closed family

type family G a b :: * -> *
type instance G Int            = (,)     -- WRONG: must be two type parameters
type instance G Int Char Float = Double  -- WRONG: must be two type parameters

7.7.2.5. Compatibility and apartness of type family equations

There must be some restrictions on the equations of type families, lest we define an ambiguous rewrite system. So, equations of open type families are restricted to be compatible. Two type patterns are compatible if

  1. all corresponding types in the patterns are apart, or

  2. the two patterns unify producing a substitution, and the right-hand sides are equal under that substitution.

Two types are considered apart if, for all possible substitutions, the types cannot reduce to a common reduct.

The first clause of "compatible" is the more straightforward one. It says that the patterns of two distinct type family instances cannot overlap. For example, the following is disallowed:

type instance F Int = Bool
type instance F Int = Char

The second clause is a little more interesting. It says that two overlapping type family instances are allowed if the right-hand sides coincide in the region of overlap. Some examples help here:

type instance F (a, Int) = [a]
type instance F (Int, b) = [b]   -- overlap permitted

type instance G (a, Int)  = [a]
type instance G (Char, a) = [a]  -- ILLEGAL overlap, as [Char] /= [Int]

Note that this compatibility condition is independent of whether the type family is associated or not, and it is not only a matter of consistency, but one of type safety.

The definition for "compatible" uses a notion of "apart", whose definition in turn relies on type family reduction. This condition of "apartness", as stated, is impossible to check, so we use this conservative approximation: two types are considered to be apart when the two types cannot be unified, even by a potentially infinite unifier. Allowing the unifier to be infinite disallows the following pair of instances:

type instance H x   x = Int
type instance H [x] x = Bool

The type patterns in this pair equal if x is replaced by an infinite nesting of lists. Rejecting instances such as these is necessary for type soundness.

Compatibility also affects closed type families. When simplifying an application of a closed type family, GHC will select an equation only when it is sure that no incompatible previous equation will ever apply. Here are some examples:

type family F a where
  F Int = Bool
  F a   = Char

type family G a where
  G Int = Int
  G a   = a

In the definition for F, the two equations are incompatible -- their patterns are not apart, and yet their right-hand sides do not coincide. Thus, before GHC selects the second equation, it must be sure that the first can never apply. So, the type F a does not simplify; only a type such as F Double will simplify to Char. In G, on the other hand, the two equations are compatible. Thus, GHC can ignore the first equation when looking at the second. So, G a will simplify to a.

However see Section 2.4.4, “Type, class and other declarations” for the overlap rules in GHCi.

7.7.2.6. Decidability of type synonym instances

In order to guarantee that type inference in the presence of type families decidable, we need to place a number of additional restrictions on the formation of type instance declarations (c.f., Definition 5 (Relaxed Conditions) of “Type Checking with Open Type Functions”). Instance declarations have the general form

type instance F t1 .. tn = t

where we require that for every type family application (G s1 .. sm) in t,

  1. s1 .. sm do not contain any type family constructors,

  2. the total number of symbols (data type constructors and type variables) in s1 .. sm is strictly smaller than in t1 .. tn, and

  3. for every type variable a, a occurs in s1 .. sm at most as often as in t1 .. tn.

These restrictions are easily verified and ensure termination of type inference. However, they are not sufficient to guarantee completeness of type inference in the presence of, so called, ''loopy equalities'', such as a ~ [F a], where a recursive occurrence of a type variable is underneath a family application and data constructor application - see the above mentioned paper for details.

If the option -XUndecidableInstances is passed to the compiler, the above restrictions are not enforced and it is on the programmer to ensure termination of the normalisation of type families during type inference.

7.7.3. Associated data and type families

A data or type synonym family can be declared as part of a type class, thus:

class GMapKey k where
  data GMap k :: * -> *
  ...

class Collects ce where
  type Elem ce :: *
  ...

When doing so, we (optionally) may drop the "family" keyword.

The type parameters must all be type variables, of course, and some (but not necessarily all) of then can be the class parameters. Each class parameter may only be used at most once per associated type, but some may be omitted and they may be in an order other than in the class head. Hence, the following contrived example is admissible:

  class C a b c where
    type T c a x :: *

Here c and a are class parameters, but the type is also indexed on a third parameter x.

7.7.3.1. Associated instances

When an associated data or type synonym family instance is declared within a type class instance, we (optionally) may drop the instance keyword in the family instance:

instance (GMapKey a, GMapKey b) => GMapKey (Either a b) where
  data GMap (Either a b) v = GMapEither (GMap a v) (GMap b v)
  ...

instance (Eq (Elem [e])) => Collects ([e]) where
  type Elem [e] = e
  ...

The most important point about associated family instances is that the type indexes corresponding to class parameters must be identical to the type given in the instance head; here this is the first argument of GMap, namely Either a b, which coincides with the only class parameter.

Instances for an associated family can only appear as part of instance declarations of the class in which the family was declared - just as with the equations of the methods of a class. Also in correspondence to how methods are handled, declarations of associated types can be omitted in class instances. If an associated family instance is omitted, the corresponding instance type is not inhabited; i.e., only diverging expressions, such as undefined, can assume the type.

Although it is unusual, there can be multiple instances for an associated family in a single instance declaration. For example, this is legitimate:

instance GMapKey Flob where
  data GMap Flob [v] = G1 v
  data GMap Flob Int = G2 Int
  ...

Here we give two data instance declarations, one in which the last parameter is [v], and one for which it is Int. Since you cannot give any subsequent instances for (GMap Flob ...), this facility is most useful when the free indexed parameter is of a kind with a finite number of alternatives (unlike *).

7.7.3.2. Associated type synonym defaults

It is possible for the class defining the associated type to specify a default for associated type instances. So for example, this is OK:

class IsBoolMap v where
  type Key v
  type instance Key v = Int

  lookupKey :: Key v -> v -> Maybe Bool

instance IsBoolMap [(Int, Bool)] where
  lookupKey = lookup

The instance keyword is optional.

There can also be multiple defaults for a single type, as long as they do not overlap:

class C a where
  type F a b
  type F a Int  = Bool
  type F a Bool = Int

A default declaration is not permitted for an associated data type.

7.7.3.3. Scoping of class parameters

The visibility of class parameters in the right-hand side of associated family instances depends solely on the parameters of the family. As an example, consider the simple class declaration

class C a b where
  data T a

Only one of the two class parameters is a parameter to the data family. Hence, the following instance declaration is invalid:

instance C [c] d where
  data T [c] = MkT (c, d)    -- WRONG!!  'd' is not in scope

Here, the right-hand side of the data instance mentions the type variable d that does not occur in its left-hand side. We cannot admit such data instances as they would compromise type safety.

7.7.3.4. Instance contexts and associated type and data instances

Associated type and data instance declarations do not inherit any context specified on the enclosing instance. For type instance declarations, it is unclear what the context would mean. For data instance declarations, it is unlikely a user would want the context repeated for every data constructor. The only place where the context might likely be useful is in a deriving clause of an associated data instance. However, even here, the role of the outer instance context is murky. So, for clarity, we just stick to the rule above: the enclosing instance context is ignored. If you need to use a non-trivial context on a derived instance, use a standalone deriving clause (at the top level).

7.7.4. Import and export

The rules for export lists (Haskell Report Section 5.2) needs adjustment for type families:

  • The form T(..), where T is a data family, names the family T and all the in-scope constructors (whether in scope qualified or unqualified) that are data instances of T.

  • The form T(.., ci, .., fj, ..), where T is a data family, names T and the specified constructors ci and fields fj as usual. The constructors and field names must belong to some data instance of T, but are not required to belong to the same instance.

  • The form C(..), where C is a class, names the class C and all its methods and associated types.

  • The form C(.., mi, .., type Tj, ..), where C is a class, names the class C, and the specified methods mi and associated types Tj. The types need a keyword "type" to distinguish them from data constructors.

7.7.4.1. Examples

Recall our running GMapKey class example:

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

instance (GMapKey a, GMapKey b) => GMapKey (Either a b) where
  data GMap (Either a b) v = GMapEither (GMap a v) (GMap b v)
  ...method declarations...

Here are some export lists and their meaning:

  • module GMap( GMapKey ): Exports just the class name.

  • module GMap( GMapKey(..) ): Exports the class, the associated type GMap and the member functions empty, lookup, and insert. The data constructors of GMap (in this case GMapEither) are not exported.

  • module GMap( GMapKey( type GMap, empty, lookup, insert ) ): Same as the previous item. Note the "type" keyword.

  • module GMap( GMapKey(..), GMap(..) ): Same as previous item, but also exports all the data constructors for GMap, namely GMapEither.

  • module GMap ( GMapKey( empty, lookup, insert), GMap(..) ): Same as previous item.

  • module GMap ( GMapKey, empty, lookup, insert, GMap(..) ): Same as previous item.

Two things to watch out for:

  • You cannot write GMapKey(type GMap(..)) — i.e., sub-component specifications cannot be nested. To specify GMap's data constructors, you have to list it separately.

  • Consider this example:

      module X where
        data family D
    
      module Y where
        import X
        data instance D Int = D1 | D2
    

    Module Y exports all the entities defined in Y, namely the data constructors D1 and D2, but not the data family D. That (annoyingly) means that you cannot selectively import Y selectively, thus "import Y( D(D1,D2) )", because Y does not export D. Instead you should list the exports explicitly, thus:

         module Y( D(..) ) where ...
    or   module Y( module Y, D ) where ...
    

7.7.4.2. Instances

Family instances are implicitly exported, just like class instances. However, this applies only to the heads of instances, not to the data constructors an instance defines.

7.7.5. Type families and instance declarations

Type families require us to extend the rules for the form of instance heads, which are given in Section 7.6.3.2, “Relaxed rules for the instance head”. Specifically:

  • Data type families may appear in an instance head

  • Type synonym families may not appear (at all) in an instance head

The reason for the latter restriction is that there is no way to check for instance matching. Consider

   type family F a
   type instance F Bool = Int

   class C a

   instance C Int
   instance C (F a)

Now a constraint (C (F Bool)) would match both instances. The situation is especially bad because the type instance for F Bool might be in another module, or even in a module that is not yet written.

However, type class instances of instances of data families can be defined much like any other data type. For example, we can say

data instance T Int = T1 Int | T2 Bool
instance Eq (T Int) where
  (T1 i) == (T1 j) = i==j
  (T2 i) == (T2 j) = i==j
  _      == _      = False

Note that class instances are always for particular instances of a data family and never for an entire family as a whole. This is for essentially the same reasons that we cannot define a toplevel function that performs pattern matching on the data constructors of different instances of a single type family. It would require a form of extensible case construct.

Data instance declarations can also have deriving clauses. For example, we can write

data GMap () v = GMapUnit (Maybe v)
               deriving Show

which implicitly defines an instance of the form

instance Show v => Show (GMap () v) where ...