[project @ 2005-10-26 13:03:39 by simonpj]

Improve documentation of typeclass extensions; merge to stable if it goes easily

1 files changed, 265 insertions, 238 deletions

diff --git a/ghc/docs/users_guide/glasgow_exts.xml b/ghc/docs/users_guide/glasgow_exts.xml
index c9dfaf0a12..36b7bf8f1f 100644
--- a/ghc/docs/users_guide/glasgow_exts.xml
+++ b/ghc/docs/users_guide/glasgow_exts.xml
@@ -1429,19 +1429,20 @@ declarations.  Define your own instances!
 <title>Class declarations</title>
 
 <para>
-This section documents GHC's implementation of multi-parameter type
-classes.  There's lots of background in the paper <ulink
+This section, and the next one, documents GHC's type-class extensions.
+There's lots of background in the paper <ulink
 url="http://research.microsoft.com/~simonpj/Papers/type-class-design-space" >Type
 classes: exploring the design space</ulink > (Simon Peyton Jones, Mark
 Jones, Erik Meijer).
 </para>
 <para>
-There are the following constraints on class declarations:
-<orderedlist>
-<listitem>
+All the extensions are enabled by the <option>-fglasgow-exts</option> flag.
+</para>
 
+<sect3>
+<title>Multi-parameter type classes</title>
 <para>
- <emphasis>Multi-parameter type classes are permitted</emphasis>. For example:
+Multi-parameter type classes are permitted. For example:
 
 
 <programlisting>
@@ -1450,39 +1451,16 @@ There are the following constraints on class declarations:
     ...etc.
 </programlisting>
 
-
-
 </para>
-</listitem>
-<listitem>
-
-<para>
- <emphasis>The class hierarchy must be acyclic</emphasis>.  However, the definition
-of "acyclic" involves only the superclass relationships.  For example,
-this is OK:
-
-
-<programlisting>
-  class C a where {
-    op :: D b => a -> b -> b
-  }
-
-  class C a => D a where { ... }
-</programlisting>
-
-
-Here, <literal>C</literal> is a superclass of <literal>D</literal>, but it's OK for a
-class operation <literal>op</literal> of <literal>C</literal> to mention <literal>D</literal>.  (It
-would not be OK for <literal>D</literal> to be a superclass of <literal>C</literal>.)
+</sect3>
 
-</para>
-</listitem>
-<listitem>
+<sect3>
+<title>The superclasses of a class declaration</title>
 
 <para>
- <emphasis>There are no restrictions on the context in a class declaration
+There are no restrictions on the context in a class declaration
 (which introduces superclasses), except that the class hierarchy must
-be acyclic</emphasis>.  So these class declarations are OK:
+be acyclic.  So these class declarations are OK:
 
 
 <programlisting>
@@ -1495,62 +1473,33 @@ be acyclic</emphasis>.  So these class declarations are OK:
 
 
 </para>
-</listitem>
-
-<listitem>
-
 <para>
- <emphasis>All of the class type variables must be reachable (in the sense 
-mentioned in <xref linkend="type-restrictions"/>)
-from the free variables of each method type
-</emphasis>.  For example:
+As in Haskell 98, The class hierarchy must be acyclic.  However, the definition
+of "acyclic" involves only the superclass relationships.  For example,
+this is OK:
 
 
 <programlisting>
-  class Coll s a where
-    empty  :: s
-    insert :: s -> a -> s
-</programlisting>
-
-
-is not OK, because the type of <literal>empty</literal> doesn't mention
-<literal>a</literal>.  This rule is a consequence of Rule 1(a), above, for
-types, and has the same motivation.
-
-Sometimes, offending class declarations exhibit misunderstandings.  For
-example, <literal>Coll</literal> might be rewritten
-
+  class C a where {
+    op :: D b => a -> b -> b
+  }
 
-<programlisting>
-  class Coll s a where
-    empty  :: s a
-    insert :: s a -> a -> s a
+  class C a => D a where { ... }
 </programlisting>
 
 
-which makes the connection between the type of a collection of
-<literal>a</literal>'s (namely <literal>(s a)</literal>) and the element type <literal>a</literal>.
-Occasionally this really doesn't work, in which case you can split the
-class like this:
-
-
-<programlisting>
-  class CollE s where
-    empty  :: s
-
-  class CollE s => Coll s a where
-    insert :: s -> a -> s
-</programlisting>
+Here, <literal>C</literal> is a superclass of <literal>D</literal>, but it's OK for a
+class operation <literal>op</literal> of <literal>C</literal> to mention <literal>D</literal>.  (It
+would not be OK for <literal>D</literal> to be a superclass of <literal>C</literal>.)
+</para>
+</sect3>
 
 
-</para>
-</listitem>
 
