Commit 2da06d7c authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu

User manual update, as prodded by #10760.

This clarifies that kind variables are inputs to type families
and can be used to distinguish instances.
parent b4ed1300
...@@ -6247,7 +6247,18 @@ F Char [Int] Bool -- OK! Kind: * ...@@ -6247,7 +6247,18 @@ F Char [Int] Bool -- OK! Kind: *
F IO Bool -- WRONG: kind mismatch in the first argument F IO Bool -- WRONG: kind mismatch in the first argument
F Bool -- WRONG: unsaturated application F Bool -- WRONG: unsaturated application
</programlisting> </programlisting>
</para> </para>
<para>
The result kind annotation is optional and defaults to
<literal>*</literal> (like argument kinds) if
omitted. Polykinded type families can be
declared using a parameter in the kind annotation:
<programlisting>
type family F a :: k
</programlisting>
In this case the kind parameter <literal>k</literal> is actually an implicit
parameter of the type family.
</sect3> </sect3>
<sect3 id="type-instance-declarations"> <sect3 id="type-instance-declarations">
...@@ -6365,7 +6376,7 @@ type instance G Int Char Float = Double -- WRONG: must be two type parameters ...@@ -6365,7 +6376,7 @@ type instance G Int Char Float = Double -- WRONG: must be two type parameters
are restricted to be <firstterm>compatible</firstterm>. Two type patterns are restricted to be <firstterm>compatible</firstterm>. Two type patterns
are compatible if are compatible if
<orderedlist> <orderedlist>
<listitem><para>all corresponding types in the patterns are <firstterm>apart</firstterm>, or</para></listitem> <listitem><para>all corresponding types and implicit kinds in the patterns are <firstterm>apart</firstterm>, or</para></listitem>
<listitem><para>the two patterns unify producing a substitution, and the right-hand sides are equal under that substitution.</para></listitem> <listitem><para>the two patterns unify producing a substitution, and the right-hand sides are equal under that substitution.</para></listitem>
</orderedlist> </orderedlist>
Two types are considered <firstterm>apart</firstterm> if, for all possible Two types are considered <firstterm>apart</firstterm> if, for all possible
...@@ -6392,7 +6403,17 @@ type instance G (Char, a) = [a] -- ILLEGAL overlap, as [Char] /= [Int] ...@@ -6392,7 +6403,17 @@ type instance G (Char, a) = [a] -- ILLEGAL overlap, as [Char] /= [Int]
</programlisting> </programlisting>
Note that this compatibility condition is independent of whether the type family 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 is associated or not, and it is not only a matter of consistency, but
one of type safety. </para> one of type safety. </para>
<para>For a polykinded type family, the kinds are checked for
apartness just like types. For example, the following is accepted:
<programlisting>
type family J a :: k
type instance J Int = Bool
type instance J Int = Maybe
</programlisting>
These instances are compatible because they differ in their implicit kind parameter; the first uses <literal>*</literal> while the second uses <literal>* -> *</literal>.</para>
<para> <para>
The definition for "compatible" uses a notion of "apart", whose definition The definition for "compatible" uses a notion of "apart", whose definition
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment