[project @ 2002-10-01 15:59:03 by erkok]
[ghc-hetmet.git] / ghc / docs / users_guide / glasgow_exts.sgml
index d390f71..d4a39be 100644 (file)
@@ -16,143 +16,15 @@ performance because of the implementation costs of Haskell's
 </para>
 
 <para>
-Executive summary of our extensions:
-</para>
-
-  <variablelist>
-
-    <varlistentry>
-      <term>Unboxed types and primitive operations:</Term>
-      <listitem>
-       <para>You can get right down to the raw machine types and
-        operations; included in this are &ldquo;primitive
-        arrays&rdquo; (direct access to Big Wads of Bytes).  Please
-        see <XRef LinkEnd="glasgow-unboxed"> and following.</para>
-      </listitem>
-    </varlistentry>
-
-    <varlistentry>
-      <term>Type system extensions:</term>
-      <listitem>
-       <para> GHC supports a large number of extensions to Haskell's
-        type system.  Specifically:</para>
-
-       <variablelist>
-         <varlistentry>
-           <term>Multi-parameter type classes:</term>
-           <listitem>
-             <para><xref LinkEnd="multi-param-type-classes"></para>
-           </listitem>
-         </varlistentry>
-
-         <varlistentry>
-           <term>Functional dependencies:</term>
-           <listitem>
-             <para><xref LinkEnd="functional-dependencies"></para>
-           </listitem>
-         </varlistentry>
-
-         <varlistentry>
-           <term>Implicit parameters:</term>
-           <listitem>
-             <para><xref LinkEnd="implicit-parameters"></para>
-           </listitem>
-         </varlistentry>
-
-         <varlistentry>
-           <term>Local universal quantification:</term>
-           <listitem>
-             <para><xref LinkEnd="universal-quantification"></para>
-           </listitem>
-         </varlistentry>
-
-         <varlistentry>
-           <term>Extistentially quantification in data types:</term>
-           <listitem>
-             <para><xref LinkEnd="existential-quantification"></para>
-           </listitem>
-         </varlistentry>
-
-         <varlistentry>
-           <term>Scoped type variables:</term>
-           <listitem>
-             <para>Scoped type variables enable the programmer to
-              supply type signatures for some nested declarations,
-              where this would not be legal in Haskell 98.  Details in
-              <xref LinkEnd="scoped-type-variables">.</para>
-           </listitem>
-         </varlistentry>
-       </variablelist>
-      </listitem>
-    </varlistentry>
-
-    <varlistentry>
-      <term>Pattern guards</term>
-      <listitem>
-       <para>Instead of being a boolean expression, a guard is a list
-       of qualifiers, exactly as in a list comprehension. See <xref
-       LinkEnd="pattern-guards">.</para>
-      </listitem>
-    </varlistentry>
-
-    <varlistentry>
-      <term>Parallel list comprehensions</term>
-      <listitem>
-       <para>An extension to the list comprehension syntax to support
-       <literal>zipWith</literal>-like functionality.  See <xref
-       linkend="parallel-list-comprehensions">.</para>
-      </listitem>
-    </varlistentry>
-
-    <varlistentry>
-      <term>Foreign calling:</term>
-      <listitem>
-       <para>Just what it sounds like.  We provide
-        <emphasis>lots</emphasis> of rope that you can dangle around
-        your neck.  Please see <xref LinkEnd="ffi">.</para>
-      </listitem>
-    </varlistentry>
-
-    <varlistentry>
-      <term>Pragmas</term>
-      <listitem>
-       <para>Pragmas are special instructions to the compiler placed
-        in the source file.  The pragmas GHC supports are described in
-        <xref LinkEnd="pragmas">.</para>
-      </listitem>
-    </varlistentry>
-
-    <varlistentry>
-      <term>Rewrite rules:</term>
-      <listitem>
-       <para>The programmer can specify rewrite rules as part of the
-        source program (in a pragma).  GHC applies these rewrite rules
-        wherever it can.  Details in <xref
-        LinkEnd="rewrite-rules">.</para>
-      </listitem>
-    </varlistentry>
-
-    <varlistentry>
-      <term>Generic classes:</term>
-      <listitem>
-       <para>Generic class declarations allow you to define a class
-        whose methods say how to work over an arbitrary data type.
-        Then it's really easy to make any new type into an instance of
-        the class.  This generalises the rather ad-hoc "deriving"
-        feature of Haskell 98.  Details in <xref
-        LinkEnd="generic-classes">.</para>
-      </listitem>
-    </varlistentry>
-  </variablelist>
-
-<para>
 Before you get too carried away working at the lowest level (e.g.,
 sloshing <literal>MutableByteArray&num;</literal>s around your
 program), you may wish to check if there are libraries that provide a
-&ldquo;Haskellised veneer&rdquo; over the features you want.  See
-<xref linkend="book-hslibs">.
+&ldquo;Haskellised veneer&rdquo; over the features you want.  The
+separate libraries documentation describes all the libraries that come
+with GHC.
 </para>
 
+<!-- LANGUAGE OPTIONS -->
   <sect1 id="options-language">
     <title>Language options</title>
 
@@ -181,6 +53,30 @@ program), you may wish to check if there are libraries that provide a
       </varlistentry>
 
       <varlistentry>
+       <term><option>-ffi</option> and <option>-fffi</option>:</term>
+       <indexterm><primary><option>-ffi</option></primary></indexterm>
+       <indexterm><primary><option>-fffi</option></primary></indexterm>
+       <listitem>
+         <para>This option enables the language extension defined in the
+         Haskell 98 Foreign Function Interface Addendum plus deprecated
+         syntax of previous versions of the FFI for backwards
+         compatibility.</para> 
+       </listitem>
+      </varlistentry>
+
+      <varlistentry>
+       <term><option>-fwith</option>:</term>
+       <indexterm><primary><option>-fwith</option></primary></indexterm>
+       <listitem>
+         <para>This option enables the deprecated <literal>with</literal>
+         keyword for implicit parameters; it is merely provided for backwards
+         compatibility.
+          It is independent of the <option>-fglasgow-exts</option>
+          flag. </para>
+       </listitem>
+      </varlistentry>
+
+      <varlistentry>
        <term><option>-fno-monomorphism-restriction</option>:</term>
        <indexterm><primary><option>-fno-monomorphism-restriction</option></primary></indexterm>
        <listitem>
@@ -193,6 +89,7 @@ program), you may wish to check if there are libraries that provide a
       <varlistentry>
        <term><option>-fallow-overlapping-instances</option></term>
        <term><option>-fallow-undecidable-instances</option></term>
+       <term><option>-fallow-incoherent-instances</option></term>
        <term><option>-fcontext-stack</option></term>
        <indexterm><primary><option>-fallow-overlapping-instances</option></primary></indexterm>
        <indexterm><primary><option>-fallow-undecidable-instances</option></primary></indexterm>
@@ -234,7 +131,7 @@ program), you may wish to check if there are libraries that provide a
             module namespace is flat, and you must not conflict with
             any Prelude module.)</para>
 
-           <para>Even though you have not imported the Prelude, all
+           <para>Even though you have not imported the Prelude, most of
             the built-in syntax still refers to the built-in Haskell
             Prelude types and values, as specified by the Haskell
             Report.  For example, the type <literal>[Int]</literal>
@@ -243,51 +140,9 @@ program), you may wish to check if there are libraries that provide a
             translation for list comprehensions continues to use
             <literal>Prelude.map</literal> etc.</para>
 
-           <para> With one group of exceptions!  You may want to
-            define your own numeric class hierarchy.  It completely
-            defeats that purpose if the literal "1" means
-            "<literal>Prelude.fromInteger 1</literal>", which is what
-            the Haskell Report specifies.  So the
-            <option>-fno-implicit-prelude</option> flag causes the
-            following pieces of built-in syntax to refer to <emphasis>whatever
-            is in scope</emphasis>, not the Prelude versions:</para>
-
-           <itemizedlist>
-             <listitem>
-               <para>Integer and fractional literals mean
-                "<literal>fromInteger 1</literal>" and
-                "<literal>fromRational 3.2</literal>", not the
-                Prelude-qualified versions; both in expressions and in
-                patterns.</para>
-             </listitem>
-
-             <listitem>
-               <para>Negation (e.g. "<literal>- (f x)</literal>")
-               means "<literal>negate (f x)</literal>" (not
-               <literal>Prelude.negate</literal>).</para>
-             </listitem>
-
-             <listitem>
-               <para>In an n+k pattern, the standard Prelude
-                <literal>Ord</literal> class is still used for comparison,
-                but the necessary subtraction uses whatever
-                "<literal>(-)</literal>" is in scope (not
-                "<literal>Prelude.(-)</literal>").</para>
-             </listitem>
-           </itemizedlist>
-
-            <para>Note: Negative literals, such as <literal>-3</literal>, are
-             specified by (a careful reading of) the Haskell Report as 
-             meaning <literal>Prelude.negate (Prelude.fromInteger 3)</literal>.
-             However, GHC deviates from this slightly, and treats them as meaning
-             <literal>fromInteger (-3)</literal>.  One particular effect of this
-             slightly-non-standard reading is that there is no difficulty with
-             the literal <literal>-2147483648</literal> at type <literal>Int</literal>;
-             it means <literal>fromInteger (-2147483648)</literal>.  The strict interpretation
-             would be <literal>negate (fromInteger 2147483648)</literal>,
-             and the call to <literal>fromInteger</literal> would overflow
-             (at type <literal>Int</literal>, remember).
-             </para>
+           <para>However, <option>-fno-implicit-prelude</option> does
+           change the handling of certain built-in syntax: see
+           <xref LinkEnd="rebindable-syntax">.</para>
 
          </listitem>
        </varlistentry>
@@ -296,558 +151,324 @@ program), you may wish to check if there are libraries that provide a
   </sect1>
 
 <!-- UNBOXED TYPES AND PRIMITIVE OPERATIONS -->
+<!--    included from primitives.sgml  -->
 &primitives;
 
-<sect1 id="glasgow-ST-monad">
-<title>Primitive state-transformer monad</title>
 
-<para>
-<indexterm><primary>state transformers (Glasgow extensions)</primary></indexterm>
-<indexterm><primary>ST monad (Glasgow extension)</primary></indexterm>
-</para>
+<!-- TYPE SYSTEM EXTENSIONS -->
+<sect1 id="type-extensions">
+<title>Type system extensions</title>
 
-<para>
-This monad underlies our implementation of arrays, mutable and
-immutable, and our implementation of I/O, including &ldquo;C calls&rdquo;.
-</para>
+<sect2 id="nullary-types">
+<title>Data types with no constructors</title>
 
-<para>
-The <literal>ST</literal> library, which provides access to the
-<function>ST</function> monad, is described in <xref
-linkend="sec-ST">.
-</para>
+<para>With the <option>-fglasgow-exts</option> flag, GHC lets you declare
+a data type with no constructors.  For example:</para>
 
-</sect1>
+<programlisting>
+  data S      -- S :: *
+  data T a    -- T :: * -> *
+</programlisting>
 
-<sect1 id="glasgow-prim-arrays">
-<title>Primitive arrays, mutable and otherwise
-</title>
+<para>Syntactically, the declaration lacks the "= constrs" part.  The 
+type can be parameterised over types of any kind, but if the kind is
+not <literal>*</literal> then an explicit kind annotation must be used
+(see <xref linkend="sec-kinding">).</para>
+
+<para>Such data types have only one value, namely bottom.
+Nevertheless, they can be useful when defining "phantom types".</para>
+</sect2>
+
+<sect2 id="infix-tycons">
+<title>Infix type constructors</title>
 
 <para>
-<indexterm><primary>primitive arrays (Glasgow extension)</primary></indexterm>
-<indexterm><primary>arrays, primitive (Glasgow extension)</primary></indexterm>
+GHC allows type constructors to be operators, and to be written infix, very much 
+like expressions.  More specifically:
+<itemizedlist>
+<listitem><para>
+  A type constructor can be an operator, beginning with a colon; e.g. <literal>:*:</literal>.
+  The lexical syntax is the same as that for data constructors.
+  </para></listitem>
+<listitem><para>
+  Types can be written infix.  For example <literal>Int :*: Bool</literal>.  
+  </para></listitem>
+<listitem><para>
+  Back-quotes work
+  as for expressions, both for type constructors and type variables;  e.g. <literal>Int `Either` Bool</literal>, or
+  <literal>Int `a` Bool</literal>.  Similarly, parentheses work the same; e.g.  <literal>(:*:) Int Bool</literal>.
+  </para></listitem>
+<listitem><para>
+  Fixities may be declared for type constructors just as for data constructors.  However,
+  one cannot distinguish between the two in a fixity declaration; a fixity declaration
+  sets the fixity for a data constructor and the corresponding type constructor.  For example:
+<screen>
+  infixl 7 T, :*:
+</screen>
+  sets the fixity for both type constructor <literal>T</literal> and data constructor <literal>T</literal>,
+  and similarly for <literal>:*:</literal>.
+  <literal>Int `a` Bool</literal>.
+  </para></listitem>
+<listitem><para>
+  Function arrow is <literal>infixr</literal> with fixity 0.  (This might change; I'm not sure what it should be.)
+  </para></listitem>
+<listitem><para>
+  Data type and type-synonym declarations can be written infix.  E.g.
+<screen>
+  data a :*: b = Foo a b
+  type a :+: b = Either a b
+</screen>
+  </para></listitem>
+<listitem><para>
+  The only thing that differs between operators in types and operators in expressions is that
+  ordinary non-constructor operators, such as <literal>+</literal> and <literal>*</literal>
+  are not allowed in types. Reason: the uniform thing to do would be to make them type
+  variables, but that's not very useful.  A less uniform but more useful thing would be to
+  allow them to be type <emphasis>constructors</emphasis>.  But that gives trouble in export
+  lists.  So for now we just exclude them.
+  </para></listitem>
+
+</itemizedlist>
 </para>
+</sect2>
+
+<sect2 id="sec-kinding">
+<title>Explicitly-kinded quantification</title>
 
 <para>
-GHC knows about quite a few flavours of Large Swathes of Bytes.
+Haskell infers the kind of each type variable.  Sometimes it is nice to be able
+to give the kind explicitly as (machine-checked) documentation, 
+just as it is nice to give a type signature for a function.  On some occasions,
+it is essential to do so.  For example, in his paper "Restricted Data Types in Haskell" (Haskell Workshop 1999)
+John Hughes had to define the data type:
+<Screen>
+     data Set cxt a = Set [a]
+                    | Unused (cxt a -> ())
+</Screen>
+The only use for the <literal>Unused</literal> constructor was to force the correct
+kind for the type variable <literal>cxt</literal>.
 </para>
-
 <para>
-First, GHC distinguishes between primitive arrays of (boxed) Haskell
-objects (type <literal>Array&num; obj</literal>) and primitive arrays of bytes (type
-<literal>ByteArray&num;</literal>).
+GHC now instead allows you to specify the kind of a type variable directly, wherever
+a type variable is explicitly bound.  Namely:
+<itemizedlist>
+<listitem><para><literal>data</literal> declarations:
+<Screen>
+  data Set (cxt :: * -> *) a = Set [a]
+</Screen></para></listitem>
+<listitem><para><literal>type</literal> declarations:
+<Screen>
+  type T (f :: * -> *) = f Int
+</Screen></para></listitem>
+<listitem><para><literal>class</literal> declarations:
+<Screen>
+  class (Eq a) => C (f :: * -> *) a where ...
+</Screen></para></listitem>
+<listitem><para><literal>forall</literal>'s in type signatures:
+<Screen>
+  f :: forall (cxt :: * -> *). Set cxt Int
+</Screen></para></listitem>
+</itemizedlist>
 </para>
 
 <para>
-Second, it distinguishes between&hellip;
-<variablelist>
+The parentheses are required.  Some of the spaces are required too, to
+separate the lexemes.  If you write <literal>(f::*->*)</literal> you
+will get a parse error, because "<literal>::*->*</literal>" is a
+single lexeme in Haskell.
+</para>
 
-<varlistentry>
-<term>Immutable:</term>
-<listitem>
 <para>
-Arrays that do not change (as with &ldquo;standard&rdquo; Haskell arrays); you
-can only read from them.  Obviously, they do not need the care and
-attention of the state-transformer monad.
+As part of the same extension, you can put kind annotations in types
+as well.  Thus:
+<Screen>
+   f :: (Int :: *) -> Int
+   g :: forall a. a -> (a :: *)
+</Screen>
+The syntax is
+<Screen>
+   atype ::= '(' ctype '::' kind ')
+</Screen>
+The parentheses are required.
 </para>
-</listitem>
-</varlistentry>
-<varlistentry>
-<term>Mutable:</term>
-<listitem>
+</sect2>
+
+
+<sect2 id="class-method-types">
+<title>Class method types
+</title>
 <para>
-Arrays that may be changed or &ldquo;mutated.&rdquo;  All the operations on them
-live within the state-transformer monad and the updates happen
-<emphasis>in-place</emphasis>.
+Haskell 98 prohibits class method types to mention constraints on the
+class type variable, thus:
+<programlisting>
+  class Seq s a where
+    fromList :: [a] -> s a
+    elem     :: Eq a => a -> s a -> Bool
+</programlisting>
+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>).
 </para>