-</orderedlist>
-</para>
 
 <sect3 id="class-method-types">
 <title>Class method types</title>
+
 <para>
 Haskell 98 prohibits class method types to mention constraints on the
 class type variable, thus:
@@ -1562,186 +1511,120 @@ class type variable, thus:
 The type of <literal>elem</literal> is illegal in Haskell 98, because it
 contains the constraint <literal>Eq a</literal>, constrains only the 
 class type variable (in this case <literal>a</literal>).
+GHC lifts this restriction.
 </para>
-<para>
-With the <option>-fglasgow-exts</option> GHC lifts this restriction.
-</para>
+
 
 </sect3>
 
-</sect2>
 
-<sect2 id="type-restrictions">
-<title>Type signatures</title>
+<sect3 id="functional-dependencies">
+<title>Functional dependencies
+</title>
 
-<sect3><title>The context of a type signature</title>
+<para> Functional dependencies are implemented as described by Mark Jones
+in &ldquo;<ulink url="http://www.cse.ogi.edu/~mpj/pubs/fundeps.html">Type Classes with Functional Dependencies</ulink>&rdquo;, Mark P. Jones, 
+In Proceedings of the 9th European Symposium on Programming, 
+ESOP 2000, Berlin, Germany, March 2000, Springer-Verlag LNCS 1782,
+.
+</para>
 <para>
-Unlike Haskell 98, constraints in types do <emphasis>not</emphasis> have to be of
-the form <emphasis>(class type-variable)</emphasis> or
-<emphasis>(class (type-variable type-variable ...))</emphasis>.  Thus,
-these type signatures are perfectly OK
+Functional dependencies are introduced by a vertical bar in the syntax of a 
+class declaration;  e.g. 
 <programlisting>
-  g :: Eq [a] => ...
-  g :: Ord (T a ()) => ...
+  class (Monad m) => MonadState s m | m -> s where ...
+
+  class Foo a b c | a b -> c where ...
 </programlisting>
+There should be more documentation, but there isn't (yet).  Yell if you need it.
 </para>
 <para>
-GHC imposes the following restrictions on the constraints in a type signature.
-Consider the type:
+In a class declaration, all of the class type variables must be reachable (in the sense 
+mentioned in <xref linkend="type-restrictions"/>)
+from the free variables of each method type.
+For example:
 
 <programlisting>
-  forall tv1..tvn (c1, ...,cn) => type
+  class Coll s a where
+    empty  :: s
+    insert :: s -> a -> s
 </programlisting>
 
-(Here, we write the "foralls" explicitly, although the Haskell source
-language omits them; in Haskell 98, all the free type variables of an
-explicit source-language type signature are universally quantified,
-except for the class type variables in a class declaration.  However,
-in GHC, you can give the foralls if you want.  See <xref linkend="universal-quantification"/>).
-</para>
-
-<para>
-
-<orderedlist>
-<listitem>
-
-<para>
- <emphasis>Each universally quantified type variable
-<literal>tvi</literal> must be reachable from <literal>type</literal></emphasis>.
-
-A type variable <literal>a</literal> is "reachable" if it it appears
-in the same constraint as either a type variable free in in
-<literal>type</literal>, or another reachable type variable.  
-A value with a type that does not obey 
-this reachability restriction cannot be used without introducing
-ambiguity; that is why the type is rejected.
-Here, for example, is an illegal type:
-
-
+is not OK, because the type of <literal>empty</literal> doesn't mention
+<literal>a</literal>.  Functional dependencies can make the type variable
+reachable:
 <programlisting>
-  forall a. Eq a => Int
+  class Coll s a | s -> a where
+    empty  :: s
+    insert :: s -> a -> s
 </programlisting>
 
+Alternatively <literal>Coll</literal> might be rewritten
 
