#555: Higher Order Patterns in Rewrite Rules, rec accept

older
Fwd: GHC2023

Joachim Breitner

10 Jan 2023 10 Jan '23

6:17 a.m.

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 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 -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

Show replies by date

Simon Peyton Jones

19 Jan 19 Jan

4:10 a.m.

New subject: #555: Higher Order Patterns in Rewrite Rules, rec accept

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 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

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

-- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Chris Dornan

9:51 a.m.

New subject: #555: Higher Order Patterns in Rewrite Rules, rec accept

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 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

-- Joachim Breitner mail@joachim-breitner.de mailto:mail@joachim-breitner.de http://www.joachim-breitner.de/ http://www.joachim-breitner.de/

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org mailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Joachim Breitner

10:12 a.m.

New subject: #555: Higher Order Patterns in Rewrite Rules, rec accept

Hi, Am Donnerstag, dem 19.01.2023 um 14:51 +0000 schrieb Chris Dornan:

...

I vote in favour.

Thanks :-)

...

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). :- )

Well, in this case silence means silent consent after two weeks, the secret pill of our committee’s productivity… I’m not overly concerned about lack of nods for rather straightforward proposals within the first two weeks, but I am a bit worried about the other 9 proposals that have been lingering for much longer in pending shepherd or pending committee decisions… See https://github.com/ghc-proposals/ghc-proposals/pulls?q=is%3Aopen+is%3Apr+lab... https://github.com/ghc-proposals/ghc-proposals/pulls?q=is%3Aopen+is%3Apr+lab... for the lists (assuming the labels are up-to-date; they are not always), or the last Status Update email. Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

Chris Dornan

10:31 a.m.

New subject: #555: Higher Order Patterns in Rewrite Rules, rec accept

...

Well, in this case silence means silent consent after two weeks, the secret pill of our committee’s productivity… I’m not overly concerned about lack of nods for rather straightforward proposals within the first two weeks, but I am a bit worried about the other 9 proposals that have been lingering for much longer in pending shepherd or pending committee decisions…

Yes, I quite agree -- and have used that same formulation for accepting "Make Symbol a newtype over String". Chris

Arnaud Spiwack

10:31 a.m.

New subject: #555: Higher Order Patterns in Rewrite Rules, rec accept

Hello all, I'm back for real this time, The proposal (link https://github.com/ghc-proposals/ghc-proposals/pull/555 ) is quite reasonable. I think that, in general, higher order patterns are an uncontroversial extension to rewrite rules (it could be extended further but if I remember correctly, there are choices there). 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 think the automatic addition of lambdas is likely to be fairly innocuous (despite the fact that it may change `undefined` into, say, `\x y -> undefined y x`): it happens under lambdas already, so it's unlikely to effectively change the behaviour of program unbeknownst to the rule author. I'm sure someone will eventually manage to be bitten by it. But I think that it's an ok compromise. /Arnaud On Thu, 19 Jan 2023 at 15:51, Chris Dornan 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 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 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

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

-- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Adam Gundry

4:28 p.m.

New subject: #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

Joachim Breitner

23 Jan 23 Jan

2:43 a.m.

New subject: #555: Higher Order Patterns in Rewrite Rules, rec accept

Hi, Am Dienstag, dem 10.01.2023 um 12:17 +0100 schrieb Joachim Breitner:

...

Therefore, I’m recommending acceptance.

since I got only positive or no feedback, I’m marking this as accepted. Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

848

Age (days ago)

861

Last active (days ago)

List overview

Download

7 comments

5 participants

participants (5)

Adam Gundry
Arnaud Spiwack
Chris Dornan
Joachim Breitner
Simon Peyton Jones

#555: Higher Order Patterns in Rewrite Rules, rec accept

tags

participants (5)