+data family GMap k :: * -> *
+</programlisting>
+ The special <literal>family</literal> distinguishes family from standard
+ data declarations. The result kind annotation is optional and, as
+ usual, defaults to <literal>*</literal> if omitted. An example is
+<programlisting>
+data family Array e
+</programlisting>
+ 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 <literal>Array</literal> alternatively with
+<programlisting>
+data family Array :: * -> *
+</programlisting>
+ </para>
+
+ <sect4 id="assoc-data-family-decl">
+ <title>Associated data family declarations</title>
+ <para>
+ When a data family is declared as part of a type class, we drop
+ the <literal>family</literal> special. The <literal>GMap</literal>
+ declaration takes the following form
+<programlisting>
+class GMapKey k where
+ data GMap k :: * -> *
+ ...
+</programlisting>
+ In contrast to toplevel declarations, named arguments must be used for
+ all type parameters that are to be used as type-indexes. Moreover,
+ the argument names must be 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:
+<programlisting>
+ class C a b c where
+ data T c a :: *
+</programlisting>
+ </para>
+ </sect4>
+ </sect3>
+
+ <sect3 id="data-instance-declarations">
+ <title>Data instance declarations</title>
+
+ <para>
+ Instance declarations of data and newtype families are very similar to
+ standard data and newtype declarations. The only two differences are
+ that the keyword <literal>data</literal> or <literal>newtype</literal>
+ is followed by <literal>instance</literal> 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 <literal>Either</literal>
+ instance for <literal>GMap</literal> is
+<programlisting>
+data instance GMap (Either a b) v = GMapEither (GMap a v) (GMap b v)
+</programlisting>
+ In this example, the declaration has only one variant. In general, it
+ can be any number.
+ </para>
+ <para>
+ Data and newtype instance declarations are only permitted when an
+ appropriate family declaration is in scope - just as a class instance declaratoin
+ 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.
+ </para>
+ <para>
+ A data family instance declaration can use the full exprssiveness of
+ ordinary <literal>data</literal> or <literal>newtype</literal> declarations:
+ <itemizedlist>
+ <listitem><para> Although, a data family is <emphasis>introduced</emphasis> with
+ the keyword "<literal>data</literal>", a data family <emphasis>instance</emphasis> can
+ use either <literal>data</literal> or <literal>newtype</literal>. For example:
+<programlisting>
+data family T a
+data instance T Int = T1 Int | T2 Bool
+newtype instance T Char = TC Bool
+</programlisting>
+ </para></listitem>
+ <listitem><para> A <literal>data instance</literal> can use GADT syntax for the data constructors,
+ and indeed can define a GADT. For example:
+<programlisting>
+data family G a b
+data instance G [a] b where
+ G1 :: c -> G [Int] b
+ G2 :: G [a] Bool
+</programlisting>
+ </para></listitem>
+ <listitem><para> You can use a <literal>deriving</literal> clause on a
+ <literal>data instance</literal> or <literal>newtype instance</literal>
+ declaration.
+ </para></listitem>
+ </itemizedlist>
+ </para>
+
+ <para>
+ Even if type 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:
+<programlisting>
+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.
+</programlisting>
+Instead, you would have to write <literal>foo</literal> as a class operation, thus:
+<programlisting>
+class C a where
+ foo :: T a -> Int
+instance Foo Int where
+ foo A = 1
+instance Foo Char where
+ foo B = 2
+</programlisting>
+ (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
+ <emphasis>open;</emphasis> 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.)
+ </para>
+
+ <sect4 id="assoc-data-inst">
+ <title>Associated data instances</title>
+ <para>
+ When an associated data family instance is declared within a type
+ class instance, we drop the <literal>instance</literal> keyword in the
+ family instance. So, the <literal>Either</literal> instance
+ for <literal>GMap</literal> becomes:
+<programlisting>
+instance (GMapKey a, GMapKey b) => GMapKey (Either a b) where
+ data GMap (Either a b) v = GMapEither (GMap a v) (GMap b v)
+ ...
+</programlisting>
+ 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 <literal>GMap</literal>, namely <literal>Either a b</literal>,
+ which coincides with the only class parameter. Any parameters to the
+ family constructor that do not correspond to class parameters, need to
+ be variables in every instance; here this is the
+ variable <literal>v</literal>.
+ </para>
+ <para>
+ Instances for an associated family can only appear as part of
+ instances 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 <literal>undefined</literal>, can assume the type.
+ </para>
+ </sect4>
+
+ <sect4 id="scoping-class-params">
+ <title>Scoping of class parameters</title>
+ <para>
+ In the case of multi-parameter type classes, the visibility of class
+ parameters in the right-hand side of associated family instances
+ depends <emphasis>solely</emphasis> on the parameters of the data
+ family. As an example, consider the simple class declaration
+<programlisting>
+class C a b where
+ data T a
+</programlisting>
+ Only one of the two class parameters is a parameter to the data
+ family. Hence, the following instance declaration is invalid:
+<programlisting>
+instance C [c] d where
+ data T [c] = MkT (c, d) -- WRONG!! 'd' is not in scope
+</programlisting>
+ Here, the right-hand side of the data instance mentions the type
+ variable <literal>d</literal> that does not occur in its left-hand
+ side. We cannot admit such data instances as they would compromise
+ type safety.
+ </para>
+ </sect4>
+
+ <sect4 id="family-class-inst">
+ <title>Type class instances of family instances</title>
+ <para>
+ Type class instances of instances of data families can be defined as
+ usual, and in particular data instance declarations can
+ have <literal>deriving</literal> clauses. For example, we can write
+<programlisting>
+data GMap () v = GMapUnit (Maybe v)
+ deriving Show
+</programlisting>
+ which implicitly defines an instance of the form
+<programlisting>
+instance Show v => Show (GMap () v) where ...
+</programlisting>
+ </para>
+ <para>
+ Note that class instances are always for
+ particular <emphasis>instances</emphasis> 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 <emphasis>different</emphasis> instances of a single type family.
+ It would require a form of extensible case construct.
+ </para>
+ </sect4>
+
+ <sect4 id="data-family-overlap">
+ <title>Overlap of data instances</title>
+ <para>
+ 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.
+ </para>
+ </sect4>
+
+ </sect3>
+
+ <sect3 id="data-family-import-export">
+ <title>Import and export</title>
+
+ <para>
+ The association of data constructors with type families is more dynamic
+ than that is the case with standard data and newtype declarations. In
+ the standard case, the notation <literal>T(..)</literal> in an import or
+ export list denotes the type constructor and all the data constructors
+ introduced in its declaration. However, a family declaration never
+ introduces any data constructors; instead, data constructors are
+ introduced by family instances. As a result, which data constructors
+ are associated with a type family depends on the currently visible
+ instance declarations for that family. Consequently, an import or
+ export item of the form <literal>T(..)</literal> denotes the family
+ constructor and all currently visible data constructors - in the case of
+ an export item, these may be either imported or defined in the current
+ module. The treatment of import and export items that explicitly list
+ data constructors, such as <literal>GMap(GMapEither)</literal>, is
+ analogous.
+ </para>
+
+ <sect4 id="data-family-impexp-assoc">
+ <title>Associated families</title>
+ <para>
+ As expected, an import or export item of the
+ form <literal>C(..)</literal> denotes all of the class' methods and
+ associated types. However, when associated types are explicitly
+ listed as subitems of a class, we need some new syntax, as uppercase
+ identifiers as subitems are usually data constructors, not type
+ constructors. To clarify that we denote types here, each associated
+ type name needs to be prefixed by the keyword <literal>type</literal>.
+ So for example, when explicitly listing the components of
+ the <literal>GMapKey</literal> class, we write <literal>GMapKey(type
+ GMap, empty, lookup, insert)</literal>.
+ </para>
+ </sect4>
+
+ <sect4 id="data-family-impexp-examples">
+ <title>Examples</title>
+ <para>
+ Assuming our running <literal>GMapKey</literal> class example, let us
+ look at some export lists and their meaning:
+ <itemizedlist>
+ <listitem>
+ <para><literal>module GMap (GMapKey) where...</literal>: Exports
+ just the class name.</para>
+ </listitem>
+ <listitem>
+ <para><literal>module GMap (GMapKey(..)) where...</literal>:
+ Exports the class, the associated type <literal>GMap</literal>
+ and the member
+ functions <literal>empty</literal>, <literal>lookup</literal>,
+ and <literal>insert</literal>. None of the data constructors is
+ exported.</para>
+ </listitem>
+ <listitem>
+ <para><literal>module GMap (GMapKey(..), GMap(..))
+ where...</literal>: As before, but also exports all the data
+ constructors <literal>GMapInt</literal>,
+ <literal>GMapChar</literal>,
+ <literal>GMapUnit</literal>, <literal>GMapPair</literal>,
+ and <literal>GMapUnit</literal>.</para>
+ </listitem>
+ <listitem>
+ <para><literal>module GMap (GMapKey(empty, lookup, insert),
+ GMap(..)) where...</literal>: As before.</para>
+ </listitem>
+ <listitem>
+ <para><literal>module GMap (GMapKey, empty, lookup, insert, GMap(..))
+ where...</literal>: As before.</para>
+ </listitem>
+ </itemizedlist>
+ </para>
+ <para>
+ Finally, you can write <literal>GMapKey(type GMap)</literal> to denote
+ both the class <literal>GMapKey</literal> as well as its associated
+ type <literal>GMap</literal>. However, you cannot
+ write <literal>GMapKey(type GMap(..))</literal> — i.e.,
+ sub-component specifications cannot be nested. To
+ specify <literal>GMap</literal>'s data constructors, you have to list
+ it separately.
+ </para>
+ </sect4>
+
+ <sect4 id="data-family-impexp-instances">
+ <title>Instances</title>
+ <para>
+ 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.
+ </para>
+ </sect4>
+
+ </sect3>
+
+</sect2>
+
+<sect2 id="synonym-families">
+ <title>Synonym families</title>
+
+ <para>
+ Type 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 type synonyms). 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.
+ </para>
+
+ <sect3 id="type-family-declarations">
+ <title>Type family declarations</title>
+
+ <para>
+ Indexed type families are introduced by a signature, such as
+<programlisting>
+type family Elem c :: *
+</programlisting>
+ The special <literal>family</literal> distinguishes family from standard
+ type declarations. The result kind annotation is optional and, as
+ usual, defaults to <literal>*</literal> if omitted. An example is
+<programlisting>
+type family Elem c
+</programlisting>
+ 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:
+<programlisting>
+type family F a b :: * -> * -- F's arity is 2,
+ -- although its overall kind is * -> * -> * -> *
+</programlisting>
+ Given this declaration the following are examples of well-formed and
+ malformed types:
+<programlisting>
+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