-When a value with this type was used, the constraint <literal>Eq tv</literal>
-would be introduced where <literal>tv</literal> is a fresh type variable, and
-(in the dictionary-translation implementation) the value would be
-applied to a dictionary for <literal>Eq tv</literal>.  The difficulty is that we
-can never know which instance of <literal>Eq</literal> to use because we never
-get any more information about <literal>tv</literal>.
-</para>
-<para>
-Note
-that the reachability condition is weaker than saying that <literal>a</literal> is
-functionally dependent on a type variable free in
-<literal>type</literal> (see <xref
-linkend="functional-dependencies"/>).  The reason for this is there
-might be a "hidden" dependency, in a superclass perhaps.  So
-"reachable" is a conservative approximation to "functionally dependent".
-For example, consider:
 <programlisting>
-  class C a b | a -> b where ...
-  class C a b => D a b where ...
-  f :: forall a b. D a b => a -> a
+  class Coll s a where
+    empty  :: s a
+    insert :: s a -> a -> s a
 </programlisting>
-This is fine, because in fact <literal>a</literal> does functionally determine <literal>b</literal>
-but that is not immediately apparent from <literal>f</literal>'s type.
-</para>
-</listitem>
-<listitem>
 
-<para>
- <emphasis>Every constraint <literal>ci</literal> must mention at least one of the
-universally quantified type variables <literal>tvi</literal></emphasis>.
 
-For example, this type is OK because <literal>C a b</literal> mentions the
-universally quantified type variable <literal>b</literal>:
+which makes the connection between the type of a collection of
+<literal>a</literal>'s (namely <literal>(s a)</literal>) and the element type <literal>a</literal>.
+Occasionally this really doesn't work, in which case you can split the
+class like this:
 
 
 <programlisting>
-  forall a. C a b => burble
-</programlisting>
-
+  class CollE s where
+    empty  :: s
 
-The next type is illegal because the constraint <literal>Eq b</literal> does not
-mention <literal>a</literal>:
+  class CollE s => Coll s a where
+    insert :: s -> a -> s
+</programlisting>
+</para>
+</sect3>
 
 
-<programlisting>
-  forall a. Eq b => burble
-</programlisting>
 
 
-The reason for this restriction is milder than the other one.  The
-excluded types are never useful or necessary (because the offending
-context doesn't need to be witnessed at this point; it can be floated
-out).  Furthermore, floating them out increases sharing. Lastly,
-excluding them is a conservative choice; it leaves a patch of
-territory free in case we need it later.
 
-</para>
-</listitem>
+</sect2>
 
-</orderedlist>
+<sect2 id="instance-decls">
+<title>Instance declarations</title>
 
-</para>
-</sect3>
+<sect3 id="instance-heads">
+<title>Instance heads</title>
 
-<sect3 id="hoist">
-<title>For-all hoisting</title>
 <para>
-It is often convenient to use generalised type synonyms (see <xref linkend="type-synonyms"/>) at the right hand
-end of an arrow, thus:
-<programlisting>
-  type Discard a = forall b. a -> b -> a
-
-  g :: Int -> Discard Int
-  g x y z = x+y
-</programlisting>
-Simply expanding the type synonym would give
-<programlisting>
-  g :: Int -> (forall b. Int -> b -> Int)
-</programlisting>
-but GHC "hoists" the <literal>forall</literal> to give the isomorphic type
-<programlisting>
-  g :: forall b. Int -> Int -> b -> Int
-</programlisting>
-In general, the rule is this: <emphasis>to determine the type specified by any explicit
-user-written type (e.g. in a type signature), GHC expands type synonyms and then repeatedly
-performs the transformation:</emphasis>
-<programlisting>
-  <emphasis>type1</emphasis> -> forall a1..an. <emphasis>context2</emphasis> => <emphasis>type2</emphasis>
-==>
-  forall a1..an. <emphasis>context2</emphasis> => <emphasis>type1</emphasis> -> <emphasis>type2</emphasis>
-</programlisting>
-(In fact, GHC tries to retain as much synonym information as possible for use in
-error messages, but that is a usability issue.)  This rule applies, of course, whether
-or not the <literal>forall</literal> comes from a synonym. For example, here is another
-valid way to write <literal>g</literal>'s type signature:
-<programlisting>
-  g :: Int -> Int -> forall b. b -> Int
-</programlisting>
+The <emphasis>head</emphasis> of an instance declaration is the part to the
+right of the "<literal>=&gt;</literal>".  In Haskell 98 the head of an instance
+declaration
+must be of the form <literal>C (T a1 ... an)</literal>, where
+<literal>C</literal> is the class, <literal>T</literal> is a type constructor,
+and the <literal>a1 ... an</literal> are distinct type variables.
 </para>
 <para>