-</listitem>
-</varlistentry>
-<varlistentry>
-<term>&ldquo;Static&rdquo; (in C land):</term>
-<listitem>
 <para>
-A C routine may pass an <literal>Addr&num;</literal> pointer back into Haskell land.  There
-are then primitive operations with which you may merrily grab values
-over in C land, by indexing off the &ldquo;static&rdquo; pointer.
+With the <option>-fglasgow-exts</option> GHC lifts this restriction.
 </para>
-</listitem>
-</varlistentry>
-<varlistentry>
-<term>&ldquo;Stable&rdquo; pointers:</term>
-<listitem>
+
+</sect2>
+
+<sect2 id="multi-param-type-classes">
+<title>Multi-parameter type classes
+</title>
+
 <para>
-If, for some reason, you wish to hand a Haskell pointer (i.e.,
-<emphasis>not</emphasis> an unboxed value) to a C routine, you first make the
-pointer &ldquo;stable,&rdquo; so that the garbage collector won't forget that it
-exists.  That is, GHC provides a safe way to pass Haskell pointers to
-C.
+This section documents GHC's implementation of multi-parameter type
+classes.  There's lots of background in the paper <ULink
+URL="http://research.microsoft.com/~simonpj/multi.ps.gz" >Type
+classes: exploring the design space</ULink > (Simon Peyton Jones, Mark
+Jones, Erik Meijer).
 </para>
 
 <para>
-Please see <xref LinkEnd="sec-stable-pointers"> for more details.
+I'd like to thank people who reported shorcomings in the GHC 3.02
+implementation.  Our default decisions were all conservative ones, and
+the experience of these heroic pioneers has given useful concrete
+examples to support several generalisations.  (These appear below as
+design choices not implemented in 3.02.)
 </para>
-</listitem>
-</varlistentry>
-<varlistentry>
-<term>&ldquo;Foreign objects&rdquo;:</term>
-<listitem>
+
 <para>
-A &ldquo;foreign object&rdquo; is a safe way to pass an external object (a
-C-allocated pointer, say) to Haskell and have Haskell do the Right
-Thing when it no longer references the object.  So, for example, C
-could pass a large bitmap over to Haskell and say &ldquo;please free this
-memory when you're done with it.&rdquo;
+I've discussed these notes with Mark Jones, and I believe that Hugs
+will migrate towards the same design choices as I outline here.
+Thanks to him, and to many others who have offered very useful
+feedback.
 </para>
 
+<sect3>
+<title>Types</title>
+
 <para>
-Please see <xref LinkEnd="sec-ForeignObj"> for more details.
-</para>
-</listitem>
-</varlistentry>
-</variablelist>
+There are the following restrictions on the form of a qualified
+type:
 </para>
 
 <para>
-The libraries documentatation gives more details on all these
-&ldquo;primitive array&rdquo; types and the operations on them.
+
+<programlisting>
+  forall tv1..tvn (c1, ...,cn) => type
+</programlisting>
+
 </para>
 
