[project @ 1999-07-14 11:33:10 by simonmar]
[ghc-hetmet.git] / ghc / docs / users_guide / glasgow_exts.vsgml
index 4c0fd15..284dd9c 100644 (file)
@@ -1,5 +1,5 @@
 % 
-% $Id: glasgow_exts.vsgml,v 1.3 1998/12/02 13:20:38 simonm Exp $
+% $Id: glasgow_exts.vsgml,v 1.12 1999/07/14 11:33:10 simonmar Exp $
 %
 % GHC Language Extensions.
 %
@@ -36,7 +36,7 @@ classes" id="multi-param-type-classes">.
 
 <tag>Local universal quantification:</tag>
 
-GHC's type system supports explicit unversal quantification in
+GHC's type system supports explicit universal quantification in
 constructor fields and function arguments.  This is useful for things
 like defining @runST@ from the state-thread world.  See Section <ref
 name="Local universal quantification" id="universal-quantification">.
@@ -47,12 +47,32 @@ Some or all of the type variables in a datatype declaration may be
 <em>existentially quantified</em>.  More details in Section <ref
 name="Existential Quantification" id="existential-quantification">.
 
+<tag>Scoped type variables:</tag>
+
+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 Section <ref name="Scoped Type Variables"
+id="scoped-type-variables">.
+
 <tag>Calling out to C:</tag> 
 
 Just what it sounds like.  We provide <em>lots</em> of rope that you
 can dangle around your neck.  Please see Section <ref name="Calling~C
 directly from Haskell" id="glasgow-ccalls">.
 