-When doing this hoisting operation, GHC eliminates duplicate constraints.  For
-example:
-<programlisting>
-  type Foo a = (?x::Int) => Bool -> a
-  g :: Foo (Foo Int)
-</programlisting>
-means
+The <option>-fglasgow-exts</option> flag lifts this restriction and allows the
+instance head to be of form <literal>C t1 ... tn</literal> where <literal>t1
+... tn</literal> are arbitrary types (provided, of course, everything is
+well-kinded).  In particular, types <literal>ti</literal> can be type variables
+or structured types, and can contain repeated occurrences of a single type
+variable.
+Examples:
 <programlisting>
-  g :: (?x::Int) => Bool -> Bool -> Int
+  instance Eq (T a a) where ...
+	-- Repeated type variable
+
+  instance Eq (S [a]) where ...
+	-- Structured type
+
+  instance C Int [a] where ...
+	-- Multiple parameters
 </programlisting>
 </para>
 </sect3>
 
-
-</sect2>
-
-<sect2 id="instance-decls">
-<title>Instance declarations</title>
-
 <sect3 id="instance-overlap">
 <title>Overlapping instances</title>
 <para>
@@ -1892,7 +1775,7 @@ but this is not:
 <programlisting>
   instance F a where ...
 </programlisting>
-Note that instance heads <emphasis>may</emphasis> contain repeated type variables.
+Note that instance heads may contain repeated type variables (<xref linkend="instance-heads"/>).
 For example, this is OK:
 <programlisting>
   instance Stateful (ST s) (MutVar s) where ...
@@ -1981,6 +1864,174 @@ allowing these idioms interesting idioms.
 
 </sect2>
 
