Rewrite rules involving LHS lambda?

Emil Axelsson 78emil at
Sun Dec 3 17:53:49 UTC 2017

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

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 at

More information about the Glasgow-haskell-users mailing list