Thanks for the reply, Ed.

I'd assume that `x` didn't occur in either `u` or `v`

This is exactly the issue I'm wondering about. Since rewrite rules admit lambdas and only first-order matching, I'm wondering whether they're interpreted as you did (and I'd tend to), namely that `x` doesn't occur freely in `u`or `v`, in which case lambdas don't seem useful in rules (and yet were implemented for some reason) or they're interpreted as allowing `x` in `u` and `v`, and substitution captures. I'm still puzzled. With a wee bit of higher-order matching, one might make `u` and `v` functions and instead write:

foo (\ x -> fmap (u x) (v x)) = bar u v

In that case I'd expect `u` and `v` to be synthesized rather than literally matched. For instance, `foo (\ (a,b) -> fmap (+ a) [b,b,b])` would match with `u = \ (a,b) -> (+ a)` and `v = \ (a,b) -> [b,b,b]`. -- Conal On Sat, Dec 2, 2017 at 12:20 PM, Edward Kmett wrote:

I don't knw of a formal writeup anywhere.

But does that actually mean what you are trying to write?

With the effective placement of "forall" quantifiers on the outside for u and v I'd assume that x didn't occur in either u or v. Effectively you have some scope like forall u v. exists x. ...

Under that view, the warnings are accurate, and the rewrite is pretty purely syntactic.

I don't see how we could write using our current vocabulary that which you want.

On Sun, Dec 3, 2017 at 4:50 AM, Conal Elliott wrote:

...

Is there a written explanation and/or examples of rewrite rules involving a LHS lambda? Since rule matching is first-order, I'm wondering how terms with lambda are matched on the LHS and substituted into on the RHS. For instance, I want to restructure a lambda term as follows:

...

foo (\ x -> fmap u v) = bar (\ x -> u) (\ x -> v)

My intent is that the terms `u` and `v` may contain `x` and that whatever variable name is actually used in a term being rewritten is preserved so as to re-capture its occurrences on the RHS.

When I write this sort of rule, I get warnings about `x` being defined but not used.

Thanks, -- Conal

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Den 2017-12-02 kl. 21:56, skrev Joachim Breitner:

...

With a wee bit of higher-order matching, one might make `u` and `v` functions and instead write:

...

foo (\ x -> fmap (u x) (v x)) = bar u v

In that case I'd expect `u` and `v` to be synthesized rather than literally matched. For instance, `foo (\ (a,b) -> fmap (+ a) [b,b,b])` would match with `u = \ (a,b) -> (+ a)` and `v = \ (a,b) -> [b,b,b]`.

That would be nice and interesting, but we don’t do that now, unfortunately.

And of course higher-order pattern matching is quite a can of worms. I implemented it in http://incredible.pm/ but that was a much simpler setting than a complex typed language like Core.

Implementing some form of higher-order pattern matching might actually be doable, but would it be reliable? When does it become undecidable?

Miller's pattern unification is quite useful for rewriting, and the above example falls within that (all meta-variables are applied only to object variables). Rewriting based on pattern unification is decidable and efficient; see this paper: http://www.cse.chalmers.se/~emax/documents/axelsson2015lightweight.pdf However, that paper assumes a normalized representation, so I'm not sure how well it would work in a compiler like GHC. / Emil

Joachim

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users