+<sect2 id="type-restrictions">
+<title>Type signatures</title>
+
+<sect3><title>The context of a type signature</title>
+<para>
+Unlike Haskell 98, constraints in types do <emphasis>not</emphasis> have to be of
+the form <emphasis>(class type-variable)</emphasis> or
+<emphasis>(class (type-variable type-variable ...))</emphasis>.  Thus,
+these type signatures are perfectly OK
+<programlisting>
+  g :: Eq [a] => ...
+  g :: Ord (T a ()) => ...
+</programlisting>
+</para>
+<para>
+GHC imposes the following restrictions on the constraints in a type signature.
+Consider the type:
+
+<programlisting>
+  forall tv1..tvn (c1, ...,cn) => type
+</programlisting>
+
+(Here, we write the "foralls" explicitly, although the Haskell source
+language omits them; in Haskell 98, all the free type variables of an
+explicit source-language type signature are universally quantified,
+except for the class type variables in a class declaration.  However,
+in GHC, you can give the foralls if you want.  See <xref linkend="universal-quantification"/>).
+</para>
+
+<para>
+
+<orderedlist>
+<listitem>
+
+<para>
+ <emphasis>Each universally quantified type variable
+<literal>tvi</literal> must be reachable from <literal>type</literal></emphasis>.
+
+A type variable <literal>a</literal> is "reachable" if it it appears
+in the same constraint as either a type variable free in in
+<literal>type</literal>, or another reachable type variable.  
+A value with a type that does not obey 
+this reachability restriction cannot be used without introducing
+ambiguity; that is why the type is rejected.
+Here, for example, is an illegal type:
+
+
+<programlisting>
+  forall a. Eq a => Int
+</programlisting>
+
+
+When a value with this type was used, the constraint <literal>Eq tv</literal>
+would be introduced where <literal>tv</literal> is a fresh type variable, and
+(in the dictionary-translation implementation) the value would be
+applied to a dictionary for <literal>Eq tv</literal>.  The difficulty is that we
+can never know which instance of <literal>Eq</literal> to use because we never
+get any more information about <literal>tv</literal>.
+</para>
+<para>
+Note
+that the reachability condition is weaker than saying that <literal>a</literal> is
+functionally dependent on a type variable free in
+<literal>type</literal> (see <xref
+linkend="functional-dependencies"/>).  The reason for this is there
+might be a "hidden" dependency, in a superclass perhaps.  So
+"reachable" is a conservative approximation to "functionally dependent".
+For example, consider:
+<programlisting>
+  class C a b | a -> b where ...
+  class C a b => D a b where ...
+  f :: forall a b. D a b => a -> a
+</programlisting>
+This is fine, because in fact <literal>a</literal> does functionally determine <literal>b</literal>
+but that is not immediately apparent from <literal>f</literal>'s type.
+</para>
+</listitem>
+<listitem>
+
+<para>
+ <emphasis>Every constraint <literal>ci</literal> must mention at least one of the
+universally quantified type variables <literal>tvi</literal></emphasis>.
+
+For example, this type is OK because <literal>C a b</literal> mentions the
+universally quantified type variable <literal>b</literal>:
+
+
+<programlisting>
+  forall a. C a b => burble
+</programlisting>
+
+
+The next type is illegal because the constraint <literal>Eq b</literal> does not
+mention <literal>a</literal>:
+
+
+<programlisting>
+  forall a. Eq b => burble
+</programlisting>
+
+
+The reason for this restriction is milder than the other one.  The
+excluded types are never useful or necessary (because the offending
+context doesn't need to be witnessed at this point; it can be floated
+out).  Furthermore, floating them out increases sharing. Lastly,
+excluding them is a conservative choice; it leaves a patch of
+territory free in case we need it later.
+
+</para>
+</listitem>
+
+</orderedlist>
+
+</para>
+</sect3>
+
+<sect3 id="hoist">
+<title>For-all hoisting</title>
+<para>
+It is often convenient to use generalised type synonyms (see <xref linkend="type-synonyms"/>) at the right hand
+end of an arrow, thus:
+<programlisting>
+  type Discard a = forall b. a -> b -> a
+
+  g :: Int -> Discard Int
+  g x y z = x+y
+</programlisting>
+Simply expanding the type synonym would give
+<programlisting>
+  g :: Int -> (forall b. Int -> b -> Int)
+</programlisting>
+but GHC "hoists" the <literal>forall</literal> to give the isomorphic type
+<programlisting>
+  g :: forall b. Int -> Int -> b -> Int
+</programlisting>
+In general, the rule is this: <emphasis>to determine the type specified by any explicit
+user-written type (e.g. in a type signature), GHC expands type synonyms and then repeatedly
+performs the transformation:</emphasis>
+<programlisting>
+  <emphasis>type1</emphasis> -> forall a1..an. <emphasis>context2</emphasis> => <emphasis>type2</emphasis>
+==>
+  forall a1..an. <emphasis>context2</emphasis> => <emphasis>type1</emphasis> -> <emphasis>type2</emphasis>
+</programlisting>
+(In fact, GHC tries to retain as much synonym information as possible for use in
+error messages, but that is a usability issue.)  This rule applies, of course, whether
+or not the <literal>forall</literal> comes from a synonym. For example, here is another
+valid way to write <literal>g</literal>'s type signature:
+<programlisting>
+  g :: Int -> Int -> forall b. b -> Int
+</programlisting>
+</para>
+<para>
+When doing this hoisting operation, GHC eliminates duplicate constraints.  For
+example:
+<programlisting>
+  type Foo a = (?x::Int) => Bool -> a
+  g :: Foo (Foo Int)
+</programlisting>
+means
+<programlisting>
+  g :: (?x::Int) => Bool -> Bool -> Int
+</programlisting>
+</para>
+</sect3>
+
+
+</sect2>
+
 <sect2 id="implicit-parameters">
 <title>Implicit parameters</title>
 
@@ -2378,30 +2429,6 @@ and you'd be right.  That is why they are an experimental feature.
 
 </sect2>
 
-<sect2 id="functional-dependencies">
-<title>Functional dependencies
-</title>
-
-<para> Functional dependencies are implemented as described by Mark Jones
-in &ldquo;<ulink url="http://www.cse.ogi.edu/~mpj/pubs/fundeps.html">Type Classes with Functional Dependencies</ulink>&rdquo;, Mark P. Jones, 
-In Proceedings of the 9th European Symposium on Programming, 
-ESOP 2000, Berlin, Germany, March 2000, Springer-Verlag LNCS 1782,
-.
-</para>
-<para>
-Functional dependencies are introduced by a vertical bar in the syntax of a 
-class declaration;  e.g. 
-<programlisting>
-  class (Monad m) => MonadState s m | m -> s where ...
-
-  class Foo a b c | a b -> c where ...
-</programlisting>
-There should be more documentation, but there isn't (yet).  Yell if you need it.
-</para>
-</sect2>
-
-
-
 <sect2 id="sec-kinding">
 <title>Explicitly-kinded quantification</title>