+<tag>Pragmas</tag>
+
+Pragmas are special instructions to the compiler placed in the source
+file.  The pragmas GHC supports are described in Section <ref
+name="Pragmas" id="pragmas">.
+
+<tag>Rewrite rules:</tag>
+
+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 Section <ref name="Rewrite Rules"
+id="rewrite-rules">.
+
 </descrip>
 
 Before you get too carried away working at the lowest level (e.g.,
@@ -221,13 +241,16 @@ may be just the ticket (NB: <em>no chance</em> of such code going
 through a native-code generator):
 
 <tscreen><verb>
+import Addr
+import CString
+
 oldGetEnv name
-  = _casm_ ``%r = getenv((char *) %0);'' name >>= \ litstring@(A# str#) ->
+  = _casm_ ``%r = getenv((char *) %0);'' name >>= \ litstring ->
     return (
-        if (litstring == ``NULL'') then
+        if (litstring == nullAddr) then
             Left ("Fail:oldGetEnv:"++name)
         else
-            Right (unpackCString# str#)
+            Right (unpackCString litstring)
     )
 </verb></tscreen>
 
@@ -260,6 +283,35 @@ inlining of C code (GHC - A Better C Compiler :-), the option
 
 %************************************************************************
 %*                                                                      *
+<sect2>Literal-literals
+<label id="glasgow-literal-literals">
+<p>
+<nidx>Literal-literals</nidx>
+%*                                                                      *
+%************************************************************************
+
+The literal-literal argument to @_casm_@ can be made use of separately
+from the @_casm_@ construct itself. Indeed, we've already used it:
+
+<tscreen><verb>
+fooH :: Char -> Int -> Double -> Word -> IO Double
+fooH c i d w = _ccall_ fooC (``stdin''::Addr) c i d w
+</verb></tscreen>
+
+The first argument that's passed to @fooC@ is given as a literal-literal, 
+that is, a literal chunk of C code that will be inserted into the generated
+@.hc@ code at the right place.
+
+A literal-literal is restricted to having a type that's an instance of
+the @CCallable@ class, see <ref name="CCallable" id="ccall-gotchas">
+for more information.
+
+Notice that literal-literals are by their very nature unfriendly to
+native code generators, so exercise judgement about whether or not to
+make use of them in your code.
+
+%************************************************************************
+%*                                                                      *
 <sect2>Using function headers
 <label id="glasgow-foreign-headers">
 <p>
@@ -421,7 +473,7 @@ performGC :: IO ()
 </verb></tscreen>
 
 More information on the programmers' interface to @ForeignObj@ can be
-found in Section <ref name="Foreign objects" id="sec:foreign-obj">.
+found in the library documentation.
 
 %************************************************************************
 %*                                                                      *
@@ -508,6 +560,8 @@ useful in debugging code.)
 <label id="ccall-gotchas">
 <p>
 <nidx>C call dangers</nidx>
+<nidx>CCallable</nidx>
+<nidx>CReturnable</nidx>
 %*                                                                      *
 %************************************************************************
 
@@ -1154,6 +1208,26 @@ and <tt>bind</tt> to extract the polymorphic bind and return functions
 from the <tt>MonadT</tt> data structure, rather than using pattern
 matching.
 
+You cannot pattern-match against an argument that is polymorphic.
+For example:
+<tscreen><verb>
+       newtype TIM s a = TIM (ST s (Maybe a))
+
+       runTIM :: (forall s. TIM s a) -> Maybe a
+       runTIM (TIM m) = runST m
+</verb></tscreen>
+
+Here the pattern-match fails, because you can't pattern-match against
+an argument of type <tt>(forall s. TIM s a)</tt>.  Instead you 
+must bind the variable and pattern match in the right hand side:
+<tscreen><verb>
+       runTIM :: (forall s. TIM s a) -> Maybe a
+       runTIM tm = case tm of { TIM m -> runST m }
+</verb></tscreen>
+The <tt>tm</tt> on the right hand side is (invisibly) instantiated, like
+any polymorphic value at its occurrence site, and now you can pattern-match
+against it.
+
 <sect2>The partial-application restriction
 <p>
 
@@ -1443,3 +1517,630 @@ but single-field existentially quantified constructors aren't much
 use.  So the simple restriction (no existential stuff on <tt>newtype</tt>)
 stands, unless there are convincing reasons to change it.
 </itemize>
+
+
+<sect1> <idx/Assertions/ 
+<label id="sec:assertions">
+<p>
+
+If you want to make use of assertions in your standard Haskell code, you
+could define a function like the following:
+
+<tscreen><verb>
+assert :: Bool -> a -> a
+assert False x = error "assertion failed!"
+assert _     x = x
+</verb></tscreen>
+
+which works, but gives you back a less than useful error message --
+an assertion failed, but which and where?
+
+One way out is to define an extended <tt/assert/ 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 <tt/assert/ was used.
+
+Ghc offers a helping hand here, doing all of this for you. For every
+use of <tt/assert/ in the user's source:
+
+<tscreen><verb>
+kelvinToC :: Double -> Double
+kelvinToC k = assert (k &gt;= 0.0) (k+273.15)
+</verb></tscreen>
+
+Ghc will rewrite this to also include the source location where the
+assertion was made, 
+
+<tscreen><verb>
+assert pred val ==> assertError "Main.hs|15" pred val
+</verb></tscreen>
+
+The rewrite is only performed by the compiler when it spots
+applications of <tt>Exception.assert</tt>, so you can still define and
+use your own versions of <tt/assert/, should you so wish. If not,
+import <tt/Exception/ to make use <tt/assert/ in your code.
+
+To have the compiler ignore uses of assert, use the compiler option
+@-fignore-asserts@. <nidx>-fignore-asserts option</nidx> That is,
+expressions of the form @assert pred e@ will be rewritten to @e@.
+
+Assertion failures can be caught, see the documentation for the
+Hugs/GHC Exception library for information of how.
+
+% -----------------------------------------------------------------------------
+<sect1>Scoped Type Variables
+<label id="scoped-type-variables">
+<p>
+
+A <em/pattern type signature/ can introduce a <em/scoped type
+variable/.  For example
+
+<tscreen><verb>
+f (xs::[a]) = ys ++ ys
+          where
+             ys :: [a]
+             ys = reverse xs 
+</verb></tscreen>
+
+The pattern @(xs::[a])@ includes a type signature for @xs@.
+This brings the type variable @a@ into scope; it scopes over
+all the patterns and right hand sides for this equation for @f@.
+In particular, it is in scope at the type signature for @y@.
+
+At ordinary type signatures, such as that for @ys@, any type variables
+mentioned in the type signature <em/that are not in scope/ are
+implicitly universally quantified.  (If there are no type variables in
+scope, all type variables mentioned in the signature are universally
+quantified, which is just as in Haskell 98.)  In this case, since @a@
+is in scope, it is not universally quantified, so the type of @ys@ is
+the same as that of @xs@.  In Haskell 98 it is not possible to declare
+a type for @ys@; a major benefit of scoped type variables is that
+it becomes possible to do so.
+
+Scoped type variables are implemented in both GHC and Hugs.  Where the
+implementations differ from the specification below, those differences
+are noted.
+
+So much for the basic idea.  Here are the details.
+
+<sect2>Scope and implicit quantification
+<p>
+
+<itemize>
+<item> 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 <em/type variables bound by the equation/.
+
+<item> The type variables thus brought into scope may be mentioned
+in ordinary type signatures or pattern type signatures anywhere within
+their scope.
+
+<item> In ordinary type signatures, any type variable mentioned in the
+signature that is in scope is <em/not/ universally quantified.
+
+<item> Ordinary type signatures do not bring any new type variables
+into scope (except in the type signature itself!). So this is illegal:
+
+<tscreen><verb>
+  f :: a -> a
+  f x = x::a
+</verb></tscreen>
+
+It's illegal because @a@ is not in scope in the body of @f@,
+so the ordinary signature @x::a@ is equivalent to @x::forall a.a@;
+and that is an incorrect typing.
+
+<item> There is no implicit universal quantification on pattern type
+signatures, nor may one write an explicit @forall@ type in a pattern
+type signature.  The pattern type signature is a monotype.
+
+<item> 
+The type variables in the head of a @class@ or @instance@ declaration
+scope over the methods defined in the @where@ part.  For example:
+
+<tscreen><verb>
+  class C a where
+    op :: [a] -> a
+
+    op xs = let ys::[a]
+               ys = reverse xs
+           in
+           head ys
+</verb></tscreen>
+
+(Not implemented in Hugs yet, Dec 98).
+</itemize>
+
+<sect2>Polymorphism
+<p>
+
+<itemize>
+<item> 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.
+
+<tscreen><verb>
+   f :: [a] -> [a]
+   f (xs::[b]) = reverse xs
+</verb></tscreen>
+
+<item> The function must be polymorphic in the type variables
+bound by all its equations.  Operationally, the type variables bound
+by one equation must not:
+
+<itemize>
+<item> Be unified with a type (such as @Int@, or @[a]@).
+<item> Be unified with a type variable free in the environment.
+<item> Be unified with each other.  (They may unify with the type variables 
+bound by another equation for the same function, of course.)
+</itemize>
+
+For example, the following all fail to type check:
+
+<tscreen><verb>
+  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]
+</verb></tscreen>
+
+<item> The pattern-bound type variable may, however, be constrained
+by the context of the principal type, thus:
+
+<tscreen><verb>
+  f (x::a) (y::a) = x+y*2
+</verb></tscreen>
+
+gets the inferred type: @forall a. Num a => a -> a -> a@.
+</itemize>
+
+<sect2>Result type signatures
+<p>
+
+<itemize>
+<item> The result type of a function can be given a signature,
+thus:
+
+<tscreen><verb>
+  f (x::a) :: [a] = [x,x,x]
+</verb></tscreen>
+
+The final @":: [a]"@ after all the patterns gives a signature to the
+result type.  Sometimes this is the only way of naming the type variable
+you want:
+
+<tscreen><verb>
+  f :: Int -> [a] -> [a]
+  f n :: ([a] -> [a]) = let g (x::a, y::a) = (y,x)
+                       in \xs -> map g (reverse xs `zip` xs)
+</verb></tscreen>
+
+</itemize>
+
+Result type signatures are not yet implemented in Hugs.
+
+<sect2>Pattern signatures on other constructs
+<p>
+
+<itemize>
+<item> A pattern type signature can be on an arbitrary sub-pattern, not
+just on a variable:
+
+<tscreen><verb>
+  f ((x,y)::(a,b)) = (y,x) :: (b,a)
+</verb></tscreen>
+
+<item> Pattern type signatures, including the result part, can be used
+in lambda abstractions:
+
+<tscreen><verb>
+  (\ (x::a, y) :: a -> x)
+</verb></tscreen>
+
+Type variables bound by these patterns must be polymorphic in
+the sense defined above.
+For example:
+
+<tscreen><verb>
+  f1 (x::c) = f1 x     -- ok
+  f2 = \(x::c) -> f2 x -- not ok
+</verb></tscreen>
+
+Here, @f1@ is OK, but @f2@ is not, because @c@ gets unified
+with a type variable free in the environment, in this
+case, the type of @f2@, which is in the environment when
+the lambda abstraction is checked.
+
+<item> Pattern type signatures, including the result part, can be used
+in @case@ expressions:
+
+<tscreen><verb>
+  case e of { (x::a, y) :: a -> x } 
+</verb></tscreen>
+
+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:
+
+<tscreen><verb>
+  case (True,False) of { (x::a, y) -> x }
+</verb></tscreen>
+
+Even though the context is that of a pair of booleans, 
+the alternative itself is polymorphic.  Of course, it is
+also OK to say:
+
+<tscreen><verb>
+  case (True,False) of { (x::Bool, y) -> x }
+</verb></tscreen>
+
+<item>
+To avoid ambiguity, the type after the ``@::@'' in a result
+pattern signature on a lambda or @case@ must be atomic (i.e. a single
+token or a parenthesised type of some sort).  To see why, 
+consider how one would parse this:
+
+<tscreen><verb>
+  \ x :: a -> b -> x
+</verb></tscreen>
+
+<item> Pattern type signatures that bind new type variables
+may not be used in pattern bindings at all.
+So this is illegal:
+
+<tscreen><verb>
+  f x = let (y, z::a) = x in ...
+</verb></tscreen>
+
+But these are OK, because they do not bind fresh type variables:
+
+<tscreen><verb>
+  f1 x            = let (y, z::Int) = x in ...
+  f2 (x::(Int,a)) = let (y, z::a)   = x in ...
+</verb></tscreen>
+
+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:
+
+<tscreen><verb>
+  f :: (b->b) = \(x::b) -> x
+</verb></tscreen>
+
+</itemize>
+Such degnerate function bindings do not fall under the monomorphism
+restriction.  Thus:
+
+<tscreen><verb>
+  g :: a -> a -> Bool = \x y. x==y
+</verb></tscreen>
+
+Here @g@ has type @forall a. Eq a => a -> a -> Bool@, just as if
+@g@ had a separate type signature.  Lacking a type signature, @g@
+would get a monomorphic type.
+
+<sect2>Existentials
+<p>
+
+<itemize>
+<item> Pattern type signatures can bind existential type variables.
+For example:
+
+<tscreen><verb>
+  data T = forall a. MkT [a]
+
+  f :: T -> T
+  f (MkT [t::a]) = MkT t3
+                where
+                  t3::[a] = [t,t,t]
+</verb></tscreen>
+
+</itemize>
+
+%-----------------------------------------------------------------------------
+<sect1>Pragmas
+<label id="pragmas">
+<p>
+
+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.
+
+<sect2>INLINE pragma
+<label id="inline-pragma">
+<nidx>INLINE pragma</nidx>
+<nidx>pragma, INLINE</nidx>
+<p>
+
+GHC (with @-O@, as always) tries to inline (or ``unfold'')
+functions/values that are ``small enough,'' thus avoiding the call
+overhead and possibly exposing other more-wonderful optimisations.
+
+You will probably see these unfoldings (in Core syntax) in your
+interface files.
+
+Normally, if GHC decides a function is ``too expensive'' to inline, it
+will not do so, nor will it export that unfolding for other modules to
+use.
+
+The sledgehammer you can bring to bear is the
+@INLINE@<nidx>INLINE pragma</nidx> pragma, used thusly:
+<tscreen><verb>
+key_function :: Int -> String -> (Bool, Double) 
+
+#ifdef __GLASGOW_HASKELL__
+{-# INLINE key_function #-}
+#endif
+</verb></tscreen>
+(You don't need to do the C pre-processor carry-on unless you're going
+to stick the code through HBC---it doesn't like @INLINE@ pragmas.)
+
+The major effect of an @INLINE@ pragma is to declare a function's
+``cost'' to be very low.  The normal unfolding machinery will then be
+very keen to inline it.
+
+An @INLINE@ pragma for a function can be put anywhere its type
+signature could be put.
+
+@INLINE@ pragmas are a particularly good idea for the
+@then@/@return@ (or @bind@/@unit@) functions in a monad.
+For example, in GHC's own @UniqueSupply@ monad code, we have:
+<tscreen><verb>
+#ifdef __GLASGOW_HASKELL__
+{-# INLINE thenUs #-}
+{-# INLINE returnUs #-}
+#endif
+</verb></tscreen>
+
+<sect2>NOINLINE pragma
+<label id="noinline-pragma">
+<p>
+<nidx>NOINLINE pragma</nidx>
+<nidx>pragma, NOINLINE</nidx>
+
+The @NOINLINE@ 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.
+
+<sect2>SPECIALIZE pragma
+<label id="specialize-pragma">
+<p>
+<nidx>SPECIALIZE pragma</nidx>
+<nidx>pragma, SPECIALIZE</nidx>
+<nidx>overloading, death to</nidx>
+
+(UK spelling also accepted.)  For key overloaded functions, you can
+create extra versions (NB: more code space) specialised to particular
+types.  Thus, if you have an overloaded function:
+
+<tscreen><verb>
+hammeredLookup :: Ord key => [(key, value)] -> key -> value
+</verb></tscreen>
+
+If it is heavily used on lists with @Widget@ keys, you could
+specialise it as follows:
+<tscreen><verb>
+{-# SPECIALIZE hammeredLookup :: [(Widget, value)] -> Widget -> value #-}
+</verb></tscreen>
+
+To get very fancy, you can also specify a named function to use for
+the specialised value, by adding @= blah@, as in:
+<tscreen><verb>
+{-# SPECIALIZE hammeredLookup :: ...as before... = blah #-}
+</verb></tscreen>
+It's <em>Your Responsibility</em> to make sure that @blah@ really
+behaves as a specialised version of @hammeredLookup@!!!
+
+NOTE: the @=blah@ feature isn't implemented in GHC 4.xx.
+
+An example in which the @= blah@ form will Win Big:
+<tscreen><verb>
+toDouble :: Real a => a -> Double
+toDouble = fromRational . toRational
+
+{-# SPECIALIZE toDouble :: Int -> Double = i2d #-}
+i2d (I# i) = D# (int2Double# i) -- uses Glasgow prim-op directly
+</verb></tscreen>
+The @i2d@ function is virtually one machine instruction; the
+default conversion---via an intermediate @Rational@---is obscenely
+expensive by comparison.
+
+By using the US spelling, your @SPECIALIZE@ pragma will work with
+HBC, too.  Note that HBC doesn't support the @= blah@ form.
+
+A @SPECIALIZE@ pragma for a function can be put anywhere its type
+signature could be put.
+
+<sect2>SPECIALIZE instance pragma
+<label id="specialize-instance-pragma">
+<p>
+<nidx>SPECIALIZE pragma</nidx>
+<nidx>overloading, death to</nidx>
+Same idea, except for instance declarations.  For example:
+<tscreen><verb>
+instance (Eq a) => Eq (Foo a) where { ... usual stuff ... }
+
+{-# SPECIALIZE instance Eq (Foo [(Int, Bar)] #-}
+</verb></tscreen>
+Compatible with HBC, by the way.
+
+<sect2>LINE pragma
+<label id="line-pragma">
+<p>
+<nidx>LINE pragma</nidx>
+<nidx>pragma, LINE</nidx>
+
+This pragma is similar to C's @#line@ pragma, and is mainly for use in
+automatically generated Haskell code.  It lets you specify the line
+number and filename of the original code; for example
+
+<tscreen><verb>
+{-# LINE 42 "Foo.vhs" #-}
+</verb></tscreen>
+
+if you'd generated the current file from something called @Foo.vhs@
+and this line corresponds to line 42 in the original.  GHC will adjust
+its error messages to refer to the line/file named in the @LINE@
+pragma.
+
+<sect2>RULES pragma
+<p>
+The RULES pragma lets you specify rewrite rules.  It is described in
+Section <ref name="Rewrite Rules"
+id="rewrite-rules">.
+
+%-----------------------------------------------------------------------------
+<sect1>Rewrite rules
+<label id="rewrite-rules">
+<nidx>RULES pagma</nidx>
+<nidx>pragma, RULES</nidx>
+<nidx>rewrite rules</nidx>
+<p>
+
+The programmer can specify rewrite rules as part of the source program
+(in a pragma).  GHC applies these rewrite rules wherever it can.
+
+Here is an example:
+<tscreen><verb>
+  {-# RULES
+       "map/map"       forall f,g,xs. map f (map g) xs = map (f.g) xs
+  #-}
+</verb></tscreen>
+
+<sect2>Syntax
+<p>
+
+From a syntactic point of view:
+<itemize>
+<item> Each rule has a name, enclosed in double quotes.
+<item> There may be zero or more rules in a @RULES@ pragma.
+<item> Layout applies in a @RULES@ pragma.  Currently no new indentation level
+is set, so you must lay out your rules starting in the same column as the
+enclosing definitions.
+<item> Each variable mentioned in a rule must either be in scope (e.g. @map@),
+or bound by the @forall@ (e.g. @f@, @g@, @xs@).  The variables bound by
+the @forall@ are called the <em>pattern</em> variables.
+<item> A pattern variable may optionally have a type signature.
+If its type is polymorphic, it <em>must</em> have a type signature.
+For example, here is the @foldr/build@ rule:
+<tscreen><verb>
+  "fold/build"         forall k,z,g::forall b. (a->b->b) -> b -> b . 
+               foldr k z (build g) = g k z
+</verb></tscreen>
+
+
+<item> The left hand side of a rule must consist of a top-level variable applied
+to arbitrary expressions.  For example, this is <em>not</em> OK:
+<tscreen><verb>
+  "wrong1"   forall e1,e2.  case True of { True -> e1; False -> e2 } = e1
+  "wrong2"   forall f.      f True = True
+</verb></tscreen>
+In @"wrong1"@, the LHS is not an application; in @"wrong1"@, the LHS has a pattern variable
+in the head.
+<item> A rule does not need to be in the same module as (any of) the
+variables it mentions, though of course they need to be in scope.
+<item> Rules are automatically exported from a module, just as instance declarations are.
+</itemize>
+
+<sect2>Semantics
+<p>
+
+From a semantic point of view:
+<itemize>
+<item> Rules are only applied if you use the @-O@ flag.
+
+<item> Rules are regarded as left-to-right rewrite rules.  
+When GHC finds an expression that is a substitution instance of the LHS
+of a rule, it replaces the expression by the (appropriately-substituted) RHS.
+By "a substitution instance" we mean that the LHS can be made equal to the 
+expression by substituting for the pattern variables.
+
+<item> The LHS and RHS of a rule are typechecked, and must have the
+same type.
+
+<item> GHC makes absolutely no attempt to verify that the LHS and RHS
+of a rule have the same meaning.  That is undecideable in general, and
+infeasible in most interesting cases.  The responsibility is entirely the programmer's!
+
+<item> GHC makes no attempt to make sure that the rules are confluent or
+terminating.  For example:
+<tscreen><verb>
+  "loop"       forall x,y.  f x y = f y x
+</verb></tscreen>
+This rule will cause the compiler to go into an infinite loop.
+
+<item> GHC currently uses a very simple, syntactic, matching algorithm
+for matching a rule LHS with an expression.  It seeks a substitution
+which makes the LHS and expression syntactically equal modulo: alpha
+conversion, and (I think) eta conversion.  But not beta conversion (that's
+called higher-order matching).
+
+<item> GHC keeps trying to apply the rules as it optimises the program.
+For example, consider:
+<tscreen><verb>
+  let s = map f
+      t = map g
+  in
+  s (t xs)
+</verb></tscreen>
+The expression @s (t xs)@ does not match the rule @"map/map"@, but GHC
+will substitute for @s@ and @t@, giving an expression which does match.
+If @s@ or @t@ was (a) used more than once, and (b) large or a redex, then it would
+not be substituted, and the rule would not fire.
+
+<item> In the earlier phases of compilation, GHC inlines <em>nothing
+that appears on the LHS of a rule</em>, because once you have substituted
+for something you can't match against it (given the simple minded 
+matching).  So if you write the rule
+<tscreen><verb>
+       "map/map"       forall f,g.  map f . map g = map (f.g)
+</verb></tscreen>
+this <em>won't</em> match the expression @map f (map g xs)@.
+It will only match something written with explicit use of ".".  
+Well, not quite.  It <em>will</em> match the expression
+<tscreen><verb>
+       wibble f g xs
+</verb></tscreen>
+where @wibble@ is defined:
+<tscreen><verb>
+       wibble f g = map f . map g 
+</verb></tscreen>
+because @wibble@ will be inlined (it's small).
+
+Later on in compilation, GHC starts inlining even things on the
+LHS of rules, but still leaves the rules enabled.  This inlining
+policy is controlled by the per-simplification-pass flag @-finline-phase@n.
+</itemize>
+
+
+<sect2>Controlling what's going on
+<p>
+
+<itemize>
+<item> Use @-fddump-rules@ to see what transformation rules GHC is using.
+<item> Use @-fddump-simpl-stats@ to see what rules are being fired.
+<item> The defintion of (say) @build@ in @PrelBase.lhs@ looks llike this:
+<tscreen><verb>
+       build   :: forall a. (forall b. (a -> b -> b) -> b -> b) -> [a]
+       {-# INLINE build #-}
+       build g = g (:) []
+</verb></tscreen>
+Notice the @INLINE@!  That prevents @(:)@ from being inlined when compiling
+@PrelBase@, so that an importing module will ``see'' the @(:)@, and can
+match it on the LHS of a rule.  @INLINE@ prevents any inlining happening
+in the RHS of the @INLINE@ thing.  I regret the delicacy of this.
+
+<item> In @ghc/lib/std/PrelBase.lhs@ look at the rules for @map@ to
+see how to write rules that will do fusion and yet give an efficient
+program even if fusion doesn't happen.  More rules in @PrelList.lhs@.
+</itemize>