Higher order template application matching for rewrite rules
This ticket is the subject of GHC Proposal #555.
Motivation
concatMap
The problem of optimising concatMap
under stream fusion has been an open problem for a very long time (see e.g. #915 (comment 26104)).
It's an important one too: in their paper "The Hermit in the stream", Farmer et al describe an entire plugin for GHC devoted to this one task. Here's part of the abstract
-
Stream Fusion, a popular deforestation technique in the Haskell community, cannot fuse the
concatMap
combinator. This is a serious limitation, asconcatMa
p represents computations on nested streams. The original implementation of Stream Fusion used the Glasgow Haskell Compiler's user-directed rewriting system. A transformation which allows the compiler to fuse many uses of concatMap has previously been proposed, but never implemented, because the host rewrite system was not expressive enough to implement the proposed transformation.In this paper, we develop a custom optimization plugin which implements the proposed
concatMap
transformation, and study the effectiveness of the transformation in practice. We also provide a new translation scheme for list comprehensions which enables them to be optimized. Within this framework, we extend the transformation to monadic streams. Code featuring uses ofconcatMap
experiences significant speedup when compiled with this optimization. This allows Stream Fusion to outperform its rival, foldr/build, on many list computations, and enables performance-sensitive code to be expressed at a higher level of abstraction.
See also
- The earlier paper From lists to streams to nothing at all.
- #915 (closed)
@dcoutts proposed using the following rewrite rule in "Stream Fusion: Practical shortcut fusion for coinductive sequence types" (Section 4.8.3):
"concatMap" forall next f. concatMap (\x -> Stream next (f x)) = concatMap' next f
Unfortunately, this rule only matches if the left hand side contains a literal application of some function f
to the local variable x
. This precludes cases like concatMap (\x. Stream next (x*2 +x))
.
A higher order matching algorithm could recover the substitution [f :-> (\p. p*2 +p)]
, but higher order unification is tricky to implement. De Moor and Sittampalam use the example pattern forall f x. f x
matched to the expression 0
. This matching has an infinite number of possible results like:
-
[f :-> (\p -> p), x :-> 0]
, -
[f :-> (\_ -> 0)]
, -
[f :-> (\g -> g 0), x :-> (\p -> p)]
, - etc.
In their paper "Higher-order matching for program transformation", De Moor and Sittampalam provide an algorithm for a restricted form of higher order matching, but it seems that still would require significant changes to the rule matcher in GHC.
Recently in #22361 (comment 460918) @simonpj also noted that the foldr/build
fusion mechanism could benefit from such higher order matching with the example:
"mapList" [1] forall f. foldr (\x r -> (:) (f x) r) [] = map f
Proposal
I propose to implement an even more limited form of higher order matching based on template applications. Template applications are inspired by the pattern restriction described by Miller in "Unification Under a Mixed Prefix" (thanks @sgraf812 for the reference to this related work). Here is a precise specfication.
Start with terminology. Consider the rule
{-# RULES "wombat" forall f x. foo x (\y. f y) = bar x f #-}
- Template. The LHS of a rule is called its template.
-
Template variables. The
forall
'd variables are called the template variables. In rule "wombat",f
andx
are template variables. -
Local binders. The local binders of a rule are the variables bound inside the template. Example:
y
is a local binder of rule "wombat". - Target and substitution. The rule matcher matches the LHS of the rule (the template) against an expression in the program (the target).
- Substitution. A sucessful match finds a substitution S: a binding for each template variable, such that applying S to the LHS yields the target.
- After a successful match we replace the target expression with the substitution S applied to the RHS of the rule.
In GHC today, a template variable v
matches any expression e
if
-
e
has the same type asv
- No local binder of the template is free in
e
.
The change proposed here is that a template application matches any expression (of the same type):
-
Template application. A template application is an expression of form
f x y z
where:-
f
is a template variable -
x
,y
,z
are locally bound in the template (likey
in rule "wombat" above). They are specifically not template variables, nor are they free in the entire rule. - The arguments
x
,y
,z
are distinct variables -
x
,y
,z
can be term variables or type variables.
-
-
A template application
f x y z
matches any expressione
provided:- The target has the same type as the template
- no local binder is free in
e
, other thanx
,y
,z
.
-
If these two condition hold, the template application
f x y z
matches the target expressione
, yielding the substitution[f :-> \x y z. e]
. Notice that this substitution is type preserving, and the RHS of the substitution has no free local binders.
Example
Consider the rule "mapList" above, with target expression
foldr (\x r -> (:) (p (q (x+2))) r) []
With the new matching semantics, matching rule "mapList" aginst this target would succeed, with substitution [f :-> (\x. p (q (x+2)))]
. So the target would be reweritten to
foldr (\x r -> (:) (p (q (x+2))) r) []
===>
map (\x. p (q (x+2)))
The concatMap
rule would work similarly. So, although this proposal is very restricted, it is sufficient to solve practical problems.
Uniqueness of matching
Consider this rule and target:
RULE "funny" foo (\x y. Just (f x y))
Target: ...(foo (\ p q. Just (h (p+1) q)))....
Then during matching we will encounter:
Template: f x y
Target: h (p+1) q [p:->x, q:->y]
The renaming [p:->x, q:->y]
is done by the matcher (today) on the fly, to make the bound variables of the template and target "line up".
Now, we can
- Either use the new template-application rule to succeed with
[f :-> \x y. h (x+1) y]
. - Or use the existing decompose-application rule to match
(f x)
against(h (p+1))
andy
againstq
. This will succeed, with[f :-> \x. h (x+1)]
.
Critically, it doesn't matter which we do. We get the same result either way. That's encouraging.
However if the example had been like this:
Target: ...(foo (\ p q. Just (h (p+q) q))).... -- Note (p+q) instead of (p+1)
Now, if we use the existing decompose-application rule, we'll end up matching (h x)
against h (p+q)
, and that will fail because we'll end up trying to match [f :-> \x. h (x+y)]
, which doesn't work because y
is free.
Conclusion: the new template-application rule should take priority, because if you don't use it, you may not be able use it on a sub-expression.
Separately, I also think that if a match exists it is unique (moudulo eta-reduction). It'd be good to prove this, because ambiguity is the bug-bear of more general higher order matching.
Related work
There are two notable streams of research: matching and unification. Both problems are about finding a substitution such that two expressions containing variables become equal. The difference is that unification applies to two expressions that both can contain (unification) variables, while matching applies to one expression with (template) variables and one concrete expression. Matching is an easier problem to solve.
The main related work on matching is "Higher-order matching for program transformation" by De Moor and Sittampalam. This work identifies a subset of the higher order matching problem which is decidable and always has a finite set of possible substitutions. This subset is strictly larger than the subset of template applications which we consider in this proposal. For example, their subset is able to find substitutions to match forall f x. f x
to 0
. Our proposal does not support this form of higher order matching.
Existing work on higher order unification has revealed that higher order unification of the template application form is a useful decidable subset of the general problem. This was first observed by Miller in "Unification Under a Mixed Prefix". Miller called these template applications 'patterns', but we decided against using that terminology because of the confusion with regular pattern matching in Haskell. Nowadays higher unification with Miller's pattern restriction is commonplace in dependently typed languages such as Agda and Idris, which shows that higher order unification with this restriction is still very powerful.
One notable extension of Miller's patterns is the extension by Duggan in his paper "Unification with extended patterns". Duggan extends the simple template application form to allow projections of local binders as arguments to the template variables. Such an extension might also be applicable to the template application form in this proposal.