[project @ 2005-07-22 10:05:11 by simonpj]

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

diff --git a/ghc/docs/users_guide/glasgow_exts.xml b/ghc/docs/users_guide/glasgow_exts.xml
index a1c44ba..4da043b 100644 (file)
--- a/ghc/docs/users_guide/glasgow_exts.xml
+++ b/ghc/docs/users_guide/glasgow_exts.xml
@@ -3413,6 +3413,68 @@ the standard method is used or the one described here.)
 
 </sect2>
 
+<sect2 id="typing-binds">
+<title>Generalised typing of mutually recursive bindings</title>
+
+<para>
+The Haskell Report specifies that a group of bindings (at top level, or in a
+<literal>let</literal> or <literal>where</literal>) should be sorted into
+strongly-connected components, and then type-checked in dependency order
+(<ulink url="http://haskell.org/onlinereport/decls.html#sect4.5.1">Haskell
+Report, Section 4.5.1</ulink>).  
+As each group is type-checked, any binders of the group that
+have
+an explicit type signature are put in the type environment with the specified
+polymorphic type,
+and all others are monomorphic until the group is generalised 
+(<ulink url="http://haskell.org/onlinereport/decls.html#sect4.5.2">Haskell Report, Section 4.5.2</ulink>).
+</para>
+
+<para>Following a suggestion of Mark Jones, in his paper
+<ulink url="http://www.cse.ogi.edu/~mpj/thih/">Typing Haskell in
+Haskell</ulink>,
+GHC implements a more general scheme.  If <option>-fglasgow-exts</option> is
+specified:
+<emphasis>the dependency analysis ignores references to variables that have an explicit
+type signature</emphasis>.
+As a result of this refined dependency analysis, the dependency groups are smaller, and more bindings will
+typecheck.  For example, consider:
+<programlisting>
+  f :: Eq a =&gt; a -> Bool
+  f x = (x == x) || g True || g "Yes"
+  
+  g y = (y &lt;= y) || f True
+</programlisting>
+This is rejected by Haskell 98, but under Jones's scheme the definition for
+<literal>g</literal> is typechecked first, separately from that for
+<literal>f</literal>,
+because the reference to <literal>f</literal> in <literal>g</literal>'s right
+hand side is ingored by the dependency analysis.  Then <literal>g</literal>'s
+type is generalised, to get
+<programlisting>
+  g :: Ord a =&gt; a -> Bool
+</programlisting>
+Now, the defintion for <literal>f</literal> is typechecked, with this type for
+<literal>g</literal> in the type environment.
+</para>
+
+<para>
+The same refined dependency analysis also allows the type signatures of 
+mutually-recursive functions to have different contexts, something that is illegal in
+Haskell 98 (Section 4.5.2, last sentence).  With
+<option>-fglasgow-exts</option>
+GHC only insists that the type signatures of a <emphasis>refined</emphasis> group have identical
+type signatures; in practice this means that only variables bound by the same
+pattern binding must have the same context.  For example, this is fine:
+<programlisting>
+  f :: Eq a =&gt; a -> Bool
+  f x = (x == x) || g True
+  
+  g :: Ord a =&gt; a -> Bool
+  g y = (y &lt;= y) || f True
+</programlisting>
+</para>
+</sect2>
 
 </sect1>
 <!-- ==================== End of type system extensions =================  -->
@@ -4612,7 +4674,7 @@ key_function :: Int -> String -> (Bool, Double)
       overloaded function:</para>
 
 <programlisting>
-hammeredLookup :: Ord key => [(key, value)] -> key -> value
+  hammeredLookup :: Ord key => [(key, value)] -> key -> value
 </programlisting>
 
       <para>If it is heavily used on lists with
@@ -4620,7 +4682,7 @@ hammeredLookup :: Ord key => [(key, value)] -> key -> value
       follows:</para>
 
 <programlisting>
-{-# SPECIALIZE hammeredLookup :: [(Widget, value)] -> Widget -> value #-}
+  {-# SPECIALIZE hammeredLookup :: [(Widget, value)] -> Widget -> value #-}
 </programlisting>
 
       <para>A <literal>SPECIALIZE</literal> pragma for a function can
@@ -4631,7 +4693,35 @@ hammeredLookup :: Ord key => [(key, value)] -> key -> value
       (see <xref linkend="rewrite-rules"/>) that rewrites a call to the
       un-specialised function into a call to the specialised one.</para>
 
-      <para>In earlier versions of GHC, it was possible to provide your own
+      <para>The type in a SPECIALIZE pragma can be any type that is less
+       polymorphic than the type of the original function.  In concrete terms,
+       if the original function is <literal>f</literal> then the pragma
+<programlisting>
+  {-# SPECIALIZE f :: &lt;type&gt; #-}
+</programlisting>
+      is valid if and only if the defintion
+<programlisting>
+  f_spec :: &lt;type&gt;
+  f_spec = f
+</programlisting>
+      is valid.  Here are some examples (where we only give the type signature
+      for the original function, not its code):
+<programlisting>
+  f :: Eq a => a -> b -> b
+  {-# SPECIALISE g :: Int -> b -> b #-}
+
+  g :: (Eq a, Ix b) => a -> b -> b
+  {-# SPECIALISE g :: (Eq a) => a -> Int -> Int #-}
+
+  h :: Eq a => a -> a -> a
+  {-# SPECIALISE h :: (Eq a) => [a] -> [a] -> [a] #-}
+</programlisting>  
+The last of these examples will generate a 
+RULE with a somewhat-complex left-hand side (try it yourself), so it might not fire very
+well.  If you use this kind of specialisation, let us know how well it works.
+</para>
+
+      <para>Note: In earlier versions of GHC, it was possible to provide your own
       specialised function for a given type:
 
 <programlisting>