[project @ 2005-12-16 15:17:29 by simonpj]

[ghc-hetmet.git] / ghc / docs / users_guide / glasgow_exts.xml

diff --git a/ghc/docs/users_guide/glasgow_exts.xml b/ghc/docs/users_guide/glasgow_exts.xml
index 073003d..1e0e5b9 100644 (file)
--- a/ghc/docs/users_guide/glasgow_exts.xml
+++ b/ghc/docs/users_guide/glasgow_exts.xml
@@ -1092,8 +1092,12 @@ because GHC does not allow  unboxed tuples on the left of a function arrow.
 
 <para>
 The idea of using existential quantification in data type declarations
 
 <para>
 The idea of using existential quantification in data type declarations

-was suggested by Laufer (I believe, thought doubtless someone will
-correct me), and implemented in Hope+. It's been in Lennart
+was suggested by Perry, and implemented in Hope+ (Nigel Perry, <emphasis>The Implementation
+of Practical Functional Programming Languages</emphasis>, PhD Thesis, University of
+London, 1991). It was later formalised by Laufer and Odersky
+(<emphasis>Polymorphic type inference and abstract data types</emphasis>,
+TOPLAS, 16(5), pp1411-1430, 1994).
+It's been in Lennart

 Augustsson's <command>hbc</command> Haskell compiler for several years, and
 proved very useful.  Here's the idea.  Consider the declaration:
 </para>
 Augustsson's <command>hbc</command> Haskell compiler for several years, and
 proved very useful.  Here's the idea.  Consider the declaration:
 </para>

@@ -1205,7 +1209,7 @@ adding a new existential quantification construct.
 <title>Type classes</title>
 
 <para>
 <title>Type classes</title>
 
 <para>

-An easy extension (implemented in <command>hbc</command>) is to allow
+An easy extension is to allow

 arbitrary contexts before the constructor.  For example:
 </para>
 
 arbitrary contexts before the constructor.  For example:
 </para>
 

@@ -1264,6 +1268,86 @@ universal quantification earlier.
 </sect4>
 
 <sect4>
 </sect4>
 
 <sect4>

+<title>Record Constructors</title>
+
+<para>
+GHC allows existentials to be used with records syntax as well.  For example:
+
+<programlisting>
+data Counter a = forall self. NewCounter
+    { _this    :: self
+    , _inc     :: self -> self
+    , _display :: self -> IO ()
+    , tag      :: a
+    }
+</programlisting>
+Here <literal>tag</literal> is a public field, with a well-typed selector
+function <literal>tag :: Counter a -> a</literal>.  The <literal>self</literal>
+type is hidden from the outside; any attempt to apply <literal>_this</literal>,
+<literal>_inc</literal> or <literal>_output</literal> as functions will raise a
+compile-time error.  In other words, <emphasis>GHC defines a record selector function
+only for fields whose type does not mention the existentially-quantified variables</emphasis>.
+(This example used an underscore in the fields for which record selectors
+will not be defined, but that is only programming style; GHC ignores them.)
+</para>
+
+<para>
+To make use of these hidden fields, we need to create some helper functions:
+
+<programlisting>
+inc :: Counter a -> Counter a
+inc (NewCounter x i d t) = NewCounter
+    { _this = i x, _inc = i, _display = d, tag = t } 
+
+display :: Counter a -> IO ()
+display NewCounter{ _this = x, _display = d } = d x
+</programlisting>
+
+Now we can define counters with different underlying implementations:
+
+<programlisting>
+counterA :: Counter String 
+counterA = NewCounter
+    { _this = 0, _inc = (1+), _display = print, tag = "A" }
+
+counterB :: Counter String 
+counterB = NewCounter
+    { _this = "", _inc = ('#':), _display = putStrLn, tag = "B" }
+
+main = do
+    display (inc counterA)         -- prints "1"
+    display (inc (inc counterB))   -- prints "##"
+</programlisting>
+
+In GADT declarations (see <xref linkend="gadt"/>), the explicit
+<literal>forall</literal> may be omitted.  For example, we can express
+the same <literal>Counter a</literal> using GADT:
+
+<programlisting>
+data Counter a where
+    NewCounter { _this    :: self
+               , _inc     :: self -> self
+               , _display :: self -> IO ()
+               , tag      :: a
+               }
+        :: Counter a
+</programlisting>
+
+At the moment, record update syntax is only supported for Haskell 98 data types,
+so the following function does <emphasis>not</emphasis> work:
+
+<programlisting>
+-- This is invalid; use explicit NewCounter instead for now
+setTag :: Counter a -> a -> Counter a
+setTag obj t = obj{ tag = t }
+</programlisting>
+
+</para>
+
+</sect4>
+
+
+<sect4>

 <title>Restrictions</title>
 
 <para>
 <title>Restrictions</title>
 
 <para>