-</sect1>
+<para>
+(Here, I write the "foralls" explicitly, although the Haskell source
+language omits them; in Haskell 1.4, 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>
 
-<sect1 id="pattern-guards">
-<title>Pattern guards</title>
+<OrderedList>
+<listitem>
 
 <para>
-<indexterm><primary>Pattern guards (Glasgow extension)</primary></indexterm>
-The discussion that follows is an abbreviated version of Simon Peyton Jones's original <ULink URL="http://research.microsoft.com/~simonpj/Haskell/guards.html">proposal</ULink>. (Note that the proposal was written before pattern guards were implemented, so refers to them as unimplemented.)
+ <emphasis>Each universally quantified type variable
+<literal>tvi</literal> must be mentioned (i.e. appear free) in <literal>type</literal></emphasis>.
+
+The reason for this is that a value with a type that does not obey
+this restriction could not be used without introducing
+ambiguity. 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>
+</listitem>
+<listitem>
 
 <para>
-Suppose we have an abstract data type of finite maps, with a
-lookup operation:
+ <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>
-lookup :: FiniteMap -> Int -> Maybe Int
+  forall a. C a b => burble
 </programlisting>
 
-The lookup returns <function>Nothing</function> if the supplied key is not in the domain of the mapping, and <function>(Just v)</function> otherwise,
-where <VarName>v</VarName> is the value that the key maps to.  Now consider the following definition:
-</para>
+
+The next type is illegal because the constraint <literal>Eq b</literal> does not
+mention <literal>a</literal>:
+
 
 <programlisting>
-clunky env var1 var2 | ok1 && ok2 = val1 + val2
-| otherwise  = var1 + var2
-where
-  m1 = lookup env var1
-  m2 = lookup env var2
-  ok1 = maybeToBool m1
-  ok2 = maybeToBool m2
-  val1 = expectJust m1
-  val2 = expectJust m2
+  forall a. Eq b => burble
 </programlisting>
 
-<para>
-The auxiliary functions are 
+
+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>
 
-<programlisting>
-maybeToBool :: Maybe a -&gt; Bool
-maybeToBool (Just x) = True
-maybeToBool Nothing  = False
+</OrderedList>
 
-expectJust :: Maybe a -&gt; a
-expectJust (Just x) = x
-expectJust Nothing  = error "Unexpected Nothing"
-</programlisting>
+</para>
 
 <para>
-What is <function>clunky</function> doing? The guard <literal>ok1 &&
-ok2</literal> checks that both lookups succeed, using
-<function>maybeToBool</function> to convert the <function>Maybe</function>
-types to booleans. The (lazily evaluated) <function>expectJust</function>
-calls extract the values from the results of the lookups, and binds the
-returned values to <VarName>val1</VarName> and <VarName>val2</VarName>
-respectively.  If either lookup fails, then clunky takes the
-<literal>otherwise</literal> case and returns the sum of its arguments.
+These restrictions apply to all types, whether declared in a type signature
+or inferred.
 </para>
 
 <para>
-This is certainly legal Haskell, but it is a tremendously verbose and
-un-obvious way to achieve the desired effect.  Arguably, a more direct way
-to write clunky would be to use case expressions:
+Unlike Haskell 1.4, constraints in types do <emphasis>not</emphasis> have to be of
+the form <emphasis>(class type-variables)</emphasis>.  Thus, these type signatures
+are perfectly OK
 </para>
 
+<para>
+
 <programlisting>
-clunky env var1 var1 = case lookup env var1 of
-  Nothing -&gt; fail
-  Just val1 -&gt; case lookup env var2 of
-    Nothing -&gt; fail
-    Just val2 -&gt; val1 + val2
-where
-  fail = val1 + val2
+  f :: Eq (m a) => [m a] -> [m a]
+  g :: Eq [a] => ...
 </programlisting>
 
-<para>
-This is a bit shorter, but hardly better.  Of course, we can rewrite any set
-of pattern-matching, guarded equations as case expressions; that is
-precisely what the compiler does when compiling equations! The reason that
-Haskell provides guarded equations is because they allow us to write down
-the cases we want to consider, one at a time, independently of each other. 
-This structure is hidden in the case version.  Two of the right-hand sides
-are really the same (<function>fail</function>), and the whole expression
-tends to become more and more indented. 
 </para>
 
 <para>
-Here is how I would write clunky:
+This choice recovers principal types, a property that Haskell 1.4 does not have.
 </para>
 
-<programlisting>
-clunky env var1 var1
-  | Just val1 &lt;- lookup env var1
-  , Just val2 &lt;- lookup env var2
-  = val1 + val2
-...other equations for clunky...
-</programlisting>
+</sect3>
+
+<sect3>
+<title>Class declarations</title>
 
 <para>
-The semantics should be clear enough.  The qualifers are matched in order. 
-For a <literal>&lt;-</literal> qualifier, which I call a pattern guard, the
-right hand side is evaluated and matched against the pattern on the left. 
-If the match fails then the whole guard fails and the next equation is
-tried.  If it succeeds, then the appropriate binding takes place, and the
-next qualifier is matched, in the augmented environment.  Unlike list
-comprehensions, however, the type of the expression to the right of the
-<literal>&lt;-</literal> is the same as the type of the pattern to its
-left.  The bindings introduced by pattern guards scope over all the
-remaining guard qualifiers, and over the right hand side of the equation.
-</para>
+
+<OrderedList>
+<listitem>
 
 <para>
-Just as with list comprehensions, boolean expressions can be freely mixed
-with among the pattern guards.  For example:
-</para>
-
-<programlisting>
-f x | [y] <- x
-    , y > 3
-    , Just z <- h y
-    = ...
-</programlisting>
-
-<para>
-Haskell's current guards therefore emerge as a special case, in which the
-qualifier list has just one element, a boolean expression.
-</para>
-</sect1>
-
-  <sect1 id="parallel-list-comprehensions">
-    <title>Parallel List Comprehensions</title>
-    <indexterm><primary>list comprehensions</primary><secondary>parallel</secondary>
-    </indexterm>
-    <indexterm><primary>parallel list comprehensions</primary>
-    </indexterm>
-
-    <para>Parallel list comprehensions are a natural extension to list
-    comprehensions.  List comprehensions can be thought of as a nice
-    syntax for writing maps and filters.  Parallel comprehensions
-    extend this to include the zipWith family.</para>
-
-    <para>A parallel list comprehension has multiple independent
-    branches of qualifier lists, each separated by a `|' symbol.  For
-    example, the following zips together two lists:</para>
-
-<programlisting>
-   [ (x, y) | x <- xs | y <- ys ] 
-</programlisting>
-
-    <para>The behavior of parallel list comprehensions follows that of
-    zip, in that the resulting list will have the same length as the
-    shortest branch.</para>
-
-    <para>We can define parallel list comprehensions by translation to
-    regular comprehensions.  Here's the basic idea:</para>
-
-    <para>Given a parallel comprehension of the form: </para>
-
-<programlisting>
-   [ e | p1 <- e11, p2 <- e12, ... 
-       | q1 <- e21, q2 <- e22, ... 
-       ... 
-   ] 
-</programlisting>
-
-    <para>This will be translated to: </para>
-
-<programlisting>
-   [ e | ((p1,p2), (q1,q2), ...) <- zipN [(p1,p2) | p1 <- e11, p2 <- e12, ...] 
-                                         [(q1,q2) | q1 <- e21, q2 <- e22, ...] 
-                                         ... 
-   ] 
-</programlisting>
-
-    <para>where `zipN' is the appropriate zip for the given number of
-    branches.</para>
-
-  </sect1>
-
-  <sect1 id="sec-ffi">
-    <title>The foreign interface</title>
-
-    <para>The foreign interface consists of the following components:</para>
-
-    <itemizedlist>
-      <listitem>
-       <para>The Foreign Function Interface language specification
-       (included in this manual, in <xref linkend="ffi">).</para>
-      </listitem>
-
-      <listitem>
-       <para>The <literal>Foreign</literal> module (see <xref
-       linkend="sec-Foreign">) collects together several interfaces
-       which are useful in specifying foreign language
-       interfaces, including the following:</para>
-
-       <itemizedlist>
-         <listitem>
-           <para>The <literal>ForeignObj</literal> module (see <xref
-           linkend="sec-ForeignObj">), for managing pointers from
-           Haskell into the outside world.</para>
-         </listitem>
-      
-         <listitem>
-           <para>The <literal>StablePtr</literal> module (see <xref
-           linkend="sec-stable-pointers">), for managing pointers
-           into Haskell from the outside world.</para>
-         </listitem>
-      
-         <listitem>
-           <para>The <literal>CTypes</literal> module (see <xref
-           linkend="sec-CTypes">) gives Haskell equivalents for the
-           standard C datatypes, for use in making Haskell bindings
-           to existing C libraries.</para>
-         </listitem>
-      
-         <listitem>
-           <para>The <literal>CTypesISO</literal> module (see <xref
-           linkend="sec-CTypesISO">) gives Haskell equivalents for C
-           types defined by the ISO C standard.</para>
-         </listitem>
-      
-         <listitem>
-           <para>The <literal>Storable</literal> library, for
-           primitive marshalling of data types between Haskell and
-           the foreign language.</para>
-         </listitem>
-       </itemizedlist>
-
-      </listitem>
-    </itemizedlist>
-
-<para>The following sections also give some hints and tips on the use
-of the foreign function interface in GHC.</para>
-
-<sect2 id="glasgow-foreign-headers">
-<title>Using function headers
-</title>
-
-<para>
-<indexterm><primary>C calls, function headers</primary></indexterm>
-</para>
-
-<para>
-When generating C (using the <option>-fvia-C</option> directive), one can assist the
-C compiler in detecting type errors by using the <Command>-&num;include</Command> directive
-to provide <filename>.h</filename> files containing function headers.
-</para>
-
-<para>
-For example,
-</para>
-
-<para>
-
-<programlisting>
-#include "HsFFI.h"
-
-void         initialiseEFS (HsInt size);
-HsInt        terminateEFS (void);
-HsForeignObj emptyEFS(void);
-HsForeignObj updateEFS (HsForeignObj a, HsInt i, HsInt x);
-HsInt        lookupEFS (HsForeignObj a, HsInt i);
-</programlisting>
-</para>
-
-      <para>The types <literal>HsInt</literal>,
-      <literal>HsForeignObj</literal> etc. are described in <xref
-      linkend="sec-mapping-table">.</para>
-
-      <para>Note that this approach is only
-      <emphasis>essential</emphasis> for returning
-      <literal>float</literal>s (or if <literal>sizeof(int) !=
-      sizeof(int *)</literal> on your architecture) but is a Good
-      Thing for anyone who cares about writing solid code.  You're
-      crazy not to do it.</para>
-
-</sect2>
-
-</sect1>
-
-<sect1 id="multi-param-type-classes">
-<title>Multi-parameter type classes
-</title>
-
-<para>
-This section documents GHC's implementation of multi-parameter type
-classes.  There's lots of background in the paper <ULink
-URL="http://research.microsoft.com/~simonpj/multi.ps.gz" >Type
-classes: exploring the design space</ULink > (Simon Peyton Jones, Mark
-Jones, Erik Meijer).
-</para>
-
-<para>
-I'd like to thank people who reported shorcomings in the GHC 3.02
-implementation.  Our default decisions were all conservative ones, and
-the experience of these heroic pioneers has given useful concrete
-examples to support several generalisations.  (These appear below as
-design choices not implemented in 3.02.)
-</para>
-
-<para>
-I've discussed these notes with Mark Jones, and I believe that Hugs
-will migrate towards the same design choices as I outline here.
-Thanks to him, and to many others who have offered very useful
-feedback.
-</para>
-
-<sect2>
-<title>Types</title>
-
-<para>
-There are the following restrictions on the form of a qualified
-type:
-</para>
-
-<para>
-
-<programlisting>
-  forall tv1..tvn (c1, ...,cn) => type
-</programlisting>
-
-</para>
-
-<para>
-(Here, I write the "foralls" explicitly, although the Haskell source
-language omits them; in Haskell 1.4, 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 mentioned (i.e. appear free) in <literal>type</literal></emphasis>.
-
-The reason for this is that a value with a type that does not obey
-this restriction could not be used without introducing
-ambiguity. 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>
-</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>
-
-<para>
-These restrictions apply to all types, whether declared in a type signature
-or inferred.
-</para>
-
-<para>
-Unlike Haskell 1.4, constraints in types do <emphasis>not</emphasis> have to be of
-the form <emphasis>(class type-variables)</emphasis>.  Thus, these type signatures
-are perfectly OK
-</para>
-
-<para>
-
-<programlisting>
-  f :: Eq (m a) => [m a] -> [m a]
-  g :: Eq [a] => ...
-</programlisting>
-
-</para>
-
-<para>
-This choice recovers principal types, a property that Haskell 1.4 does not have.
-</para>
-
-</sect2>
-
-<sect2>
-<title>Class declarations</title>
-
-<para>
-
-<OrderedList>
-<listitem>
-
-<para>
- <emphasis>Multi-parameter type classes are permitted</emphasis>. For example:
-
+ <emphasis>Multi-parameter type classes are permitted</emphasis>. For example:
+
 
 <programlisting>
   class Collection c a where
@@ -997,9 +618,9 @@ class like this:
 
 </para>
 
-</sect2>
+</sect3>
 
-<sect2 id="instance-decls">
+<sect3 id="instance-decls">
 <title>Instance declarations</title>
 
 <para>
@@ -1022,9 +643,9 @@ declarations
 
 However, if you give the command line option
 <option>-fallow-overlapping-instances</option><indexterm><primary>-fallow-overlapping-instances
-option</primary></indexterm> then two overlapping instance declarations are permitted
-iff
-
+option</primary></indexterm> then overlapping instance declarations are permitted.
+However, GHC arranges never to commit to using an instance declaration
+if another instance declaration also applies, either now or later.
 
 <itemizedlist>
 <listitem>
@@ -1037,22 +658,11 @@ iff
 
 <para>
  OR <literal>type2</literal> is a substitution instance of <literal>type1</literal>
-(but not identical to <literal>type1</literal>)
-</para>
-</listitem>
-<listitem>
-
-<para>
- OR vice versa
+(but not identical to <literal>type1</literal>), or vice versa.
 </para>
 </listitem>
-
 </itemizedlist>
-
-
 Notice that these rules
-
-
 <itemizedlist>
 <listitem>
 
@@ -1072,8 +682,34 @@ Reason: you can pick which instance decl
 </listitem>
 
 </itemizedlist>
-
-
+However the rules are over-conservative.  Two instance declarations can overlap,
+but it can still be clear in particular situations which to use.  For example:
+<programlisting>
+  instance C (Int,a) where ...
+  instance C (a,Bool) where ...
+</programlisting>
+These are rejected by GHC's rules, but it is clear what to do when trying
+to solve the constraint <literal>C (Int,Int)</literal> because the second instance
+cannot apply.  Yell if this restriction bites you.
+</para>
+<para>
+GHC is also conservative about committing to an overlapping instance.  For example:
+<programlisting>
+  class C a where { op :: a -> a }
+  instance C [Int] where ...
+  instance C a => C [a] where ...
+  
+  f :: C b => [b] -> [b]
+  f x = op x
+</programlisting>
+From the RHS of f we get the constraint <literal>C [b]</literal>.  But
+GHC does not commit to the second instance declaration, because in a paricular
+call of f, b might be instantiate to Int, so the first instance declaration
+would be appropriate.  So GHC rejects the program.  If you add <option>-fallow-incoherent-instances</option>
+GHC will instead silently pick the second instance, without complaining about 
+the problem of subsequent instantiations.
+</para>
+<para>
 Regrettably, GHC doesn't guarantee to detect overlapping instance
 declarations if they appear in different modules.  GHC can "see" the
 instance declarations in the transitive closure of all the modules
@@ -1247,11 +883,11 @@ with <option>-fcontext-stack</option><emphasis>N</emphasis>.
 
 </para>
 
-</sect2>
+</sect3>
 
-</sect1>
+</sect2>
 
-<sect1 id="implicit-parameters">
+<sect2 id="implicit-parameters">
 <title>Implicit parameters
 </title>
 
@@ -1261,11 +897,107 @@ J Lewis, MB Shields, E Meijer, J Launchbury,
 27th ACM Symposium on Principles of Programming Languages (POPL'00),
 Boston, Jan 2000.
 </para>
+<para>(Most of the following, stil rather incomplete, documentation is due to Jeff Lewis.)</para>
+<para>
+A variable is called <emphasis>dynamically bound</emphasis> when it is bound by the calling
+context of a function and <emphasis>statically bound</emphasis> when bound by the callee's
+context. In Haskell, all variables are statically bound. Dynamic
+binding of variables is a notion that goes back to Lisp, but was later
+discarded in more modern incarnations, such as Scheme. Dynamic binding
+can be very confusing in an untyped language, and unfortunately, typed
+languages, in particular Hindley-Milner typed languages like Haskell,
+only support static scoping of variables.
+</para>
+<para>
+However, by a simple extension to the type class system of Haskell, we
+can support dynamic binding. Basically, we express the use of a
+dynamically bound variable as a constraint on the type. These
+constraints lead to types of the form <literal>(?x::t') => t</literal>, which says "this
+function uses a dynamically-bound variable <literal>?x</literal> 
+of type <literal>t'</literal>". For
+example, the following expresses the type of a sort function,
+implicitly parameterized by a comparison function named <literal>cmp</literal>.
+<programlisting>
+  sort :: (?cmp :: a -> a -> Bool) => [a] -> [a]
+</programlisting>
+The dynamic binding constraints are just a new form of predicate in the type class system.
+</para>
+<para>
+An implicit parameter is introduced by the special form <literal>?x</literal>, 
+where <literal>x</literal> is
+any valid identifier. Use if this construct also introduces new
+dynamic binding constraints. For example, the following definition
+shows how we can define an implicitly parameterized sort function in
+terms of an explicitly parameterized <literal>sortBy</literal> function:
+<programlisting>
+  sortBy :: (a -> a -> Bool) -> [a] -> [a]
 
+  sort   :: (?cmp :: a -> a -> Bool) => [a] -> [a]
+  sort    = sortBy ?cmp
+</programlisting>
+Dynamic binding constraints behave just like other type class
+constraints in that they are automatically propagated. Thus, when a
+function is used, its implicit parameters are inherited by the
+function that called it. For example, our <literal>sort</literal> function might be used
+to pick out the least value in a list:
+<programlisting>
+  least   :: (?cmp :: a -> a -> Bool) => [a] -> a
+  least xs = fst (sort xs)
+</programlisting>
+Without lifting a finger, the <literal>?cmp</literal> parameter is
+propagated to become a parameter of <literal>least</literal> as well. With explicit
+parameters, the default is that parameters must always be explicit
+propagated. With implicit parameters, the default is to always
+propagate them.
+</para>
 <para>
-There should be more documentation, but there isn't (yet).  Yell if you need it.
+An implicit parameter differs from other type class constraints in the
+following way: All uses of a particular implicit parameter must have
+the same type. This means that the type of <literal>(?x, ?x)</literal> 
+is <literal>(?x::a) => (a,a)</literal>, and not 
+<literal>(?x::a, ?x::b) => (a, b)</literal>, as would be the case for type
+class constraints.
 </para>
+<para>
+An implicit parameter is bound using the standard
+<literal>let</literal> binding form, where the bindings must be a
+collection of simple bindings to implicit-style variables (no
+function-style bindings, and no type signatures); these bindings are
+neither polymorphic or recursive. This form binds the implicit
+parameters arising in the body, not the free variables as a
+<literal>let</literal> or <literal>where</literal> would do. For
+example, we define the <literal>min</literal> function by binding
+<literal>cmp</literal>.</para>
+<programlisting>
+  min :: [a] -> a
+  min  = let ?cmp = (<=) in least
+</programlisting>
+<para>
+Note the following points:
 <itemizedlist>
+<listitem><para>
+You may not mix implicit-parameter bindings with ordinary bindings in a 
+single <literal>let</literal>
+expression; use two nested <literal>let</literal>s instead.
+</para></listitem>
+
+<listitem><para>
+You may put multiple implicit-parameter bindings in a
+single <literal>let</literal> expression; they are <emphasis>not</emphasis> treated
+as a mutually recursive group (as ordinary <literal>let</literal> bindings are).
+Instead they are treated as a non-recursive group, each scoping over the bindings that
+follow.  For example, consider:
+<programlisting>
+  f y = let { ?x = y; ?x = ?x+1 } in ?x
+</programlisting>
+This function adds one to its argument.
+</para></listitem>
+
+<listitem><para>
+You may not have an implicit-parameter binding in a <literal>where</literal> clause,
+only in a <literal>let</literal> binding.
+</para></listitem>
+
 <listitem>
 <para> You can't have an implicit parameter in the context of a class or instance
 declaration.  For example, both these declarations are illegal:
@@ -1278,83 +1010,276 @@ you invoke a function. But the ``invocation'' of instance declarations is done
 behind the scenes by the compiler, so it's hard to figure out exactly where it is done.
 Easiest thing is to outlaw the offending types.</para>
 </listitem>
-
 </itemizedlist>
+</para>
 
-</sect1>
-
+</sect2>
 
-<sect1 id="functional-dependencies">
-<title>Functional dependencies
+<sect2 id="linear-implicit-parameters">
+<title>Linear implicit parameters
 </title>
-
-<para> Functional dependencies are implemented as described by Mark Jones
-in "Type Classes with Functional Dependencies", Mark P. Jones, 
-In Proceedings of the 9th European Symposium on Programming, 
-ESOP 2000, Berlin, Germany, March 2000, Springer-Verlag LNCS 1782.
+<para>
+Linear implicit parameters are an idea developed by Koen Claessen,
+Mark Shields, and Simon PJ.  They address the long-standing
+problem that monads seem over-kill for certain sorts of problem, notably:
 </para>
+<itemizedlist>
+<listitem> <para> distributing a supply of unique names </para> </listitem>
+<listitem> <para> distributing a suppply of random numbers </para> </listitem>
+<listitem> <para> distributing an oracle (as in QuickCheck) </para> </listitem>
+</itemizedlist>
 
 <para>
-There should be more documentation, but there isn't (yet).  Yell if you need it.
+Linear implicit parameters are just like ordinary implicit parameters,
+except that they are "linear" -- that is, they cannot be copied, and
+must be explicitly "split" instead.  Linear implicit parameters are
+written '<literal>%x</literal>' instead of '<literal>?x</literal>'.  
+(The '/' in the '%' suggests the split!)
 </para>
-</sect1>
+<para>
+For example:
+<programlisting>
+    import GHC.Exts( Splittable )
 
+    data NameSupply = ...
+    
+    splitNS :: NameSupply -> (NameSupply, NameSupply)
+    newName :: NameSupply -> Name
+
+    instance Splittable NameSupply where
+       split = splitNS
 
-<sect1 id="universal-quantification">
-<title>Explicit universal quantification
-</title>
 
+    f :: (%ns :: NameSupply) => Env -> Expr -> Expr
+    f env (Lam x e) = Lam x' (f env e)
+                   where
+                     x'   = newName %ns
+                     env' = extend env x x'
+    ...more equations for f...
+</programlisting>
+Notice that the implicit parameter %ns is consumed 
+<itemizedlist>
+<listitem> <para> once by the call to <literal>newName</literal> </para> </listitem>
+<listitem> <para> once by the recursive call to <literal>f</literal> </para></listitem>
+</itemizedlist>
+</para>
+<para>
+So the translation done by the type checker makes
+the parameter explicit:
+<programlisting>
+    f :: NameSupply -> Env -> Expr -> Expr
+    f ns env (Lam x e) = Lam x' (f ns1 env e)
+                      where
+                        (ns1,ns2) = splitNS ns
+                        x' = newName ns2
+                        env = extend env x x'
+</programlisting>
+Notice the call to 'split' introduced by the type checker.
+How did it know to use 'splitNS'?  Because what it really did
+was to introduce a call to the overloaded function 'split',
+defined by the class <literal>Splittable</literal>:
+<programlisting>
+       class Splittable a where
+         split :: a -> (a,a)
+</programlisting>
+The instance for <literal>Splittable NameSupply</literal> tells GHC how to implement
+split for name supplies.  But we can simply write
+<programlisting>
+       g x = (x, %ns, %ns)
+</programlisting>
+and GHC will infer
+<programlisting>
+       g :: (Splittable a, %ns :: a) => b -> (b,a,a)
+</programlisting>
+The <literal>Splittable</literal> class is built into GHC.  It's exported by module 
+<literal>GHC.Exts</literal>.
+</para>
 <para>
-GHC's type system supports explicit universal quantification in
-constructor fields and function arguments.  This is useful for things
-like defining <literal>runST</literal> from the state-thread world. 
-GHC's syntax for this now agrees with Hugs's, namely:
+Other points:
+<itemizedlist>
+<listitem> <para> '<literal>?x</literal>' and '<literal>%x</literal>' 
+are entirely distinct implicit parameters: you 
+  can use them together and they won't intefere with each other. </para>
+</listitem>
+
+<listitem> <para> You can bind linear implicit parameters in 'with' clauses. </para> </listitem>
+
+<listitem> <para>You cannot have implicit parameters (whether linear or not)
+  in the context of a class or instance declaration. </para></listitem>
+</itemizedlist>
 </para>
 
+<sect3><title>Warnings</title>
+
+<para>
+The monomorphism restriction is even more important than usual.
+Consider the example above:
+<programlisting>
+    f :: (%ns :: NameSupply) => Env -> Expr -> Expr
+    f env (Lam x e) = Lam x' (f env e)
+                   where
+                     x'   = newName %ns
+                     env' = extend env x x'
+</programlisting>
+If we replaced the two occurrences of x' by (newName %ns), which is
+usually a harmless thing to do, we get:
+<programlisting>
+    f :: (%ns :: NameSupply) => Env -> Expr -> Expr
+    f env (Lam x e) = Lam (newName %ns) (f env e)
+                   where
+                     env' = extend env x (newName %ns)
+</programlisting>
+But now the name supply is consumed in <emphasis>three</emphasis> places
+(the two calls to newName,and the recursive call to f), so
+the result is utterly different.  Urk!  We don't even have 
+the beta rule.
+</para>
 <para>
+Well, this is an experimental change.  With implicit
+parameters we have already lost beta reduction anyway, and
+(as John Launchbury puts it) we can't sensibly reason about
+Haskell programs without knowing their typing.
+</para>
+
+</sect3>
 
+<sect3><title>Recursive functions</title>
+<para>Linear implicit parameters can be particularly tricky when you have a recursive function
+Consider
+<programlisting>
+        foo :: %x::T => Int -> [Int]
+        foo 0 = []
+        foo n = %x : foo (n-1)
+</programlisting>
+where T is some type in class Splittable.</para>
+<para>
+Do you get a list of all the same T's or all different T's
+(assuming that split gives two distinct T's back)?
+</para><para>
+If you supply the type signature, taking advantage of polymorphic
+recursion, you get what you'd probably expect.  Here's the
+translated term, where the implicit param is made explicit:
 <programlisting>
-        forall a b. (Ord a, Eq  b) => a -> b -> a
+        foo x 0 = []
+        foo x n = let (x1,x2) = split x
+                  in x1 : foo x2 (n-1)
 </programlisting>
+But if you don't supply a type signature, GHC uses the Hindley
+Milner trick of using a single monomorphic instance of the function
+for the recursive calls. That is what makes Hindley Milner type inference
+work.  So the translation becomes
+<programlisting>
+        foo x = let
+                  foom 0 = []
+                  foom n = x : foom (n-1)
+                in
+                foom
+</programlisting>
+Result: 'x' is not split, and you get a list of identical T's.  So the
+semantics of the program depends on whether or not foo has a type signature.
+Yikes!
+</para><para>
+You may say that this is a good reason to dislike linear implicit parameters
+and you'd be right.  That is why they are an experimental feature. 
+</para>
+</sect3>
+
+</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>
-The context is, of course, optional.  You can't use <literal>forall</literal> as
-a type variable any more!
+There should be more documentation, but there isn't (yet).  Yell if you need it.
 </para>
+</sect2>
+
+
+<sect2 id="universal-quantification">
+<title>Arbitrary-rank polymorphism
+</title>
 
 <para>
-Haskell type signatures are implicitly quantified.  The <literal>forall</literal>
+Haskell type signatures are implicitly quantified.  The new keyword <literal>forall</literal>
 allows us to say exactly what this means.  For example:
 </para>
-
 <para>
-
 <programlisting>
         g :: b -> b
 </programlisting>
-
-</para>
-
-<para>
 means this:
+<programlisting>
+        g :: forall b. (b -> b)
+</programlisting>
+The two are treated identically.
 </para>
 
 <para>
+However, GHC's type system supports <emphasis>arbitrary-rank</emphasis> 
+explicit universal quantification in
+types. 
+For example, all the following types are legal:
+<programlisting>
+    f1 :: forall a b. a -> b -> a
+    g1 :: forall a b. (Ord a, Eq  b) => a -> b -> a
 
+    f2 :: (forall a. a->a) -> Int -> Int
+    g2 :: (forall a. Eq a => [a] -> a -> Bool) -> Int -> Int
+
+    f3 :: ((forall a. a->a) -> Int) -> Bool -> Bool
+</programlisting>
+Here, <literal>f1</literal> and <literal>g1</literal> are rank-1 types, and
+can be written in standard Haskell (e.g. <literal>f1 :: a->b->a</literal>).
+The <literal>forall</literal> makes explicit the universal quantification that
+is implicitly added by Haskell.
+</para>
+<para>
+The functions <literal>f2</literal> and <literal>g2</literal> have rank-2 types;
+the <literal>forall</literal> is on the left of a function arrrow.  As <literal>g2</literal>
+shows, the polymorphic type on the left of the function arrow can be overloaded.
+</para>
+<para>
+The functions <literal>f3</literal> and <literal>g3</literal> have rank-3 types;
+they have rank-2 types on the left of a function arrow.
+</para>
+<para>
+GHC allows types of arbitrary rank; you can nest <literal>forall</literal>s
+arbitrarily deep in function arrows.   (GHC used to be restricted to rank 2, but
+that restriction has now been lifted.)
+In particular, a forall-type (also called a "type scheme"),
+including an operational type class context, is legal:
+<itemizedlist>
+<listitem> <para> On the left of a function arrow </para> </listitem>
+<listitem> <para> On the right of a function arrow (see <xref linkend="hoist">) </para> </listitem>
+<listitem> <para> As the argument of a constructor, or type of a field, in a data type declaration. For
+example, any of the <literal>f1,f2,f3,g1,g2,g3</literal> above would be valid
+field type signatures.</para> </listitem>
+<listitem> <para> As the type of an implicit parameter </para> </listitem>
+<listitem> <para> In a pattern type signature (see <xref linkend="scoped-type-variables">) </para> </listitem>
+</itemizedlist>
+There is one place you cannot put a <literal>forall</literal>:
+you cannot instantiate a type variable with a forall-type.  So you cannot 
+make a forall-type the argument of a type constructor.  So these types are illegal:
 <programlisting>
-        g :: forall b. (b -> b)
+    x1 :: [forall a. a->a]
+    x2 :: (forall a. a->a, Int)
+    x3 :: Maybe (forall a. a->a)
 </programlisting>
-
+Of course <literal>forall</literal> becomes a keyword; you can't use <literal>forall</literal> as
+a type variable any more!
 </para>
 
-<para>
-The two are treated identically.
-</para>
 
-<sect2 id="univ">
-<title>Universally-quantified data type fields
+<sect3 id="univ">
+<title>Examples
 </title>
 
 <para>
@@ -1377,8 +1302,7 @@ newtype Swizzle = MkSwizzle (Ord a => [a] -> [a])
 </para>
 
 <para>
-The constructors now have so-called <emphasis>rank 2</emphasis> polymorphic
-types, in which there is a for-all in the argument types.:
+The constructors have rank-2 types:
 </para>
 
 <para>
@@ -1422,11 +1346,6 @@ to <emphasis>require</emphasis> explicit quantification on constructor arguments
 where that is what is wanted.  Feedback welcomed.)
 </para>
 
-</sect2>
-
-<sect2>
-<title>Construction </title>
-
 <para>
 You construct values of types <literal>T1, MonadT, Swizzle</literal> by applying
 the constructor to suitable values, just as usual.  For example,
@@ -1435,17 +1354,23 @@ the constructor to suitable values, just as usual.  For example,
 <para>
 
 <programlisting>
-(T1 (\xy->x) 3) :: T Int
-
-(MkSwizzle sort)    :: Swizzle
-(MkSwizzle reverse) :: Swizzle
+    a1 :: T Int
+    a1 = T1 (\xy->x) 3
+    
+    a2, a3 :: Swizzle
+    a2 = MkSwizzle sort
+    a3 = MkSwizzle reverse
+    
+    a4 :: MonadT Maybe
+    a4 = let r x = Just x
+            b m k = case m of
+                      Just y -> k y
+                      Nothing -> Nothing
+         in
+         MkMonad r b
 
-(let r x = Just x
-     b m k = case m of
-                Just y -> k y
-                Nothing -> Nothing
-  in
-  MkMonad r b) :: MonadT Maybe
+    mkTs :: (forall b. b -> b -> b) -> a -> [T a]
+    mkTs f x y = [T1 f x, T1 f y]
 </programlisting>
 
 </para>
@@ -1456,11 +1381,6 @@ required, as <literal>(MkSwizzle reverse)</literal> shows.  (<function>reverse</
 does not need the <literal>Ord</literal> constraint.)
 </para>
 
-</sect2>
-
-<sect2>
-<title>Pattern matching</title>
-
 <para>
 When you use pattern matching, the bound variables may now have
 polymorphic types.  For example:
@@ -1469,17 +1389,17 @@ polymorphic types.  For example:
 <para>
 
 <programlisting>
-        f :: T a -> a -> (a, Char)
-        f (T1 f k) x = (f k x, f 'c' 'd')
+    f :: T a -> a -> (a, Char)
+    f (T1 w k) x = (w k x, w 'c' 'd')
 
-        g :: (Ord a, Ord b) => Swizzle -> [a] -> (a -> b) -> [b]
-        g (MkSwizzle s) xs f = s (map f (s xs))
+    g :: (Ord a, Ord b) => Swizzle -> [a] -> (a -> b) -> [b]
+    g (MkSwizzle s) xs f = s (map f (s xs))
 
-        h :: MonadT m -> [m a] -> m [a]
-        h m [] = return m []
-        h m (x:xs) = bind m x           $ \y ->
-                      bind m (h m xs)   $ \ys ->
-                      return m (y:ys)
+    h :: MonadT m -> [m a] -> m [a]
+    h m [] = return m []
+    h m (x:xs) = bind m x          $ \y ->
+                 bind m (h m xs)   $ \ys ->
+                 return m (y:ys)
 </programlisting>
 
 </para>
@@ -1490,205 +1410,200 @@ and <literal>bind</literal> to extract the polymorphic bind and return functions
 from the <literal>MonadT</literal> data structure, rather than using pattern
 matching.
 </para>
+</sect3>
 
-<para>
-You cannot pattern-match against an argument that is polymorphic.
-For example:
-
-<programlisting>
-        newtype TIM s a = TIM (ST s (Maybe a))
-
-        runTIM :: (forall s. TIM s a) -> Maybe a
-        runTIM (TIM m) = runST m
-</programlisting>
-
-</para>
+<sect3>
+<title>Type inference</title>
 
 <para>
-Here the pattern-match fails, because you can't pattern-match against
-an argument of type <literal>(forall s. TIM s a)</literal>.  Instead you
-must bind the variable and pattern match in the right hand side:
-
-<programlisting>
-        runTIM :: (forall s. TIM s a) -> Maybe a
-        runTIM tm = case tm of { TIM m -> runST m }
-</programlisting>
-
-The <literal>tm</literal> on the right hand side is (invisibly) instantiated, like
-any polymorphic value at its occurrence site, and now you can pattern-match
-against it.
+In general, type inference for arbitrary-rank types is undecideable.
+GHC uses an algorithm proposed by Odersky and Laufer ("Putting type annotations to work", POPL'96)
+to get a decidable algorithm by requiring some help from the programmer.
+We do not yet have a formal specification of "some help" but the rule is this:
 </para>
-
-</sect2>
-
-<sect2>
-<title>The partial-application restriction</title>
-
 <para>
-There is really only one way in which data structures with polymorphic
-components might surprise you: you must not partially apply them.
-For example, this is illegal:
+<emphasis>For a lambda-bound or case-bound variable, x, either the programmer
+provides an explicit polymorphic type for x, or GHC's type inference will assume
+that x's type has no foralls in it</emphasis>.
 </para>
-
 <para>
-
+What does it mean to "provide" an explicit type for x?  You can do that by 
+giving a type signature for x directly, using a pattern type signature
+(<xref linkend="scoped-type-variables">), thus:
 <programlisting>
-        map MkSwizzle [sort, reverse]
+     \ f :: (forall a. a->a) -> (f True, f 'c')
 </programlisting>
-
-</para>
-
-<para>
-The restriction is this: <emphasis>every subexpression of the program must
-have a type that has no for-alls, except that in a function
-application (f e1&hellip;en) the partial applications are not subject to
-this rule</emphasis>.  The restriction makes type inference feasible.
-</para>
-
-<para>
-In the illegal example, the sub-expression <literal>MkSwizzle</literal> has the
-polymorphic type <literal>(Ord b => [b] -> [b]) -> Swizzle</literal> and is not
-a sub-expression of an enclosing application.  On the other hand, this
-expression is OK:
-</para>
-
-<para>
-
+Alternatively, you can give a type signature to the enclosing
+context, which GHC can "push down" to find the type for the variable:
 <programlisting>
-        map (T1 (\a b -> a)) [1,2,3]
+     (\ f -> (f True, f 'c')) :: (forall a. a->a) -> (Bool,Char)
 </programlisting>
-
-</para>
-
-<para>
-even though it involves a partial application of <function>T1</function>, because
-the sub-expression <literal>T1 (\a b -> a)</literal> has type <literal>Int -> T
-Int</literal>.
+Here the type signature on the expression can be pushed inwards
+to give a type signature for f.  Similarly, and more commonly,
+one can give a type signature for the function itself:
+<programlisting>
+     h :: (forall a. a->a) -> (Bool,Char)
+     h f = (f True, f 'c')
+</programlisting>
+You don't need to give a type signature if the lambda bound variable
+is a constructor argument.  Here is an example we saw earlier:
+<programlisting>
+    f :: T a -> a -> (a, Char)
+    f (T1 w k) x = (w k x, w 'c' 'd')
+</programlisting>
+Here we do not need to give a type signature to <literal>w</literal>, because
+it is an argument of constructor <literal>T1</literal> and that tells GHC all
+it needs to know.
 </para>
 
-</sect2>
+</sect3>
 
-<sect2 id="sigs">
-<title>Type signatures
-</title>
 
-<para>
-Once you have data constructors with universally-quantified fields, or
-constants such as <Constant>runST</Constant> that have rank-2 types, it isn't long
-before you discover that you need more!  Consider:
-</para>
+<sect3 id="implicit-quant">
+<title>Implicit quantification</title>
 
 <para>
-
+GHC performs implicit quantification as follows.  <emphasis>At the top level (only) of 
+user-written types, if and only if there is no explicit <literal>forall</literal>,
+GHC finds all the type variables mentioned in the type that are not already
+in scope, and universally quantifies them.</emphasis>  For example, the following pairs are 
+equivalent:
 <programlisting>
-  mkTs f x y = [T1 f x, T1 f y]
-</programlisting>
-
-</para>
-
-<para>
-<function>mkTs</function> is a fuction that constructs some values of type
-<literal>T</literal>, using some pieces passed to it.  The trouble is that since
-<literal>f</literal> is a function argument, Haskell assumes that it is
-monomorphic, so we'll get a type error when applying <function>T1</function> to
-it.  This is a rather silly example, but the problem really bites in
-practice.  Lots of people trip over the fact that you can't make
-"wrappers functions" for <Constant>runST</Constant> for exactly the same reason.
-In short, it is impossible to build abstractions around functions with
-rank-2 types.
-</para>
+  f :: a -> a
+  f :: forall a. a -> a
 
-<para>
-The solution is fairly clear.  We provide the ability to give a rank-2
-type signature for <emphasis>ordinary</emphasis> functions (not only data
-constructors), thus:
+  g (x::a) = let
+                h :: a -> b -> b
+                h x y = y
+             in ...
+  g (x::a) = let
+                h :: forall b. a -> b -> b
+                h x y = y
+             in ...
+</programlisting>
 </para>
-
 <para>
-
+Notice that GHC does <emphasis>not</emphasis> find the innermost possible quantification
+point.  For example:
 <programlisting>
-  mkTs :: (forall b. b -> b -> b) -> a -> [T a]
-  mkTs f x y = [T1 f x, T1 f y]
-</programlisting>
+  f :: (a -> a) -> Int
+           -- MEANS
+  f :: forall a. (a -> a) -> Int
+           -- NOT
+  f :: (forall a. a -> a) -> Int
 
-</para>
 
-<para>
-This type signature tells the compiler to attribute <literal>f</literal> with
-the polymorphic type <literal>(forall b. b -> b -> b)</literal> when type
-checking the body of <function>mkTs</function>, so now the application of
-<function>T1</function> is fine.
+  g :: (Ord a => a -> a) -> Int
+           -- MEANS the illegal type
+  g :: forall a. (Ord a => a -> a) -> Int
+           -- NOT
+  g :: (forall a. Ord a => a -> a) -> Int
+</programlisting>
+The latter produces an illegal type, which you might think is silly,
+but at least the rule is simple.  If you want the latter type, you
+can write your for-alls explicitly.  Indeed, doing so is strongly advised
+for rank-2 types.
 </para>
+</sect3>
+</sect2>
 
-<para>
-There are two restrictions:
-</para>
+<sect2 id="type-synonyms">
+<title>Liberalised type synonyms 
+</title>
 
 <para>
-
+Type synonmys are like macros at the type level, and
+GHC does validity checking on types <emphasis>only after expanding type synonyms</emphasis>.
+That means that GHC can be very much more liberal about type synonyms than Haskell 98:
 <itemizedlist>
-<listitem>
-
-<para>
- You can only define a rank 2 type, specified by the following
-grammar:
-
-
+<listitem> <para>You can write a <literal>forall</literal> (including overloading)
+in a type synonym, thus:
 <programlisting>
-rank2type ::= [forall tyvars .] [context =>] funty
-funty     ::= ([forall tyvars .] [context =>] ty) -> funty
-            | ty
-ty        ::= ...current Haskell monotype syntax...
-</programlisting>
+  type Discard a = forall b. Show b => a -> b -> (a, String)
 
+  f :: Discard a
+  f x y = (x, show y)
 
-Informally, the universal quantification must all be right at the beginning,
-or at the top level of a function argument.
-
+  g :: Discard Int -> (Int,Bool)    -- A rank-2 type
+  g f = f Int True
+</programlisting>
 </para>
 </listitem>
-<listitem>
 
-<para>
- There is a restriction on the definition of a function whose
-type signature is a rank-2 type: the polymorphic arguments must be
-matched on the left hand side of the "<literal>=</literal>" sign.  You can't
-define <function>mkTs</function> like this:
+<listitem><para>
+You can write an unboxed tuple in a type synonym:
+<programlisting>
+  type Pr = (# Int, Int #)
 
+  h :: Int -> Pr
+  h x = (# x, x #)
+</programlisting>
+</para></listitem>
 
+<listitem><para>
+You can apply a type synonym to a forall type:
 <programlisting>
-mkTs :: (forall b. b -> b -> b) -> a -> [T a]
-mkTs = \ f x y -> [T1 f x, T1 f y]
+  type Foo a = a -> a -> Bool
+  f :: Foo (forall b. b->b)
 </programlisting>
+After expanding the synonym, <literal>f</literal> has the legal (in GHC) type:
+<programlisting>
+  f :: (forall b. b->b) -> (forall b. b->b) -> Bool
+</programlisting>
+</para></listitem>
 
+<listitem><para>
+You can apply a type synonym to a partially applied type synonym:
+<programlisting>
+  type Generic i o = forall x. i x -> o x
+  type Id x = x
+  
+  foo :: Generic Id []
+</programlisting>
+After epxanding the synonym, <literal>foo</literal> has the legal (in GHC) type:
+<programlisting>
+  foo :: forall x. x -> [x]
+</programlisting>
+</para></listitem>
 
-
-The same partial-application rule applies to ordinary functions with
-rank-2 types as applied to data constructors.
-
+</itemizedlist>
 </para>
-</listitem>
 
+<para>
+GHC currently does kind checking before expanding synonyms (though even that
+could be changed.)
+</para>
+<para>
+After expanding type synonyms, GHC does validity checking on types, looking for
+the following mal-formedness which isn't detected simply by kind checking:
+<itemizedlist>
+<listitem><para>
+Type constructor applied to a type involving for-alls.
+</para></listitem>
+<listitem><para>
+Unboxed tuple on left of an arrow.
+</para></listitem>
+<listitem><para>
+Partially-applied type synonym.
+</para></listitem>
 </itemizedlist>
+So, for example,
+this will be rejected:
+<programlisting>
+  type Pr = (# Int, Int #)
 
+  h :: Pr -> Int
+  h x = ...
+</programlisting>
+because GHC does not allow  unboxed tuples on the left of a function arrow.
 </para>
-
 </sect2>
 
-
 <sect2 id="hoist">
-<title>Type synonyms and hoisting
-</title>
-
+<title>For-all hoisting</title>
 <para>
-GHC also allows you to write a <literal>forall</literal> in a type synonym, thus:
-<programlisting>
-  type Discard a = forall b. a -> b -> a
-
-  f :: Discard a
-  f x y = x
-</programlisting>
-However, it is often convenient to use these sort of synonyms at the right hand
+It is often convenient to use generalised type synonyms at the right hand
 end of an arrow, thus:
 <programlisting>
   type Discard a = forall b. a -> b -> a
@@ -1708,9 +1623,9 @@ In general, the rule is this: <emphasis>to determine the type specified by any e
 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 a. <emphasis>type2</emphasis>
+  <emphasis>type1</emphasis> -> forall a1..an. <emphasis>context2</emphasis> => <emphasis>type2</emphasis>
 ==>
-  forall a. <emphasis>type1</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
@@ -1720,11 +1635,22 @@ valid way to write <literal>g</literal>'s type signature:
   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>
 </sect2>
 
-</sect1>
 
-<sect1 id="existential-quantification">
+<sect2 id="existential-quantification">
 <title>Existentially quantified data constructors
 </title>
 
@@ -1814,7 +1740,7 @@ that collection of packages in a uniform manner.  You can express
 quite a bit of object-oriented-like programming this way.
 </para>
 
-<sect2 id="existential">
+<sect3 id="existential">
 <title>Why existential?
 </title>
 
@@ -1837,9 +1763,9 @@ But Haskell programmers can safely think of the ordinary
 adding a new existential quantification construct.
 </para>
 
-</sect2>
+</sect3>
 
-<sect2>
+<sect3>
 <title>Type classes</title>
 
 <para>
@@ -1882,7 +1808,7 @@ So this program is legal:
   f :: Baz -> String
   f (Baz1 p q) | p == q    = "Yes"
                | otherwise = "No"
-  f (Baz1 v fn)            = show (fn v)
+  f (Baz2 v fn)            = show (fn v)
 </programlisting>
 
 </para>
@@ -1899,9 +1825,9 @@ Notice the way that the syntax fits smoothly with that used for
 universal quantification earlier.
 </para>
 
-</sect2>
+</sect3>
 
-<sect2>
+<sect3>
 <title>Restrictions</title>
 
 <para>
@@ -2045,92 +1971,12 @@ declarations.  Define your own instances!
 
 </para>
 
-</sect2>
-
-</sect1>
-
-<sect1 id="sec-assertions">
-<title>Assertions
-<indexterm><primary>Assertions</primary></indexterm>
-</title>
-
-<para>
-If you want to make use of assertions in your standard Haskell code, you
-could define a function like the following:
-</para>
-
-<para>
-
-<programlisting>
-assert :: Bool -> a -> a
-assert False x = error "assertion failed!"
-assert _     x = x
-</programlisting>
-
-</para>
-
-<para>
-which works, but gives you back a less than useful error message --
-an assertion failed, but which and where?
-</para>
-
-<para>
-One way out is to define an extended <function>assert</function> function which also
-takes a descriptive string to include in the error message and
-perhaps combine this with the use of a pre-processor which inserts
-the source location where <function>assert</function> was used.
-</para>
-
-<para>
-Ghc offers a helping hand here, doing all of this for you. For every
-use of <function>assert</function> in the user's source:
-</para>
-
-<para>
-
-<programlisting>
-kelvinToC :: Double -> Double
-kelvinToC k = assert (k &gt;= 0.0) (k+273.15)
-</programlisting>
-
-</para>
-
-<para>
-Ghc will rewrite this to also include the source location where the
-assertion was made,
-</para>
-
-<para>
-
-<programlisting>
-assert pred val ==> assertError "Main.hs|15" pred val
-</programlisting>
-
-</para>
-
-<para>
-The rewrite is only performed by the compiler when it spots
-applications of <function>Exception.assert</function>, so you can still define and
-use your own versions of <function>assert</function>, should you so wish. If not,
-import <literal>Exception</literal> to make use <function>assert</function> in your code.
-</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 <literal>assert pred e</literal> will be rewritten to <literal>e</literal>.
-</para>
-
-<para>
-Assertion failures can be caught, see the documentation for the
-<literal>Exception</literal> library (<xref linkend="sec-Exception">)
-for the details.
-</para>
+</sect3>
 
-</sect1>
+</sect2>
 
-<sect1 id="scoped-type-variables">
-<title>Scoped Type Variables
+<sect2 id="scoped-type-variables">
+<title>Scoped type variables
 </title>
 
 <para>
@@ -2157,6 +2003,8 @@ In particular, it is in scope at the type signature for <VarName>y</VarName>.
 </para>
 
 <para>
+ Pattern type signatures are completely orthogonal to ordinary, separate
+type signatures.  The two can be used independently or together.
 At ordinary type signatures, such as that for <VarName>ys</VarName>, any type variables
 mentioned in the type signature <emphasis>that are not in scope</emphasis> are
 implicitly universally quantified.  (If there are no type variables in
@@ -2178,7 +2026,47 @@ are noted.
 So much for the basic idea.  Here are the details.
 </para>
 
-<sect2>
+<sect3>
+<title>What a pattern type signature means</title>
+<para>
+A type variable brought into scope by a pattern type signature is simply
+the name for a type.   The restriction they express is that all occurrences
+of the same name mean the same type.  For example:
+<programlisting>
+  f :: [Int] -> Int -> Int
+  f (xs::[a]) (y::a) = (head xs + y) :: a
+</programlisting>
+The pattern type signatures on the left hand side of
+<literal>f</literal> express the fact that <literal>xs</literal>
+must be a list of things of some type <literal>a</literal>; and that <literal>y</literal>
+must have this same type.  The type signature on the expression <literal>(head xs)</literal>
+specifies that this expression must have the same type <literal>a</literal>.
+<emphasis>There is no requirement that the type named by "<literal>a</literal>" is
+in fact a type variable</emphasis>.  Indeed, in this case, the type named by "<literal>a</literal>" is
+<literal>Int</literal>.  (This is a slight liberalisation from the original rather complex
+rules, which specified that a pattern-bound type variable should be universally quantified.)
+For example, all of these are legal:</para>
+
+<programlisting>
+  t (x::a) (y::a) = x+y*2
+
+  f (x::a) (y::b) = [x,y]       -- a unifies with b
+
+  g (x::a) = x + 1::Int         -- a unifies with Int
+
+  h x = let k (y::a) = [x,y]    -- a is free in the
+        in k x                  -- environment
+
+  k (x::a) True    = ...        -- a unifies with Int
+  k (x::Int) False = ...
+
+  w :: [b] -> [b]
+  w (x::a) = x                  -- a unifies with [b]
+</programlisting>
+
+</sect3>
+
+<sect3>
 <title>Scope and implicit quantification</title>
 
 <para>
@@ -2187,60 +2075,104 @@ So much for the basic idea.  Here are the details.
 <listitem>
 
 <para>
- All the type variables mentioned in the patterns for a single
-function definition equation, that are not already in scope,
-are brought into scope by the patterns.  We describe this set as
-the <emphasis>type variables bound by the equation</emphasis>.
-
+All the type variables mentioned in a pattern,
+that are not already in scope,
+are brought into scope by the pattern.  We describe this set as
+the <emphasis>type variables bound by the pattern</emphasis>.
+For example:
+<programlisting>
+  f (x::a) = let g (y::(a,b)) = fst y
+             in
+             g (x,True)
+</programlisting>
+The pattern <literal>(x::a)</literal> brings the type variable
+<literal>a</literal> into scope, as well as the term 
+variable <literal>x</literal>.  The pattern <literal>(y::(a,b))</literal>
+contains an occurrence of the already-in-scope type variable <literal>a</literal>,
+and brings into scope the type variable <literal>b</literal>.
 </para>
 </listitem>
+
 <listitem>
+<para>
+The type variable(s) bound by the pattern have the same scope
+as the term variable(s) bound by the pattern.  For example:
+<programlisting>
+  let
+    f (x::a) = <...rhs of f...>
+    (p::b, q::b) = (1,2)
+  in <...body of let...>
+</programlisting>
+Here, the type variable <literal>a</literal> scopes over the right hand side of <literal>f</literal>,
+just like <literal>x</literal> does; while the type variable <literal>b</literal> scopes over the
+body of the <literal>let</literal>, and all the other definitions in the <literal>let</literal>,
+just like <literal>p</literal> and <literal>q</literal> do.
+Indeed, the newly bound type variables also scope over any ordinary, separate
+type signatures in the <literal>let</literal> group.
+</para>
+</listitem>
+
 
+<listitem>
 <para>
- The type variables thus brought into scope may be mentioned
-in ordinary type signatures or pattern type signatures anywhere within
-their scope.
+The type variables bound by the pattern may be 
+mentioned in ordinary type signatures or pattern 
+type signatures anywhere within their scope.
 
 </para>
 </listitem>
-<listitem>
 
+<listitem>
 <para>
  In ordinary type signatures, any type variable mentioned in the
 signature that is in scope is <emphasis>not</emphasis> universally quantified.
 
 </para>
 </listitem>
+
 <listitem>
 
 <para>
  Ordinary type signatures do not bring any new type variables
 into scope (except in the type signature itself!). So this is illegal:
 
-
 <programlisting>
   f :: a -> a
   f x = x::a
 </programlisting>
 
-
 It's illegal because <VarName>a</VarName> is not in scope in the body of <function>f</function>,
 so the ordinary signature <literal>x::a</literal> is equivalent to <literal>x::forall a.a</literal>;
 and that is an incorrect typing.
 
 </para>
 </listitem>
-<listitem>
 
+<listitem>
 <para>
- There is no implicit universal quantification on pattern type
-signatures, nor may one write an explicit <literal>forall</literal> type in a pattern
-type signature.  The pattern type signature is a monotype.
-
+The pattern type signature is a monotype:
 </para>
+
+<itemizedlist>
+<listitem> <para> 
+A pattern type signature cannot contain any explicit <literal>forall</literal> quantification.
+</para> </listitem>
+
+<listitem>  <para> 
+The type variables bound by a pattern type signature can only be instantiated to monotypes,
+not to type schemes.
+</para> </listitem>
+
+<listitem>  <para> 
+There is no implicit universal quantification on pattern type signatures (in contrast to
+ordinary type signatures).
+</para> </listitem>
+
+</itemizedlist>
+
 </listitem>
-<listitem>
 
+<listitem>
 <para>
 
 The type variables in the head of a <literal>class</literal> or <literal>instance</literal> declaration
@@ -2266,10 +2198,10 @@ scope over the methods defined in the <literal>where</literal> part.  For exampl
 
 </para>
 
-</sect2>
+</sect3>
 
-<sect2>
-<title>Polymorphism</title>
+<sect3>
+<title>Result type signatures</title>
 
 <para>
 
@@ -2277,338 +2209,659 @@ scope over the methods defined in the <literal>where</literal> part.  For exampl
 <listitem>
 
 <para>
- Pattern type signatures are completely orthogonal to ordinary, separate
-type signatures.  The two can be used independently or together.  There is
-no scoping associated with the names of the type variables in a separate type signature.
+ The result type of a function can be given a signature,
+thus:
+
+
+<programlisting>
+  f (x::a) :: [a] = [x,x,x]
+</programlisting>
+
+
+The final <literal>:: [a]</literal> after all the patterns gives a signature to the
+result type.  Sometimes this is the only way of naming the type variable
+you want:
 
 
 <programlisting>
-   f :: [a] -> [a]
-   f (xs::[b]) = reverse xs
+  f :: Int -> [a] -> [a]
+  f n :: ([a] -> [a]) = let g (x::a, y::a) = (y,x)
+                        in \xs -> map g (reverse xs `zip` xs)
 </programlisting>
 
 
 </para>
 </listitem>
-<listitem>
+
+</itemizedlist>
+
+</para>
 
 <para>
- The function must be polymorphic in the type variables
-bound by all its equations.  Operationally, the type variables bound
-by one equation must not:
+Result type signatures are not yet implemented in Hugs.
+</para>
 
+</sect3>
 
+<sect3>
+<title>Where a pattern type signature can occur</title>
+
+<para>
+A pattern type signature can occur in any pattern.  For example:
 <itemizedlist>
-<listitem>
 
+<listitem>
 <para>
- Be unified with a type (such as <literal>Int</literal>, or <literal>[a]</literal>).
+A pattern type signature can be on an arbitrary sub-pattern, not
+ust on a variable:
+
+
+<programlisting>
+  f ((x,y)::(a,b)) = (y,x) :: (b,a)
+</programlisting>
+
+
 </para>
 </listitem>
 <listitem>
 
 <para>
- Be unified with a type variable free in the environment.
+ Pattern type signatures, including the result part, can be used
+in lambda abstractions:
+
+<programlisting>
+  (\ (x::a, y) :: a -> x)
+</programlisting>
 </para>
 </listitem>
 <listitem>
 
 <para>
- Be unified with each other.  (They may unify with the type variables
-bound by another equation for the same function, of course.)
+ Pattern type signatures, including the result part, can be used
+in <literal>case</literal> expressions:
+
+
+<programlisting>
+  case e of { (x::a, y) :: a -> x }
+</programlisting>
+
 </para>
 </listitem>
 
-</itemizedlist>
+<listitem>
+<para>
+To avoid ambiguity, the type after the &ldquo;<literal>::</literal>&rdquo; in a result
+pattern signature on a lambda or <literal>case</literal> must be atomic (i.e. a single
+token or a parenthesised type of some sort).  To see why,
+consider how one would parse this:
 
 
-For example, the following all fail to type check:
+<programlisting>
+  \ x :: a -> b -> x
+</programlisting>
 
 
-<programlisting>
-  f (x::a) (y::b) = [x,y]       -- a unifies with b
+</para>
+</listitem>
 
-  g (x::a) = x + 1::Int         -- a unifies with Int
+<listitem>
 
-  h x = let k (y::a) = [x,y]    -- a is free in the
-        in k x                  -- environment
+<para>
+ Pattern type signatures can bind existential type variables.
+For example:
 
-  k (x::a) True    = ...        -- a unifies with Int
-  k (x::Int) False = ...
 
-  w :: [b] -> [b]
-  w (x::a) = x                  -- a unifies with [b]
+<programlisting>
+  data T = forall a. MkT [a]
+
+  f :: T -> T
+  f (MkT [t::a]) = MkT t3
+                 where
+                   t3::[a] = [t,t,t]
 </programlisting>
 
 
 </para>
 </listitem>
+
+
 <listitem>
 
 <para>
- The pattern-bound type variable may, however, be constrained
-by the context of the principal type, thus:
-
+Pattern type signatures 
+can be used in pattern bindings:
 
 <programlisting>
-  f (x::a) (y::a) = x+y*2
+  f x = let (y, z::a) = x in ...
+  f1 x                = let (y, z::Int) = x in ...
+  f2 (x::(Int,a))     = let (y, z::a)   = x in ...
+  f3 :: (b->b)        = \x -> x
 </programlisting>
 
+In all such cases, the binding is not generalised over the pattern-bound
+type variables.  Thus <literal>f3</literal> is monomorphic; <literal>f3</literal>
+has type <literal>b -&gt; b</literal> for some type <literal>b</literal>, 
+and <emphasis>not</emphasis> <literal>forall b. b -&gt; b</literal>.
+In contrast, the binding
+<programlisting>
+  f4 :: b->b
+  f4 = \x -> x
+</programlisting>
+makes a polymorphic function, but <literal>b</literal> is not in scope anywhere
+in <literal>f4</literal>'s scope.
 
-gets the inferred type: <literal>forall a. Num a =&gt; a -&gt; a -&gt; a</literal>.
 </para>
 </listitem>
-
 </itemizedlist>
-
 </para>
 
+</sect3>
 </sect2>
 
-<sect2>
-<title>Result type signatures</title>
 
-<para>
+</sect1>
+<!-- ==================== End of type system extensions =================  -->
+  
 
-<itemizedlist>
-<listitem>
+<!-- ==================== ASSERTIONS =================  -->
+
+<sect1 id="sec-assertions">
+<title>Assertions
+<indexterm><primary>Assertions</primary></indexterm>
+</title>
 
 <para>
- The result type of a function can be given a signature,
-thus:
+If you want to make use of assertions in your standard Haskell code, you
+could define a function like the following:
+</para>
 
+<para>
 
 <programlisting>
-  f (x::a) :: [a] = [x,x,x]
+assert :: Bool -> a -> a
+assert False x = error "assertion failed!"
+assert _     x = x
 </programlisting>
 
+</para>
 
-The final <literal>:: [a]</literal> after all the patterns gives a signature to the
-result type.  Sometimes this is the only way of naming the type variable
-you want:
+<para>
+which works, but gives you back a less than useful error message --
+an assertion failed, but which and where?
+</para>
+
+<para>
+One way out is to define an extended <function>assert</function> function which also
+takes a descriptive string to include in the error message and
+perhaps combine this with the use of a pre-processor which inserts
+the source location where <function>assert</function> was used.
+</para>
+
+<para>
+Ghc offers a helping hand here, doing all of this for you. For every
+use of <function>assert</function> in the user's source:
+</para>
 
+<para>
 
 <programlisting>
-  f :: Int -> [a] -> [a]
-  f n :: ([a] -> [a]) = let g (x::a, y::a) = (y,x)
-                        in \xs -> map g (reverse xs `zip` xs)
+kelvinToC :: Double -> Double
+kelvinToC k = assert (k &gt;= 0.0) (k+273.15)
 </programlisting>
 
+</para>
 
+<para>
+Ghc will rewrite this to also include the source location where the
+assertion was made,
 </para>
-</listitem>
 
-</itemizedlist>
+<para>
+
+<programlisting>
+assert pred val ==> assertError "Main.hs|15" pred val
+</programlisting>
 
 </para>
 
 <para>
-Result type signatures are not yet implemented in Hugs.
+The rewrite is only performed by the compiler when it spots
+applications of <function>Control.Exception.assert</function>, so you
+can still define and use your own versions of
+<function>assert</function>, should you so wish. If not, import
+<literal>Control.Exception</literal> to make use
+<function>assert</function> in your code.
 </para>
 
-</sect2>
-
-<sect2>
-<title>Pattern signatures on other constructs</title>
+<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
+<literal>assert pred e</literal> will be rewritten to
+<literal>e</literal>.
+</para>
 
 <para>
+Assertion failures can be caught, see the documentation for the
+<literal>Control.Exception</literal> library for the details.
+</para>
 
-<itemizedlist>
-<listitem>
+</sect1>
 
-<para>
- A pattern type signature can be on an arbitrary sub-pattern, not
-just on a variable:
 
+<sect1 id="syntax-extns">
+<title>Syntactic extensions</title>
+
+<!-- ====================== HIERARCHICAL MODULES =======================  -->
+
+    <sect2 id="hierarchical-modules">
+      <title>Hierarchical Modules</title>
+
+      <para>GHC supports a small extension to the syntax of module
+      names: a module name is allowed to contain a dot
+      <literal>&lsquo;.&rsquo;</literal>.  This is also known as the
+      &ldquo;hierarchical module namespace&rdquo; extension, because
+      it extends the normally flat Haskell module namespace into a
+      more flexible hierarchy of modules.</para>
+
+      <para>This extension has very little impact on the language
+      itself; modules names are <emphasis>always</emphasis> fully
+      qualified, so you can just think of the fully qualified module
+      name as <quote>the module name</quote>.  In particular, this
+      means that the full module name must be given after the
+      <literal>module</literal> keyword at the beginning of the
+      module; for example, the module <literal>A.B.C</literal> must
+      begin</para>
+
+<programlisting>module A.B.C</programlisting>
+
+
+      <para>It is a common strategy to use the <literal>as</literal>
+      keyword to save some typing when using qualified names with
+      hierarchical modules.  For example:</para>
 
 <programlisting>
-  f ((x,y)::(a,b)) = (y,x) :: (b,a)
+import qualified Control.Monad.ST.Strict as ST
 </programlisting>
 
+      <para>Hierarchical modules have an impact on the way that GHC
+      searches for files.  For a description, see <xref
+      linkend="finding-hierarchical-modules">.</para>
 
-</para>
-</listitem>
-<listitem>
+      <para>GHC comes with a large collection of libraries arranged
+      hierarchically; see the accompanying library documentation.
+      There is an ongoing project to create and maintain a stable set
+      of <quote>core</quote> libraries used by several Haskell
+      compilers, and the libraries that GHC comes with represent the
+      current status of that project.  For more details, see <ulink
+      url="http://www.haskell.org/~simonmar/libraries/libraries.html">Haskell
+      Libraries</ulink>.</para>
+
+    </sect2>
+
+<!-- ====================== PATTERN GUARDS =======================  -->
+
+<sect2 id="pattern-guards">
+<title>Pattern guards</title>
 
 <para>
- Pattern type signatures, including the result part, can be used
-in lambda abstractions:
+<indexterm><primary>Pattern guards (Glasgow extension)</primary></indexterm>
+The discussion that follows is an abbreviated version of Simon Peyton Jones's original <ULink URL="http://research.microsoft.com/~simonpj/Haskell/guards.html">proposal</ULink>. (Note that the proposal was written before pattern guards were implemented, so refers to them as unimplemented.)
+</para>
 
+<para>
+Suppose we have an abstract data type of finite maps, with a
+lookup operation:
 
 <programlisting>
-  (\ (x::a, y) :: a -> x)
+lookup :: FiniteMap -> Int -> Maybe Int
 </programlisting>
 
+The lookup returns <function>Nothing</function> if the supplied key is not in the domain of the mapping, and <function>(Just v)</function> otherwise,
+where <VarName>v</VarName> is the value that the key maps to.  Now consider the following definition:
+</para>
 
-Type variables bound by these patterns must be polymorphic in
-the sense defined above.
-For example:
+<programlisting>
+clunky env var1 var2 | ok1 && ok2 = val1 + val2
+| otherwise  = var1 + var2
+where
+  m1 = lookup env var1
+  m2 = lookup env var2
+  ok1 = maybeToBool m1
+  ok2 = maybeToBool m2
+  val1 = expectJust m1
+  val2 = expectJust m2
+</programlisting>
 
+<para>
+The auxiliary functions are 
+</para>
 
 <programlisting>
-  f1 (x::c) = f1 x      -- ok
-  f2 = \(x::c) -> f2 x  -- not ok
-</programlisting>
+maybeToBool :: Maybe a -&gt; Bool
+maybeToBool (Just x) = True
+maybeToBool Nothing  = False
 
+expectJust :: Maybe a -&gt; a
+expectJust (Just x) = x
+expectJust Nothing  = error "Unexpected Nothing"
+</programlisting>
 
-Here, <function>f1</function> is OK, but <function>f2</function> is not, because <VarName>c</VarName> gets unified
-with a type variable free in the environment, in this
-case, the type of <function>f2</function>, which is in the environment when
-the lambda abstraction is checked.
+<para>
+What is <function>clunky</function> doing? The guard <literal>ok1 &&
+ok2</literal> checks that both lookups succeed, using
+<function>maybeToBool</function> to convert the <function>Maybe</function>
+types to booleans. The (lazily evaluated) <function>expectJust</function>
+calls extract the values from the results of the lookups, and binds the
+returned values to <VarName>val1</VarName> and <VarName>val2</VarName>
+respectively.  If either lookup fails, then clunky takes the
+<literal>otherwise</literal> case and returns the sum of its arguments.
+</para>
 
+<para>
+This is certainly legal Haskell, but it is a tremendously verbose and
+un-obvious way to achieve the desired effect.  Arguably, a more direct way
+to write clunky would be to use case expressions:
 </para>
-</listitem>
-<listitem>
+
+<programlisting>
+clunky env var1 var1 = case lookup env var1 of
+  Nothing -&gt; fail
+  Just val1 -&gt; case lookup env var2 of
+    Nothing -&gt; fail
+    Just val2 -&gt; val1 + val2
+where
+  fail = val1 + val2
+</programlisting>
 
 <para>
- Pattern type signatures, including the result part, can be used
-in <literal>case</literal> expressions:
+This is a bit shorter, but hardly better.  Of course, we can rewrite any set
+of pattern-matching, guarded equations as case expressions; that is
+precisely what the compiler does when compiling equations! The reason that
+Haskell provides guarded equations is because they allow us to write down
+the cases we want to consider, one at a time, independently of each other. 
+This structure is hidden in the case version.  Two of the right-hand sides
+are really the same (<function>fail</function>), and the whole expression
+tends to become more and more indented. 
+</para>
 
+<para>
+Here is how I would write clunky:
+</para>
 
 <programlisting>
-  case e of { (x::a, y) :: a -> x }
+clunky env var1 var1
+  | Just val1 &lt;- lookup env var1
+  , Just val2 &lt;- lookup env var2
+  = val1 + val2
+...other equations for clunky...
 </programlisting>
 
+<para>
+The semantics should be clear enough.  The qualifers are matched in order. 
+For a <literal>&lt;-</literal> qualifier, which I call a pattern guard, the
+right hand side is evaluated and matched against the pattern on the left. 
+If the match fails then the whole guard fails and the next equation is
+tried.  If it succeeds, then the appropriate binding takes place, and the
+next qualifier is matched, in the augmented environment.  Unlike list
+comprehensions, however, the type of the expression to the right of the
+<literal>&lt;-</literal> is the same as the type of the pattern to its
+left.  The bindings introduced by pattern guards scope over all the
+remaining guard qualifiers, and over the right hand side of the equation.
+</para>
 
-The pattern-bound type variables must, as usual,
-be polymorphic in the following sense: each case alternative,
-considered as a lambda abstraction, must be polymorphic.
-Thus this is OK:
-
+<para>
+Just as with list comprehensions, boolean expressions can be freely mixed
+with among the pattern guards.  For example:
+</para>
 
 <programlisting>
-  case (True,False) of { (x::a, y) -> x }
+f x | [y] <- x
+    , y > 3
+    , Just z <- h y
+    = ...
 </programlisting>
 
+<para>
+Haskell's current guards therefore emerge as a special case, in which the
+qualifier list has just one element, a boolean expression.
+</para>
+</sect2>
 
-Even though the context is that of a pair of booleans,
-the alternative itself is polymorphic.  Of course, it is
-also OK to say:
+<!-- ===================== Recursive do-notation ===================  -->
 
+<sect2 id="mdo-notation">
+<title>The recursive do-notation
+</title>
 
+<para> The recursive do-notation (also known as mdo-notation) is implemented as described in
+"A recursive do for Haskell",
+Levent Erkok, John Launchbury",
+Haskell Workshop 2002, pages: 29-37. Pittsburgh, Pennsylvania. 
+</para>
+<para>
+The do-notation of Haskell does not allow <emphasis>recursive bindings</emphasis>,
+that is, the variables bound in a do-expression are visible only in the textually following 
+code block. Compare this to a let-expression, where bound variables are visible in the entire binding
+group. It turns out that several applications can benefit from recursive bindings in
+the do-notation, and this extension provides the necessary syntactic support.
+</para>
+<para>
+Here is a simple (yet contrived) example:
+</para>
 <programlisting>
-  case (True,False) of { (x::Bool, y) -> x }
+justOnes = mdo xs <- Just (1:xs)
+               return xs
 </programlisting>
-
-
+<para>
+As you can guess <literal>justOnes</literal> will evaluate to <literal>Just [1,1,1,...</literal>.
 </para>
-</listitem>
-<listitem>
 
 <para>
-To avoid ambiguity, the type after the &ldquo;<literal>::</literal>&rdquo; in a result
-pattern signature on a lambda or <literal>case</literal> must be atomic (i.e. a single
-token or a parenthesised type of some sort).  To see why,
-consider how one would parse this:
-
-
+The MonadFix library introduces the <literal>MonadFix</literal> class. It's definition is:
+</para>
 <programlisting>
-  \ x :: a -> b -> x
+class Monad m => MonadFix m where
+   mfix :: (a -> m a) -> m a
 </programlisting>
+<para>
+The function <literal>mfix</literal>
+dictates how the required recursion operation should be performed. If recursive bindings are required for a monad,
+then that monad must be declared an instance of the <literal>MonadFix</literal> class.
+For details, see the above mentioned reference.
+</para>
+<para>
+The <literal>MonadFix</literal> library automatically declares List, Maybe, IO, and
+state monads (both lazy and strict) as instances of the <literal>MonadFix</literal> class.
+</para>
+<para>
+There are three important points in using the recursive-do notation:
+<itemizedlist>
+<listitem><para>
+The recursive version of the do-notation uses the keyword <literal>mdo</literal> (rather
+than <literal>do</literal>).
+</para></listitem>
+
+<listitem><para>
+If you want to declare an instance of the <literal>MonadFix</literal> class for one of 
+your own monads, or you need to refer to the class name <literal>MonadFix</literal> in any other way (for instance in
+writing a type constraint), then your program should <literal>import Control.Monad.MonadFix</literal>.
+Otherwise, you don't need to import any special libraries to use the mdo-notation. That is,
+as long as you only use the predefined instances mentioned above, the mdo-notation will
+be automatically available. (Note: This differs from the Hugs implementation, where
+<literal>MonadFix</literal> should always be imported.)
+</para></listitem>
+
+<listitem><para>
+As with other extensions, ghc should be given the flag <literal>-fglasgow-exts</literal>
+</para></listitem>
+</itemizedlist>
+</para>
 
-
+<para>
+Historical note: The originial implementation of the mdo-notation, and most
+of the existing documents, use the names 
+<literal>MonadRec</literal> for the class, and 
+<literal>Control.Monad.MonadRec</literal> for the library. These names
+are no longer supported.
 </para>
-</listitem>
-<listitem>
 
 <para>
- Pattern type signatures that bind new type variables
-may not be used in pattern bindings at all.
-So this is illegal:
+The web page: <ulink url="http://www.cse.ogi.edu/PacSoft/projects/rmb">http://www.cse.ogi.edu/PacSoft/projects/rmb</ulink>
+contains up to date information on recursive monadic bindings.
+</para>
 
+</sect2>
 
-<programlisting>
-  f x = let (y, z::a) = x in ...
-</programlisting>
+<!-- ===================== PARALLEL LIST COMPREHENSIONS ===================  -->
 
+  <sect2 id="parallel-list-comprehensions">
+    <title>Parallel List Comprehensions</title>
+    <indexterm><primary>list comprehensions</primary><secondary>parallel</secondary>
+    </indexterm>
+    <indexterm><primary>parallel list comprehensions</primary>
+    </indexterm>
 
-But these are OK, because they do not bind fresh type variables:
+    <para>Parallel list comprehensions are a natural extension to list
+    comprehensions.  List comprehensions can be thought of as a nice
+    syntax for writing maps and filters.  Parallel comprehensions
+    extend this to include the zipWith family.</para>
 
+    <para>A parallel list comprehension has multiple independent
+    branches of qualifier lists, each separated by a `|' symbol.  For
+    example, the following zips together two lists:</para>
 
 <programlisting>
-  f1 x            = let (y, z::Int) = x in ...
-  f2 (x::(Int,a)) = let (y, z::a)   = x in ...
+   [ (x, y) | x <- xs | y <- ys ] 
 </programlisting>
 
+    <para>The behavior of parallel list comprehensions follows that of
+    zip, in that the resulting list will have the same length as the
+    shortest branch.</para>
 
-However a single variable is considered a degenerate function binding,
-rather than a degerate pattern binding, so this is permitted, even
-though it binds a type variable:
+    <para>We can define parallel list comprehensions by translation to
+    regular comprehensions.  Here's the basic idea:</para>
 
+    <para>Given a parallel comprehension of the form: </para>
 
 <programlisting>
-  f :: (b->b) = \(x::b) -> x
+   [ e | p1 <- e11, p2 <- e12, ... 
+       | q1 <- e21, q2 <- e22, ... 
+       ... 
+   ] 
 </programlisting>
 
-
-</para>
-</listitem>
-
-</itemizedlist>
-
-Such degnerate function bindings do not fall under the monomorphism
-restriction.  Thus:
-</para>
-
-<para>
+    <para>This will be translated to: </para>
 
 <programlisting>
-  g :: a -> a -> Bool = \x y. x==y
+   [ e | ((p1,p2), (q1,q2), ...) <- zipN [(p1,p2) | p1 <- e11, p2 <- e12, ...] 
+                                         [(q1,q2) | q1 <- e21, q2 <- e22, ...] 
+                                         ... 
+   ] 
 </programlisting>
 
-</para>
+    <para>where `zipN' is the appropriate zip for the given number of
+    branches.</para>
 
-<para>
-Here <function>g</function> has type <literal>forall a. Eq a =&gt; a -&gt; a -&gt; Bool</literal>, just as if
-<function>g</function> had a separate type signature.  Lacking a type signature, <function>g</function>
-would get a monomorphic type.
-</para>
+  </sect2>
 
-</sect2>
+<sect2 id="rebindable-syntax">
+<title>Rebindable syntax</title>
 
-<sect2>
-<title>Existentials</title>
 
-<para>
+      <para>GHC allows most kinds of built-in syntax to be rebound by
+      the user, to facilitate replacing the <literal>Prelude</literal>
+      with a home-grown version, for example.</para>
 
-<itemizedlist>
-<listitem>
+            <para>You may want to define your own numeric class
+            hierarchy.  It completely defeats that purpose if the
+            literal "1" means "<literal>Prelude.fromInteger
+            1</literal>", which is what the Haskell Report specifies.
+            So the <option>-fno-implicit-prelude</option> flag causes
+            the following pieces of built-in syntax to refer to
+            <emphasis>whatever is in scope</emphasis>, not the Prelude
+            versions:</para>
 
-<para>
- Pattern type signatures can bind existential type variables.
-For example:
+           <itemizedlist>
+             <listitem>
+               <para>Integer and fractional literals mean
+                "<literal>fromInteger 1</literal>" and
+                "<literal>fromRational 3.2</literal>", not the
+                Prelude-qualified versions; both in expressions and in
+                patterns. </para>
+               <para>However, the standard Prelude <literal>Eq</literal> class
+               is still used for the equality test necessary for literal patterns.</para>
+             </listitem>
+
+             <listitem>
+               <para>Negation (e.g. "<literal>- (f x)</literal>")
+               means "<literal>negate (f x)</literal>" (not
+               <literal>Prelude.negate</literal>).</para>
+             </listitem>
 
+             <listitem>
+               <para>In an n+k pattern, the standard Prelude
+                <literal>Ord</literal> class is still used for comparison,
+                but the necessary subtraction uses whatever
+                "<literal>(-)</literal>" is in scope (not
+                "<literal>Prelude.(-)</literal>").</para>
+             </listitem>
 
-<programlisting>
-  data T = forall a. MkT [a]
+             <listitem>
+         <para>"Do" notation is translated using whatever
+             functions <literal>(>>=)</literal>,
+             <literal>(>>)</literal>, <literal>fail</literal>, and
+             <literal>return</literal>, are in scope (not the Prelude
+             versions).  List comprehensions, and parallel array
+             comprehensions, are unaffected.  </para></listitem>
+           </itemizedlist>
 
-  f :: T -> T
-  f (MkT [t::a]) = MkT t3
-                 where
-                   t3::[a] = [t,t,t]
-</programlisting>
+            <para>Be warned: this is an experimental facility, with fewer checks than
+            usual.  In particular, it is essential that the functions GHC finds in scope
+            must have the appropriate types, namely:
+            <screen>
+               fromInteger  :: forall a. (...) => Integer  -> a
+               fromRational :: forall a. (...) => Rational -> a
+               negate       :: forall a. (...) => a -> a
+               (-)          :: forall a. (...) => a -> a -> a
+               (>>=)        :: forall m a. (...) => m a -> (a -> m b) -> m b
+               (>>)         :: forall m a. (...) => m a -> m b -> m b
+               return       :: forall m a. (...) => a      -> m a
+               fail         :: forall m a. (...) => String -> m a
+            </screen>
+            (The (...) part can be any context including the empty context; that part 
+            is up to you.)
+            If the functions don't have the right type, very peculiar things may 
+            happen.  Use <literal>-dcore-lint</literal> to
+            typecheck the desugared program.  If Core Lint is happy you should be all right.</para>
 
+</sect2>
+</sect1>
 
-</para>
-</listitem>
+<!-- =============================== PRAGMAS ===========================  -->
 
-</itemizedlist>
+  <sect1 id="pragmas">
+    <title>Pragmas</title>
 
-</para>
+    <indexterm><primary>pragma</primary></indexterm>
 
-</sect2>
+    <para>GHC supports several pragmas, or instructions to the
+    compiler placed in the source code.  Pragmas don't normally affect
+    the meaning of the program, but they might affect the efficiency
+    of the generated code.</para>
 
-</sect1>
+    <para>Pragmas all take the form
 
-<sect1 id="pragmas">
-<title>Pragmas
-</title>
+<literal>{-# <replaceable>word</replaceable> ... #-}</literal>  
 
-<para>
-GHC supports several pragmas, or instructions to the compiler placed
-in the source code.  Pragmas don't affect the meaning of the program,
-but they might affect the efficiency of the generated code.
-</para>
+    where <replaceable>word</replaceable> indicates the type of
+    pragma, and is followed optionally by information specific to that
+    type of pragma.  Case is ignored in
+    <replaceable>word</replaceable>.  The various values for
+    <replaceable>word</replaceable> that GHC understands are described
+    in the following sections; any pragma encountered with an
+    unrecognised <replaceable>word</replaceable> is (silently)
+    ignored.</para>
 
 <sect2 id="inline-pragma">
 <title>INLINE pragma
@@ -2680,17 +2933,23 @@ For example, in GHC's own <literal>UniqueSupply</literal> monad code, we have:
 <title>NOINLINE pragma
 </title>
 
-<para>
 <indexterm><primary>NOINLINE pragma</primary></indexterm>
-<indexterm><primary>pragma, NOINLINE</primary></indexterm>
-</para>
+<indexterm><primary>pragma</primary><secondary>NOINLINE</secondary></indexterm>
+<indexterm><primary>NOTINLINE pragma</primary></indexterm>
+<indexterm><primary>pragma</primary><secondary>NOTINLINE</secondary></indexterm>
 
 <para>
-The <literal>NOINLINE</literal> pragma does exactly what you'd expect: it stops the
-named function from being inlined by the compiler.  You shouldn't ever
-need to do this, unless you're very cautious about code size.
+The <literal>NOINLINE</literal> pragma does exactly what you'd expect:
+it stops the named function from being inlined by the compiler.  You
+shouldn't ever need to do this, unless you're very cautious about code
+size.
 </para>
 
+<para><literal>NOTINLINE</literal> is a synonym for
+<literal>NOINLINE</literal> (<literal>NOTINLINE</literal> is specified
+by Haskell 98 as the standard way to disable inlining, so it should be
+used if you want your code to be portable).</para>
+
 </sect2>
 
     <sect2 id="specialize-pragma">
@@ -2768,12 +3027,17 @@ i2d (I# i) = D# (int2Double# i) -- uses Glasgow prim-op directly
 Same idea, except for instance declarations.  For example:
 
 <programlisting>
-instance (Eq a) => Eq (Foo a) where { ... usual stuff ... }
-
-{-# SPECIALIZE instance Eq (Foo [(Int, Bar)] #-}
+instance (Eq a) => Eq (Foo a) where { 
+   {-# SPECIALIZE instance Eq (Foo [(Int, Bar)]) #-}
+   ... usual stuff ...
+ }
 </programlisting>
-
-Compatible with HBC, by the way.
+The pragma must occur inside the <literal>where</literal> part
+of the instance declaration.
+</para>
+<para>
+Compatible with HBC, by the way, except perhaps in the placement
+of the pragma.
 </para>
 
 </sect2>
@@ -2820,8 +3084,46 @@ The RULES pragma lets you specify rewrite rules.  It is described in
 
 </sect2>
 
+<sect2 id="deprecated-pragma">
+<title>DEPRECATED pragma</title>
+
+<para>
+The DEPRECATED pragma lets you specify that a particular function, class, or type, is deprecated.  
+There are two forms.  
+</para>
+<itemizedlist>
+<listitem><para>
+You can deprecate an entire module thus:</para>
+<programlisting>
+   module Wibble {-# DEPRECATED "Use Wobble instead" #-} where
+     ...
+</programlisting>
+<para>
+When you compile any module that import <literal>Wibble</literal>, GHC will print
+the specified message.</para>
+</listitem>
+
+<listitem>
+<para>
+You can deprecate a function, class, or type, with the following top-level declaration:
+</para>
+<programlisting>
+   {-# DEPRECATED f, C, T "Don't use these" #-}
+</programlisting>
+<para>
+When you compile any module that imports and uses any of the specifed entities, 
+GHC will print the specified message.
+</para>
+</listitem>
+</itemizedlist>
+<para>You can suppress the warnings with the flag <option>-fno-warn-deprecations</option>.</para>
+
+</sect2>
+
 </sect1>
 
+<!--  ======================= REWRITE RULES ======================== -->
+
 <sect1 id="rewrite-rules">
 <title>Rewrite rules
 
@@ -3125,14 +3427,14 @@ The following are good producers:
  <function>++</function>
 </para>
 </listitem>
-<listitem>
 
+<listitem>
 <para>
  <function>map</function>
 </para>
 </listitem>
-<listitem>
 
+<listitem>
 <para>
  <function>filter</function>
 </para>
@@ -3182,8 +3484,14 @@ The following are good consumers:
  <function>++</function> (on its first argument)
 </para>
 </listitem>
+
 <listitem>
+<para>
+ <function>foldr</function>
+</para>
+</listitem>
 
+<listitem>
 <para>
  <function>map</function>
 </para>
@@ -3377,6 +3685,9 @@ program even if fusion doesn't happen.  More rules in <filename>PrelList.lhs</fi
 <sect1 id="generic-classes">
 <title>Generic classes</title>
 
+    <para>(Note: support for generic classes is currently broken in
+    GHC 5.02).</para>
+
 <para>
 The ideas behind this extension are described in detail in "Derivable type classes",
 Ralf Hinze and Simon Peyton Jones, Haskell Workshop, Montreal Sept 2000, pp94-105.
@@ -3426,7 +3737,10 @@ where clause and over-ride whichever methods you please.
       <para>To use generics you need to</para>
       <itemizedlist>
        <listitem>
-         <para>Use the <option>-fgenerics</option> flag.</para>
+         <para>Use the flags <option>-fglasgow-exts</option> (to enable the extra syntax), 
+                <option>-fgenerics</option> (to generate extra per-data-type code),
+                and <option>-package lang</option> (to make the <literal>Generics</literal> library
+                available.  </para>
        </listitem>
        <listitem>
          <para>Import the module <literal>Generics</literal> from the
@@ -3529,10 +3843,10 @@ So this too is illegal:
 <programlisting>
   class Foo a where
     op1 :: a -> Bool
-    op {| a :*: b |} (Inl x) = True
+    op1 {| a :*: b |} (x :*: y) = True
 
     op2 :: a -> Bool
-    op {| p :*: q |} (Inr y) = False
+    op2 {| p :*: q |} (x :*: y) = False
 </programlisting>
 (The reason for this restriction is that we gather all the equations for a particular type consructor
 into a single generic instance declaration.)
@@ -3624,6 +3938,182 @@ Just to finish with, here's another example I rather like:
 </sect2>
 </sect1>
 
+<sect1 id="newtype-deriving">
+<title>Generalised derived instances for newtypes</title>
+
+<para>
+When you define an abstract type using <literal>newtype</literal>, you may want
+the new type to inherit some instances from its representation. In
+Haskell 98, you can inherit instances of <literal>Eq</literal>, <literal>Ord</literal>,
+<literal>Enum</literal> and <literal>Bounded</literal> by deriving them, but for any
+other classes you have to write an explicit instance declaration. For
+example, if you define
+
+<programlisting> 
+  newtype Dollars = Dollars Int 
+</programlisting> 
+
+and you want to use arithmetic on <literal>Dollars</literal>, you have to
+explicitly define an instance of <literal>Num</literal>:
+
+<programlisting> 
+  instance Num Dollars where
+    Dollars a + Dollars b = Dollars (a+b)
+    ...
+</programlisting>
+All the instance does is apply and remove the <literal>newtype</literal>
+constructor. It is particularly galling that, since the constructor
+doesn't appear at run-time, this instance declaration defines a
+dictionary which is <emphasis>wholly equivalent</emphasis> to the <literal>Int</literal>
+dictionary, only slower!
+</para>
+
+<sect2> <title> Generalising the deriving clause </title>
+<para>
+GHC now permits such instances to be derived instead, so one can write 
+<programlisting> 
+  newtype Dollars = Dollars Int deriving (Eq,Show,Num)
+</programlisting> 
+
+and the implementation uses the <emphasis>same</emphasis> <literal>Num</literal> dictionary
+for <literal>Dollars</literal> as for <literal>Int</literal>. Notionally, the compiler
+derives an instance declaration of the form
+
+<programlisting> 
+  instance Num Int => Num Dollars
+</programlisting> 
+
+which just adds or removes the <literal>newtype</literal> constructor according to the type.
+</para>
+<para>
+
+We can also derive instances of constructor classes in a similar
+way. For example, suppose we have implemented state and failure monad
+transformers, such that
+
+<programlisting> 
+  instance Monad m => Monad (State s m) 
+  instance Monad m => Monad (Failure m)
+</programlisting> 
+In Haskell 98, we can define a parsing monad by 
+<programlisting> 
+  type Parser tok m a = State [tok] (Failure m) a
+</programlisting> 
+
+which is automatically a monad thanks to the instance declarations
+above. With the extension, we can make the parser type abstract,
+without needing to write an instance of class <literal>Monad</literal>, via
+
+<programlisting> 
+  newtype Parser tok m a = Parser (State [tok] (Failure m) a)
+                         deriving Monad
+</programlisting>
+In this case the derived instance declaration is of the form 
+<programlisting> 
+  instance Monad (State [tok] (Failure m)) => Monad (Parser tok m) 
+</programlisting> 
+
+Notice that, since <literal>Monad</literal> is a constructor class, the
+instance is a <emphasis>partial application</emphasis> of the new type, not the
+entire left hand side. We can imagine that the type declaration is
+``eta-converted'' to generate the context of the instance
+declaration.
+</para>
+<para>
+
+We can even derive instances of multi-parameter classes, provided the
+newtype is the last class parameter. In this case, a ``partial
+application'' of the class appears in the <literal>deriving</literal>
+clause. For example, given the class
+
+<programlisting> 
+  class StateMonad s m | m -> s where ... 
+  instance Monad m => StateMonad s (State s m) where ... 
+</programlisting> 
+then we can derive an instance of <literal>StateMonad</literal> for <literal>Parser</literal>s by 
+<programlisting> 
+  newtype Parser tok m a = Parser (State [tok] (Failure m) a)
+                         deriving (Monad, StateMonad [tok])
+</programlisting>
+
+The derived instance is obtained by completing the application of the
+class to the new type:
+
+<programlisting> 
+  instance StateMonad [tok] (State [tok] (Failure m)) =>
+           StateMonad [tok] (Parser tok m)
+</programlisting>
+</para>
+<para>
+
+As a result of this extension, all derived instances in newtype
+declarations are treated uniformly (and implemented just by reusing
+the dictionary for the representation type), <emphasis>except</emphasis>
+<literal>Show</literal> and <literal>Read</literal>, which really behave differently for
+the newtype and its representation.
+</para>
+</sect2>
+
+<sect2> <title> A more precise specification </title>
+<para>
+Derived instance declarations are constructed as follows. Consider the
+declaration (after expansion of any type synonyms)
+
+<programlisting> 
+  newtype T v1...vn = T' (S t1...tk vk+1...vn) deriving (c1...cm) 
+</programlisting> 
+
+where <literal>S</literal> is a type constructor, <literal>t1...tk</literal> are 
+types,
+<literal>vk+1...vn</literal> are type variables which do not occur in any of
+the <literal>ti</literal>, and the <literal>ci</literal> are partial applications of
+classes of the form <literal>C t1'...tj'</literal>.  The derived instance
+declarations are, for each <literal>ci</literal>,
+
+<programlisting> 
+  instance ci (S t1...tk vk+1...v) => ci (T v1...vp)
+</programlisting>
+where <literal>p</literal> is chosen so that <literal>T v1...vp</literal> is of the 
+right <emphasis>kind</emphasis> for the last parameter of class <literal>Ci</literal>.
+</para>
+<para>
+
+As an example which does <emphasis>not</emphasis> work, consider 
+<programlisting> 
+  newtype NonMonad m s = NonMonad (State s m s) deriving Monad 
+</programlisting> 
+Here we cannot derive the instance 
+<programlisting> 
+  instance Monad (State s m) => Monad (NonMonad m) 
+</programlisting> 
+
+because the type variable <literal>s</literal> occurs in <literal>State s m</literal>,
+and so cannot be "eta-converted" away. It is a good thing that this
+<literal>deriving</literal> clause is rejected, because <literal>NonMonad m</literal> is
+not, in fact, a monad --- for the same reason. Try defining
+<literal>>>=</literal> with the correct type: you won't be able to.
+</para>
+<para>
+
+Notice also that the <emphasis>order</emphasis> of class parameters becomes
+important, since we can only derive instances for the last one. If the
+<literal>StateMonad</literal> class above were instead defined as
+
+<programlisting> 
+  class StateMonad m s | m -> s where ... 
+</programlisting>
+
+then we would not have been able to derive an instance for the
+<literal>Parser</literal> type above. We hypothesise that multi-parameter
+classes usually have one "main" parameter for which deriving new
+instances is most interesting.
+</para>
+</sect2>
+
+</sect1>
+
+
+
 <!-- Emacs stuff:
      ;;; Local Variables: ***
      ;;; mode: sgml ***