Hi, 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,
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?
Joachim
--
Joachim Breitner
[email protected]
http://www.joachim-breitner.de/
signature.asc
Description: This is a digitally signed message part
_______________________________________________ Glasgow-haskell-users mailing list [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