@@ -1425,19 +1509,20 @@ declarations.  Define your own instances!
 <title>Class declarations</title>
 
 <para>
 <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>
 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>
 <para>

- <emphasis>Multi-parameter type classes are permitted</emphasis>. For example:
+Multi-parameter type classes are permitted. For example:

 
 
 <programlisting>
 
 
 <programlisting>

@@ -1446,39 +1531,16 @@ There are the following constraints on class declarations:
     ...etc.
 </programlisting>
 
     ...etc.
 </programlisting>
 

-
-

 </para>
 </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>
 
 <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
 (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>
 
 
 <programlisting>

@@ -1491,62 +1553,33 @@ be acyclic</emphasis>.  So these class declarations are OK:
 
 
 </para>
 
 
 </para>

-</listitem>
-
-<listitem>
-

 <para>
 <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>
 
 
 <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>
 
 
 </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
+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>

 
 

-  class CollE s => Coll s a where
-    insert :: s -> a -> s
-</programlisting>

 
 
 
 

-</para>
-</listitem>
-
-</orderedlist>
-</para>

 
 <sect3 id="class-method-types">
 <title>Class method types</title>
 
 <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:
 <para>
 Haskell 98 prohibits class method types to mention constraints on the
 class type variable, thus:

@@ -1558,186 +1591,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>).
 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>

-<para>
-With the <option>-fglasgow-exts</option> GHC lifts this restriction.
-</para>
+

 
 </sect3>
 
 
 </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>
 <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>
 <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>
 </programlisting>

+There should be more documentation, but there isn't (yet).  Yell if you need it.

 </para>
 <para>
 </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>
 
 <programlisting>

-  forall tv1..tvn (c1, ...,cn) => type
+  class Coll s a where
+    empty  :: s
+    insert :: s -> a -> s

 </programlisting>
 
 </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>
 <programlisting>

-  forall a. Eq a => Int
+  class Coll s a | s -> a where
+    empty  :: s
+    insert :: s -> a -> s

 </programlisting>
 
 </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>
 <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>
 </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>
 
 
 <programlisting>

-  forall a. C a b => burble
-</programlisting>
+  class CollE s where
+    empty  :: s

 
 

+  class CollE s => Coll s a where
+    insert :: s -> a -> s
+</programlisting>
+</para>
+</sect3>

 
 

-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>
+</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>
 <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>
 </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>
 <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>
 
 </programlisting>
 </para>
 </sect3>
 

-
-</sect2>
-
-<sect2 id="instance-decls">
-<title>Instance declarations</title>
-

 <sect3 id="instance-overlap">
 <title>Overlapping instances</title>
 <para>
 <sect3 id="instance-overlap">
 <title>Overlapping instances</title>
 <para>

@@ -1888,7 +1855,7 @@ but this is not:
 <programlisting>
   instance F a where ...
 </programlisting>
 <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 ...
 For example, this is OK:
 <programlisting>
   instance Stateful (ST s) (MutVar s) where ...

@@ -1899,16 +1866,21 @@ For example, this is OK:
 
 <listitem>
 <para>All of the types in the <emphasis>context</emphasis> of
 
 <listitem>
 <para>All of the types in the <emphasis>context</emphasis> of

-an instance declaration <emphasis>must</emphasis> be type variables.
+an instance declaration <emphasis>must</emphasis> be type variables, and
+there must be no repeated type variables in any one constraint.

 Thus
 <programlisting>
 instance C a b => Eq (a,b) where ...
 </programlisting>
 is OK, but
 <programlisting>
 Thus
 <programlisting>
 instance C a b => Eq (a,b) where ...
 </programlisting>
 is OK, but
 <programlisting>

