The programmer can specify rewrite rules as part of the source program (in a pragma). Here is an example:
{-# RULES
"map/map" forall f g xs. map f (map g xs) = map (f.g) xs
#-}
Use the debug flag -ddump-simpl-stats to see what rules fired.
If you need more information, then -ddump-rule-firings shows you
each individual rule firing in detail.
From a syntactic point of view:
There may be zero or more rules in a RULES pragma, separated by semicolons (which
may be generated by the layout rule).
The layout rule applies in a pragma. Currently no new indentation level is set, so if you put several rules in single RULES pragma and wish to use layout to separate them, you must lay out the starting in the same column as the enclosing definitions.
{-# RULES
"map/map" forall f g xs. map f (map g xs) = map (f.g) xs
"map/append" forall f xs ys. map f (xs ++ ys) = map f xs ++ map f ys
#-}
Furthermore, the closing #-}
should start in a column to the right of the opening {-#.
Each rule has a name, enclosed in double quotes. The name itself has no significance at all. It is only used when reporting how many times the rule fired.
A rule may optionally have a phase-control number (see Section 8.13.5.3, “Phase control”), immediately after the name of the rule. Thus:
{-# RULES
"map/map" [2] forall f g xs. map f (map g xs) = map (f.g) xs
#-}
The "[2]" means that the rule is active in Phase 2 and subsequent phases. The inverse notation "[~2]" is also accepted, meaning that the rule is active up to, but not including, Phase 2.
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 pattern variables. They are separated
by spaces, just like in a type forall.
A pattern variable may optionally have a type signature.
If the type of the pattern variable is polymorphic, it must have a type signature.
For example, here is the foldr/build rule:
"fold/build" forall k z (g::forall b. (a->b->b) -> b -> b) .
foldr k z (build g) = g k z
Since g has a polymorphic type, it must have a type signature.
The left hand side of a rule must consist of a top-level variable applied to arbitrary expressions. For example, this is not OK:
"wrong1" forall e1 e2. case True of { True -> e1; False -> e2 } = e1
"wrong2" forall f. f True = True
In "wrong1", the LHS is not an application; in "wrong2", the LHS has a pattern variable
in the head.
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.
All rules are implicitly exported from the module, and are therefore in force in any module that imports the module that defined the rule, directly or indirectly. (That is, if A imports B, which imports C, then C's rules are in force when compiling A.) The situation is very similar to that for instance declarations.
Inside a RULE "forall" is treated as a keyword, regardless of
any other flag settings. Furthermore, inside a RULE, the language extension
-XScopedTypeVariables is automatically enabled; see
Section 8.8.6, “Lexically scoped type variables
”.
Like other pragmas, RULE pragmas are always checked for scope errors, and
are typechecked. Typechecking means that the LHS and RHS of a rule are typechecked,
and must have the same type. However, rules are only enabled
if the -fenable-rewrite-rules flag is
on (see Section 8.14.2, “Semantics”).
From a semantic point of view:
Rules are enabled (that is, used during optimisation)
by the -fenable-rewrite-rules flag.
This flag is implied by -O, and may be switched
off (as usual) by -fno-enable-rewrite-rules.
(NB: enabling -fenable-rewrite-rules without -O
may not do what you expect, though, because without -O GHC
ignores all optimisation information in interface files;
see -fignore-interface-pragmas, Section 5.9.2, “-f*: platform-independent flags”.)
Note that -fenable-rewrite-rules is an optimisation flag, and
has no effect on parsing or typechecking.
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.
GHC makes absolutely no attempt to verify that the LHS and RHS of a rule have the same meaning. That is undecidable in general, and infeasible in most interesting cases. The responsibility is entirely the programmer's!
GHC makes no attempt to make sure that the rules are confluent or terminating. For example:
"loop" forall x y. f x y = f y x
This rule will cause the compiler to go into an infinite loop.
If more than one rule matches a call, GHC will choose one arbitrarily to apply.
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. The pattern (rule), but not the expression, is eta-expanded if necessary. (Eta-expanding the expression can lead to laziness bugs.) But not beta conversion (that's called higher-order matching).
Matching is carried out on GHC's intermediate language, which includes type abstractions and applications. So a rule only matches if the types match too. See Section 8.14.4, “Specialisation ” below.
GHC keeps trying to apply the rules as it optimises the program. For example, consider:
let s = map f
t = map g
in
s (t xs)
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.
Ordinary inlining happens at the same time as rule rewriting, which may lead to unexpected results. Consider this (artificial) example
f x = x
{-# RULES "f" f True = False #-}
g y = f y
h z = g True
Since f's right-hand side is small, it is inlined into g,
to give
g y = y
Now g is inlined into h, but f's RULE has
no chance to fire.
If instead GHC had first inlined g into h then there
would have been a better chance that f's RULE might fire.
The way to get predictable behaviour is to use a NOINLINE
pragma on f, to ensure
that it is not inlined until its RULEs have had a chance to fire.
The RULES mechanism is used to implement fusion (deforestation) of common list functions. If a "good consumer" consumes an intermediate list constructed by a "good producer", the intermediate list should be eliminated entirely.
The following are good producers:
List comprehensions
Enumerations of Int and Char (e.g. ['a'..'z']).
Explicit lists (e.g. [True, False])
The cons constructor (e.g 3:4:[])
++
map
take, filter
iterate, repeat
zip, zipWith
The following are good consumers:
List comprehensions
array (on its second argument)
++ (on its first argument)
foldr
map
take, filter
concat
unzip, unzip2, unzip3, unzip4
zip, zipWith (but on one argument only; if both are good producers, zip
will fuse with one but not the other)
partition
head
and, or, any, all
sequence_
msum
sortBy
So, for example, the following should generate no intermediate lists:
array (1,10) [(i,i*i) | i <- map (+ 1) [0..9]]
This list could readily be extended; if there are Prelude functions that you use a lot which are not included, please tell us.
If you want to write your own good consumers or producers, look at the Prelude definitions of the above functions to see how to do so.
Rewrite rules can be used to get the same effect as a feature present in earlier versions of GHC. For example, suppose that:
genericLookup :: Ord a => Table a b -> a -> b intLookup :: Table Int b -> Int -> b
where intLookup is an implementation of
genericLookup that works very fast for
keys of type Int. You might wish
to tell GHC to use intLookup instead of
genericLookup whenever the latter was called with
type Table Int b -> Int -> b.
It used to be possible to write
{-# SPECIALIZE genericLookup :: Table Int b -> Int -> b = intLookup #-}
This feature is no longer in GHC, but rewrite rules let you do the same thing:
{-# RULES "genericLookup/Int" genericLookup = intLookup #-}
This slightly odd-looking rule instructs GHC to replace
genericLookup by intLookup
whenever the types match.
What is more, this rule does not need to be in the same
file as genericLookup, unlike the
SPECIALIZE pragmas which currently do (so that they
have an original definition available to specialise).
It is Your Responsibility to make sure that
intLookup really behaves as a specialised version
of genericLookup!!!
An example in which using RULES for
specialisation will Win Big:
toDouble :: Real a => a -> Double
toDouble = fromRational . toRational
{-# RULES "toDouble/Int" toDouble = i2d #-}
i2d (I# i) = D# (int2Double# i) -- uses Glasgow prim-op directly
The i2d function is virtually one machine
instruction; the default conversion—via an intermediate
Rational—is obscenely expensive by
comparison.
Use -ddump-rules to see what transformation rules GHC is using.
Use -ddump-simpl-stats to see what rules are being fired.
If you add -dppr-debug you get a more detailed listing.
The definition of (say) build in GHC/Base.lhs looks like this:
build :: forall a. (forall b. (a -> b -> b) -> b -> b) -> [a]
{-# INLINE build #-}
build g = g (:) []
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.
In libraries/base/GHC/Base.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 GHC/List.lhs.
The external core format supports “Note” annotations;
the CORE pragma gives a way to specify what these
should be in your Haskell source code. Syntactically, core
annotations are attached to expressions and take a Haskell string
literal as an argument. The following function definition shows an
example:
f x = ({-# CORE "foo" #-} show) ({-# CORE "bar" #-} x)
Semantically, this is equivalent to:
g x = show x
However, when external core is generated (via
-fext-core), there will be Notes attached to the
expressions show and x.
The core function declaration for f is:
f :: %forall a . GHCziShow.ZCTShow a ->
a -> GHCziBase.ZMZN GHCziBase.Char =
\ @ a (zddShow::GHCziShow.ZCTShow a) (eta::a) ->
(%note "foo"
%case zddShow %of (tpl::GHCziShow.ZCTShow a)
{GHCziShow.ZCDShow
(tpl1::GHCziBase.Int ->
a ->
GHCziBase.ZMZN GHCziBase.Char -> GHCziBase.ZMZN GHCziBase.Cha
r)
(tpl2::a -> GHCziBase.ZMZN GHCziBase.Char)
(tpl3::GHCziBase.ZMZN a ->
GHCziBase.ZMZN GHCziBase.Char -> GHCziBase.ZMZN GHCziBase.Cha
r) ->
tpl2})
(%note "bar"
eta);
Here, we can see that the function show (which
has been expanded out to a case expression over the Show dictionary)
has a %note attached to it, as does the
expression eta (which used to be called
x).