diff options
| author | Richard Eisenberg <eir@cis.upenn.edu> | 2015-08-11 09:05:30 -0400 |
|---|---|---|
| committer | Richard Eisenberg <eir@cis.upenn.edu> | 2015-08-11 09:05:30 -0400 |
| commit | 2da06d7c3fb0da894f5b5a6770c4e41aeee012cd (patch) | |
| tree | 7e81eb3c86da9b16a7f660c85de750ac47b70959 | |
| parent | b4ed13000cf0cbbb5916727dad018d91c10f1fd8 (diff) | |
| download | haskell-2da06d7c3fb0da894f5b5a6770c4e41aeee012cd.tar.gz | |
User manual update, as prodded by #10760.
This clarifies that kind variables are inputs to type families
and can be used to distinguish instances.
| -rw-r--r-- | docs/users_guide/glasgow_exts.xml | 27 |
1 files changed, 24 insertions, 3 deletions
diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml index d1a908ee5c..8b597da0a0 100644 --- a/docs/users_guide/glasgow_exts.xml +++ b/docs/users_guide/glasgow_exts.xml @@ -6247,7 +6247,18 @@ F Char [Int] Bool -- OK! Kind: * F IO Bool -- WRONG: kind mismatch in the first argument F Bool -- WRONG: unsaturated application </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 id="type-instance-declarations"> @@ -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 compatible if <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> </orderedlist> 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] </programlisting> 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. </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> The definition for "compatible" uses a notion of "apart", whose definition |