-instance C Int b => Foo b where ...
+instance C Int b => Foo [b] where ...
+</programlisting>
+is not OK (because of the non-type-variable <literal>Int</literal> in the context), and nor is
+<programlisting>
+instance C b b => Foo [b] where ...

 </programlisting>
 </programlisting>

-is not OK.
+(because of the repeated type variable).

 </para>
 </listitem>
 </orderedlist>
 </para>
 </listitem>
 </orderedlist>

@@ -1977,6 +1949,174 @@ allowing these idioms interesting idioms.
 
 </sect2>
 
 
 </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>
 
 <sect2 id="implicit-parameters">
 <title>Implicit parameters</title>
 

@@ -2374,30 +2514,6 @@ and you'd be right.  That is why they are an experimental feature.
 
 </sect2>
 
 
 </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>
 
 <sect2 id="sec-kinding">
 <title>Explicitly-kinded quantification</title>
 

@@ -3208,6 +3324,20 @@ GHC extends this list with two more classes that may be automatically derived
 modules <literal>Data.Typeable</literal> and <literal>Data.Generics</literal> respectively, and the
 appropriate class must be in scope before it can be mentioned in the <literal>deriving</literal> clause.
 </para>
 modules <literal>Data.Typeable</literal> and <literal>Data.Generics</literal> respectively, and the
 appropriate class must be in scope before it can be mentioned in the <literal>deriving</literal> clause.
 </para>

+<para>An instance of <literal>Typeable</literal> can only be derived if the
+data type has seven or fewer type parameters, all of kind <literal>*</literal>.
+The reason for this is that the <literal>Typeable</literal> class is derived using the scheme
+described in
+<ulink url="http://research.microsoft.com/%7Esimonpj/papers/hmap/gmap2.ps">
+Scrap More Boilerplate: Reflection, Zips, and Generalised Casts
+</ulink>.
+(Section 7.4 of the paper describes the multiple <literal>Typeable</literal> classes that
+are used, and only <literal>Typeable1</literal> up to
+<literal>Typeable7</literal> are provided in the library.)
+In other cases, there is nothing to stop the programmer writing a <literal>TypableX</literal>
+class, whose kind suits that of the data type constructor, and
+then writing the data type instance by hand.
+</para>

 </sect2>
 
 <sect2 id="newtype-deriving">
 </sect2>
 
 <sect2 id="newtype-deriving">

@@ -3413,6 +3543,68 @@ the standard method is used or the one described here.)
 
 </sect2>
 
 
 </sect2>
 

+<sect2 id="typing-binds">
+<title>Generalised typing of mutually recursive bindings</title>
+
+<para>
+The Haskell Report specifies that a group of bindings (at top level, or in a
+<literal>let</literal> or <literal>where</literal>) should be sorted into
+strongly-connected components, and then type-checked in dependency order
+(<ulink url="http://haskell.org/onlinereport/decls.html#sect4.5.1">Haskell
+Report, Section 4.5.1</ulink>).  
+As each group is type-checked, any binders of the group that
+have
+an explicit type signature are put in the type environment with the specified
+polymorphic type,
+and all others are monomorphic until the group is generalised 
+(<ulink url="http://haskell.org/onlinereport/decls.html#sect4.5.2">Haskell Report, Section 4.5.2</ulink>).
+</para>
+
+<para>Following a suggestion of Mark Jones, in his paper
+<ulink url="http://www.cse.ogi.edu/~mpj/thih/">Typing Haskell in
+Haskell</ulink>,
+GHC implements a more general scheme.  If <option>-fglasgow-exts</option> is
+specified:
+<emphasis>the dependency analysis ignores references to variables that have an explicit
+type signature</emphasis>.
+As a result of this refined dependency analysis, the dependency groups are smaller, and more bindings will
+typecheck.  For example, consider:
+<programlisting>
+  f :: Eq a =&gt; a -> Bool
+  f x = (x == x) || g True || g "Yes"
+  
+  g y = (y &lt;= y) || f True
+</programlisting>
+This is rejected by Haskell 98, but under Jones's scheme the definition for
+<literal>g</literal> is typechecked first, separately from that for
+<literal>f</literal>,
+because the reference to <literal>f</literal> in <literal>g</literal>'s right
+hand side is ingored by the dependency analysis.  Then <literal>g</literal>'s
+type is generalised, to get
+<programlisting>
+  g :: Ord a =&gt; a -> Bool
+</programlisting>
+Now, the defintion for <literal>f</literal> is typechecked, with this type for
+<literal>g</literal> in the type environment.
+</para>
+
+<para>
+The same refined dependency analysis also allows the type signatures of 
+mutually-recursive functions to have different contexts, something that is illegal in
+Haskell 98 (Section 4.5.2, last sentence).  With
+<option>-fglasgow-exts</option>
+GHC only insists that the type signatures of a <emphasis>refined</emphasis> group have identical
+type signatures; in practice this means that only variables bound by the same
+pattern binding must have the same context.  For example, this is fine:
+<programlisting>
+  f :: Eq a =&gt; a -> Bool
+  f x = (x == x) || g True
+  
+  g :: Ord a =&gt; a -> Bool
+  g y = (y &lt;= y) || f True
+</programlisting>
+</para>
+</sect2>

 
 </sect1>
 <!-- ==================== End of type system extensions =================  -->
 
 </sect1>
 <!-- ==================== End of type system extensions =================  -->

