[ghc-steering-committee] #555: Higher Order Patterns in Rewrite Rules, rec accept

[Adam Gundry]

This is a very well-written proposal. I support acceptance.


On 19/01/2023 15:31, Arnaud Spiwack wrote:
> I've got a question though: is the following rewrite rule something I 
> can write in Haskell today?
> 
> ```
> {- RULES … forall f g. map (\x -> f (g x)) = map f . map g
> ```
> 
> In this rule `f (g x)` is not a pattern (because `g` is not rigid). And 
> it is not clear to me how purely syntactic unification and pattern 
> unification interact.

I believe you can write this today, but the template `f (g x)` will 
match only a target with an explicit application where the argument is 
itself an explicit application (e.g. `e1 (e2 x)`).

Under the proposal, `f (g x)` is not in the pattern fragment so it will 
match only an explicit application, but `g x` is a pattern so the 
argument is allowed to be more general, e.g. the template `f (g x)` will 
match `e1 x` or `e1 (e2 x 42 x)`.

At least, this is how I understood the proposal, but I may have 
misinterpreted. The specification could be slightly clearer about how 
this works (in particular the "Ambiguity breaking" point). I've 
commented to that effect on the PR.

Adam


> On Thu, 19 Jan 2023 at 15:51, Chris Dornan <chris at chrisdornan.com 
> <mailto:chris at chrisdornan.com>> wrote:
> 
>     I am sorry for not getting back sooner Joachim,
> 
>     I agree, rewrite rules are cool and this is clearly a useful
>     generalisation.
> 
>     I vote in favour.
> 
>     A small suggestion when crafting instructions to us -- do not under
>     any circumstances, ever, give us the option of doing nothing! You
>     will be taken up on it (which is a sad reflection os us, not you). :-)
> 
>     Chris
> 
>>     On 2023-01-19, at 09:10, Simon Peyton Jones
>>     <simon.peytonjones at gmail.com <mailto:simon.peytonjones at gmail.com>>
>>     wrote:
>>
>>     Dear GHC Steering Committee
>>
>>     Joachim wrote to us ten days ago recommending acceptance of #555. 
>>     No one has responded.
>>
>>     Would you like to respond, please?  (I think this is an easy one.)
>>
>>     Thanks
>>
>>     Simon
>>
>>     On Tue, 10 Jan 2023 at 11:17, Joachim Breitner
>>     <mail at joachim-breitner.de <mailto:mail at joachim-breitner.de>> wrote:
>>
>>         Dear Committee,
>>
>>         Jaro Reinders and Simon PJ propose to allow  Higher Order
>>         Patterns in Rewrite
>>         Rules.
>>
>>         The idea, by way of an example,
>>
>>            {-# RULES forall f.  foo  (\y. f y + f y) = bar f #-}
>>
>>         will now not only match "foo (\y. negate y + negate y)" (with
>>         f set to negate)
>>         but also "foo (\y. y*y + y*y)" (with f set to (\x. x*x)).
>>
>>         Here "f y" is a higher-order pattern, which are restricted to a
>>         _pattern_ variable followed by a list of _local_ variable,
>>         indicating
>>         which variable the matched expression may depend on
>>         (previously, only
>>         closed expressions could be matched).
>>
>>         An implementation is sitting ready at
>>         https://gitlab.haskell.org/ghc/ghc/-/merge_requests/9343
>>         <https://gitlab.haskell.org/ghc/ghc/-/merge_requests/9343>
>>
>>         The design was carefully crafted to be backward-compatible and not
>>         introduce spurious etwa-expansion where there was non before.
>>
>>         It is not guarded by a LANGUAGE pragma (but RULES themselves
>>         are not).
>>         Library authors who care about backward compat will have to
>>         deal with
>>         CPP pragmas.
>>
>>
>>         I’m a big fan of rewrite rules, and the proposal is straight
>>         forward
>>         and provides a feature that I'd maybe optimistically already
>>         assumed to
>>         be there already. Therefore, I’m recommending acceptance.
>>
>>         If you disagree please speak up within two weeks, or speed up the
>>         process by indicating agreement earlier.
>>
>>         Cheers,
>>         Joachim

-- 
Adam Gundry, Haskell Consultant
Well-Typed LLP, https://www.well-typed.com/

Registered in England & Wales, OC335890
27 Old Gloucester Street, London WC1N 3AX, England