Rewrite rules involving LHS lambda?

Joachim Breitner mail at
Sat Dec 2 21:56:27 UTC 2017


Am Samstag, den 02.12.2017, 12:59 -0800 schrieb Conal Elliott:
> 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)

even with these restrictions, they are still useful for rules like

    map (\x -> x) = id

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

And of course higher-order pattern matching is quite a can of worms. I
implemented it in 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?


Joachim Breitner
  mail at
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <>

More information about the Glasgow-haskell-users mailing list