Proposal: Template Patterns in Rewrite Rules

#1

This proposal is discussed at pull request #555:

This is a GHC proposal augmenting our existing rewrite rule mechanism with lightweight higher order matching using template patterns, which provides a way to match complex terms which contain locally bound variables.

For example, consider the rule:

"concatMap"   forall next f.   
    concatMap (\x -> Stream next (f x)) = concatMap' next f

Previously the f x part (which we call template pattern) only matched applications literally, like:

concatMap (\x -> Stream next ((\y -> y * 2 + y) x)

This proposal allows it to match the beta-equivalent expression:

concatMap (\x -> Stream next (x * 2 + x))

Which results in:

concatMap' next (\x -> x * 2 + x)

Rendered

Please leave a comment if you can think of other real world applications of template patterns.

I would also appreciate suggestions for a better name than “template patterns”.

#2

“Rewrite pattern”…?

#3

Thanks for the suggestion. The main problem I see is that “pattern” doesn’t exactly make clear what it is we are referring to. The names “template pattern” and “rewrite pattern” are not much different in that respect in my opinion.

To be precise, take for example this rule:

{-# RULES "wombat"  forall f x.  foo x (\y. f y) = bar x f  #-}

The GHC source code uses this vocabulary:

  • Template. The LHS of a rule is called its template, so forall f x. foo x (\y. f y) in the rule “wombat”.
  • Template variables. The forall'd variables are called the template variables. In rule “wombat”, f and x 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. The rule matcher matches the LHS of the rule (the template) against an expression in the program (the target).

Confusingly the GHC user guide uses the term “pattern variable” instead of “template variable”.

The thing we want to give a name to is the subexpression f y in the template of the “wombat” rule. This is an application of the template variable f to the local binder x. In general we want this name to refer to any subexpression that is an application of a template variable to one or more local binders.

#4

A curious choice, considering the advent of Template Haskell - are they (somehow) related?

Alright, so “pattern” is considered vague (or overused) - from a quick synonym search: guide, recogniser…