@@ -3439,9 +3631,9 @@ for these <literal>Terms</literal>:
   eval :: Term a -> a
   eval (Lit i)             = i
   eval (Succ t)     = 1 + eval t
   eval :: Term a -> a
   eval (Lit i)             = i
   eval (Succ t)     = 1 + eval t

-  eval (IsZero i)   = eval i == 0
+  eval (IsZero t)   = eval t == 0

   eval (If b e1 e2) = if eval b then eval e1 else eval e2
   eval (If b e1 e2) = if eval b then eval e1 else eval e2

-  eval (Pair e1 e2) = (eval e2, eval e2)
+  eval (Pair e1 e2) = (eval e1, eval e2)

 </programlisting>
 These and many other examples are given in papers by Hongwei Xi, and Tim Sheard.
 </para>
 </programlisting>
 These and many other examples are given in papers by Hongwei Xi, and Tim Sheard.
 </para>

@@ -3473,9 +3665,55 @@ type above, the type of each constructor must end with <literal> ... -> Term ...
 </para></listitem>
 
 <listitem><para>
 </para></listitem>
 
 <listitem><para>

-You cannot use a <literal>deriving</literal> clause on a GADT-style data type declaration,
-nor can you use record syntax.  (It's not clear what these constructs would mean.  For example,
-the record selectors might ill-typed.)  However, you can use strictness annotations, in the obvious places
+You can use record syntax on a GADT-style data type declaration:
+
+<programlisting>
+  data Term a where
+      Lit    { val  :: Int }      :: Term Int
+      Succ   { num  :: Term Int } :: Term Int
+      Pred   { num  :: Term Int } :: Term Int
+      IsZero { arg  :: Term Int } :: Term Bool 
+      Pair   { arg1 :: Term a
+             , arg2 :: Term b
+             }                    :: Term (a,b)
+      If     { cnd  :: Term Bool
+             , tru  :: Term a
+             , fls  :: Term a
+             }                    :: Term a
+</programlisting>
+For every constructor that has a field <literal>f</literal>, (a) the type of
+field <literal>f</literal> must be the same; and (b) the
+result type of the constructor must be the same; both modulo alpha conversion.
+Hence, in our example, we cannot merge the <literal>num</literal> and <literal>arg</literal>
+fields above into a 
+single name.  Although their field types are both <literal>Term Int</literal>,
+their selector functions actually have different types:
+
+<programlisting>
+  num :: Term Int -> Term Int
+  arg :: Term Bool -> Term Int
+</programlisting>
+
+At the moment, record updates are not yet possible with GADT, so support is 
+limited to record construction, selection and pattern matching:
+
+<programlisting>
+  someTerm :: Term Bool
+  someTerm = IsZero { arg = Succ { num = Lit { val = 0 } } }
+
+  eval :: Term a -> a
+  eval Lit    { val = i } = i
+  eval Succ   { num = t } = eval t + 1
+  eval Pred   { num = t } = eval t - 1
+  eval IsZero { arg = t } = eval t == 0
+  eval Pair   { arg1 = t1, arg2 = t2 } = (eval t1, eval t2)
+  eval t@If{} = if eval (cnd t) then eval (tru t) else eval (fls t)
+</programlisting>
+
+</para></listitem>
+
+<listitem><para>
+You can use strictness annotations, in the obvious places

 in the constructor type:
 <programlisting>
   data Term a where
 in the constructor type:
 <programlisting>
   data Term a where

