Rewrite rules involving LHS lambda?

[Emil Axelsson]

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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>