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

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 mailto:chris@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 mailto:simon.peytonjones@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 mailto:mail@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