@@ -3486,6 +3724,23 @@ in the constructor type:
 </para></listitem>
 
 <listitem><para>
 </para></listitem>
 
 <listitem><para>

+You can use a <literal>deriving</literal> clause on a GADT-style data type
+declaration, but only if the data type could also have been declared in
+Haskell-98 syntax.   For example, these two declarations are equivalent
+<programlisting>
+  data Maybe1 a where {
+      Nothing1 :: Maybe a ;
+      Just1    :: a -> Maybe a
+    } deriving( Eq, Ord )
+
+  data Maybe2 a = Nothing2 | Just2 a 
+       deriving( Eq, Ord )
+</programlisting>
+This simply allows you to declare a vanilla Haskell-98 data type using the
+<literal>where</literal> form without losing the <literal>deriving</literal> clause.
+</para></listitem>
+
+<listitem><para>

 Pattern matching causes type refinement.  For example, in the right hand side of the equation
 <programlisting>
   eval :: Term a -> a
 Pattern matching causes type refinement.  For example, in the right hand side of the equation
 <programlisting>
   eval :: Term a -> a

@@ -3569,9 +3824,11 @@ Tim Sheard is going to expand it.)
                  </para>
              <para> A splice can occur in place of 
                  <itemizedlist>
                  </para>
              <para> A splice can occur in place of 
                  <itemizedlist>

-                   <listitem><para> an expression; the spliced expression must have type <literal>Expr</literal></para></listitem>
+                   <listitem><para> an expression; the spliced expression must
+                   have type <literal>Q Exp</literal></para></listitem>

                    <listitem><para> a list of top-level declarations; ; the spliced expression must have type <literal>Q [Dec]</literal></para></listitem>
                    <listitem><para> a list of top-level declarations; ; the spliced expression must have type <literal>Q [Dec]</literal></para></listitem>

-                   <listitem><para> a type; the spliced expression must have type <literal>Type</literal>.</para></listitem>
+                   <listitem><para> [Planned, but not implemented yet.] a
+                   type; the spliced expression must have type <literal>Q Typ</literal>.</para></listitem>

                    </itemizedlist>
           (Note that the syntax for a declaration splice uses "<literal>$</literal>" not "<literal>splice</literal>" as in
        the paper. Also the type of the enclosed expression must be  <literal>Q [Dec]</literal>, not  <literal>[Q Dec]</literal>
                    </itemizedlist>
           (Note that the syntax for a declaration splice uses "<literal>$</literal>" not "<literal>splice</literal>" as in
        the paper. Also the type of the enclosed expression must be  <literal>Q [Dec]</literal>, not  <literal>[Q Dec]</literal>

@@ -3586,7 +3843,7 @@ Tim Sheard is going to expand it.)
                              the quotation has type <literal>Expr</literal>.</para></listitem>
                    <listitem><para> <literal>[d| ... |]</literal>, where the "..." is a list of top-level declarations;
                              the quotation has type <literal>Q [Dec]</literal>.</para></listitem>
                              the quotation has type <literal>Expr</literal>.</para></listitem>
                    <listitem><para> <literal>[d| ... |]</literal>, where the "..." is a list of top-level declarations;
                              the quotation has type <literal>Q [Dec]</literal>.</para></listitem>

-                   <listitem><para> <literal>[t| ... |]</literal>, where the "..." is a type; 
+                   <listitem><para>  [Planned, but not implemented yet.]  <literal>[t| ... |]</literal>, where the "..." is a type; 

                              the quotation has type <literal>Type</literal>.</para></listitem>
                  </itemizedlist></para></listitem>
 
                              the quotation has type <literal>Type</literal>.</para></listitem>
                  </itemizedlist></para></listitem>
 

@@ -3748,7 +4005,7 @@ What follows is a brief introduction to the notation;
 it won't make much sense unless you've read Hughes's paper.
 This notation is translated to ordinary Haskell,
 using combinators from the
 it won't make much sense unless you've read Hughes's paper.
 This notation is translated to ordinary Haskell,
 using combinators from the

-<ulink url="../libraries/base/Control.Arrow.html"><literal>Control.Arrow</literal></ulink>
+<ulink url="../libraries/base/Control-Arrow.html"><literal>Control.Arrow</literal></ulink>

 module.
 </para>
 
 module.
 </para>
 

@@ -3861,7 +4118,7 @@ the arrow <literal>f</literal>, and matches its output against
 <literal>y</literal>.
 In the next line, the output is discarded.
 The arrow <function>returnA</function> is defined in the
 <literal>y</literal>.
 In the next line, the output is discarded.
 The arrow <function>returnA</function> is defined in the

-<ulink url="../libraries/base/Control.Arrow.html"><literal>Control.Arrow</literal></ulink>
+<ulink url="../libraries/base/Control-Arrow.html"><literal>Control.Arrow</literal></ulink>

 module as <literal>arr id</literal>.
 The above example is treated as an abbreviation for
 <screen>
 module as <literal>arr id</literal>.
 The above example is treated as an abbreviation for
 <screen>

@@ -3878,7 +4135,7 @@ arr (\ x -> (x, x)) >>>
 Note that variables not used later in the composition are projected out.
 After simplification using rewrite rules (see <xref linkend="rewrite-rules"/>)
 defined in the
 Note that variables not used later in the composition are projected out.
 After simplification using rewrite rules (see <xref linkend="rewrite-rules"/>)
 defined in the

-<ulink url="../libraries/base/Control.Arrow.html"><literal>Control.Arrow</literal></ulink>
+<ulink url="../libraries/base/Control-Arrow.html"><literal>Control.Arrow</literal></ulink>

 module, this reduces to
 <screen>
 arr (\ x -> (x+1, x)) >>>
 module, this reduces to
 <screen>
 arr (\ x -> (x+1, x)) >>>

@@ -4173,7 +4430,7 @@ additional restrictions:
 <listitem>
 <para>
 The module must import
 <listitem>
 <para>
 The module must import

-<ulink url="../libraries/base/Control.Arrow.html"><literal>Control.Arrow</literal></ulink>.
+<ulink url="../libraries/base/Control-Arrow.html"><literal>Control.Arrow</literal></ulink>.

 </para>
 </listitem>
 
 </para>
 </listitem>
 

@@ -4269,12 +4526,13 @@ can still define and use your own versions of
 </para>
 
 <para>
 </para>
 
 <para>

-To have the compiler ignore uses of assert, use the compiler option
-<option>-fignore-asserts</option>. <indexterm><primary>-fignore-asserts
-option</primary></indexterm> That is, expressions of the form
+GHC ignores assertions when optimisation is turned on with the
+      <option>-O</option><indexterm><primary><option>-O</option></primary></indexterm> flag.  That is, expressions of the form

 <literal>assert pred e</literal> will be rewritten to
 <literal>assert pred e</literal> will be rewritten to

-<literal>e</literal>.
-</para>
+<literal>e</literal>.  You can also disable assertions using the
+      <option>-fignore-asserts</option>
+      option<indexterm><primary><option>-fignore-asserts</option></primary>
+      </indexterm>.</para>

 
 <para>
 Assertion failures can be caught, see the documentation for the
 
 <para>
 Assertion failures can be caught, see the documentation for the

@@ -4537,6 +4795,29 @@ key_function :: Int -> String -> (Bool, Double)
       </sect3>
     </sect2>
 
       </sect3>
     </sect2>
 

+    <sect2 id="language-pragma">
+      <title>LANGUAGE pragma</title>
+
+      <indexterm><primary>LANGUAGE</primary><secondary>pragma</secondary></indexterm>
+      <indexterm><primary>pragma</primary><secondary>LANGUAGE</secondary></indexterm>
+
+      <para>This allows language extensions to be enabled in a portable way.
+       It is the intention that all Haskell compilers support the
+       <literal>LANGUAGE</literal> pragma with the same syntax, although not
+       all extensions are supported by all compilers, of
+       course.  The <literal>LANGUAGE</literal> pragma should be used instead
+       of <literal>OPTIONS_GHC</literal>, if possible.</para>
+
+      <para>For example, to enable the FFI and preprocessing with CPP:</para>
+
+<programlisting>{-# LANGUAGE ForeignFunctionInterface, CPP #-}</programlisting>
+
+      <para>Any extension from the <literal>Extension</literal> type defined in
+       <ulink
+         url="../libraries/Cabal/Language-Haskell-Extension.html"><literal>Language.Haskell.Extension</literal></ulink> may be used.  GHC will report an error if any of the requested extensions are not supported.</para>
+    </sect2>
+
+

     <sect2 id="line-pragma">
       <title>LINE pragma</title>
 
     <sect2 id="line-pragma">
       <title>LINE pragma</title>
 

@@ -4547,9 +4828,7 @@ key_function :: Int -> String -> (Bool, Double)
       code.  It lets you specify the line number and filename of the
       original code; for example</para>
 
       code.  It lets you specify the line number and filename of the
       original code; for example</para>
 

-<programlisting>
-{-# LINE 42 "Foo.vhs" #-}
-</programlisting>
+<programlisting>{-# LINE 42 "Foo.vhs" #-}</programlisting>

 
       <para>if you'd generated the current file from something called
       <filename>Foo.vhs</filename> and this line corresponds to line
 
       <para>if you'd generated the current file from something called
       <filename>Foo.vhs</filename> and this line corresponds to line

@@ -4594,7 +4873,7 @@ key_function :: Int -> String -> (Bool, Double)
       overloaded function:</para>
 
 <programlisting>
       overloaded function:</para>
 
 <programlisting>

-hammeredLookup :: Ord key => [(key, value)] -> key -> value
+  hammeredLookup :: Ord key => [(key, value)] -> key -> value

 </programlisting>
 
       <para>If it is heavily used on lists with
 </programlisting>
 
       <para>If it is heavily used on lists with

@@ -4602,7 +4881,7 @@ hammeredLookup :: Ord key => [(key, value)] -> key -> value
       follows:</para>
 
 <programlisting>
       follows:</para>
 
 <programlisting>

-{-# SPECIALIZE hammeredLookup :: [(Widget, value)] -> Widget -> value #-}
+  {-# SPECIALIZE hammeredLookup :: [(Widget, value)] -> Widget -> value #-}

 </programlisting>
 
       <para>A <literal>SPECIALIZE</literal> pragma for a function can
 </programlisting>
 
       <para>A <literal>SPECIALIZE</literal> pragma for a function can

@@ -4613,7 +4892,35 @@ hammeredLookup :: Ord key => [(key, value)] -> key -> value
       (see <xref linkend="rewrite-rules"/>) that rewrites a call to the
       un-specialised function into a call to the specialised one.</para>
 
       (see <xref linkend="rewrite-rules"/>) that rewrites a call to the
       un-specialised function into a call to the specialised one.</para>
 

-      <para>In earlier versions of GHC, it was possible to provide your own
+      <para>The type in a SPECIALIZE pragma can be any type that is less
+       polymorphic than the type of the original function.  In concrete terms,
+       if the original function is <literal>f</literal> then the pragma
+<programlisting>
+  {-# SPECIALIZE f :: &lt;type&gt; #-}
+</programlisting>
+      is valid if and only if the defintion
+<programlisting>
+  f_spec :: &lt;type&gt;
+  f_spec = f
+</programlisting>
+      is valid.  Here are some examples (where we only give the type signature
+      for the original function, not its code):
+<programlisting>
+  f :: Eq a => a -> b -> b
+  {-# SPECIALISE g :: Int -> b -> b #-}
+
+  g :: (Eq a, Ix b) => a -> b -> b
+  {-# SPECIALISE g :: (Eq a) => a -> Int -> Int #-}
+
+  h :: Eq a => a -> a -> a
+  {-# SPECIALISE h :: (Eq a) => [a] -> [a] -> [a] #-}
+</programlisting>  
+The last of these examples will generate a 
+RULE with a somewhat-complex left-hand side (try it yourself), so it might not fire very
+well.  If you use this kind of specialisation, let us know how well it works.
+</para>
+
+      <para>Note: In earlier versions of GHC, it was possible to provide your own

       specialised function for a given type:
 
 <programlisting>
       specialised function for a given type:
 
 <programlisting>