Yes, if you confine yourself to Miller's "pattern fragment" (Meta variables may appear in the head of an application, but then the arguments may only be *distinct* bound variables) then you might be fine.
Thanks for giving it a try! Am Mo., 14. Nov. 2022 um 14:27 Uhr schrieb J. Reinders < jaro.reind...@gmail.com>: > I think higher order pattern unification is different from higher order > matching because the unification means both sides are allowed to be > patterns that may contain meta variables, while matching works on only one > pattern and one concrete term. > > The example pattern ‘forall a. someFunction (\x -> a x x)’ would indeed be > a potential problem, but indeed I think disallowing that is fine because it > is never necessary to write such patterns in practice. > > The paper linked by Simon contains another example: ‘forall f x. f x’ > matched to ‘0’, which is also a problem because it has infinitely many > possible solutions, but I would consider this out of scope because it > involves an application of two unification variables. For the practical > examples I’ve seen up to now, we only need to handle the application of one > unification variable with one locally bound variable. > > I’m pretty optimistic now that it is possible to implement an algorithm > that covers the practical use cases (also the Simon’s ‘mapFB' example falls > into this category) while being much simpler than existing algorithms for > both higher order unification and higher order matching. > > I’ll do some experiments with the rule matcher. > > Cheers, > Jaro > > > On 14 Nov 2022, at 14:03, Sebastian Graf <sgraf1...@gmail.com> wrote: > > > > > I believe the reason that this is easier than higher order matching in > general because it is restricted to applications of unification variables > to locally bound variables. > > > > Indeed, it is easier to confine oneself to the pattern fragment. I think > that's entirely the point of pattern unification: Meta variables may appear > in the head of an application, but then the arguments may only be distinct > bound variables. E.g., `α x x` would be disallowed. > > > > Perhaps it is possible to tweak RULEs just enough to match > > > > forall f next. concatMap (λx → Stream next (f x)) = concatMap' next f > > > > (Now that I re-read your RULE, the explicit app `f x` makes sense > compared to the absence of an app in `next` to indicate it must not mention > `x`. I completely overread it before.) > > > > If `f x` should match `x*2+x` with `f := \x -> 2*x+x` then that means > RULE matching modulo beta reductions, for a start. > > Do we also want eta? I think we do, because we are already matching > modulo eta since https://gitlab.haskell.org/ghc/ghc/-/merge_requests/6222 > (and are very careful not to increase arity of target term in doing so). > > > > There are many other troubling issues with pattern unification stemming > from meta variables on both sides of the equation, but perhaps they don't > come up because the target term does not contain meta variables. Solving a > meta variable simply does `eqExpr` with solutions from other use sites, as > today. It doesn't matter much that we are `eq`ing lambdas, because that's > pretty simple to do. > > I can't think of an obvious example where higher-order pattern > *matching* (urgh, what an unfortunate intersection of meaning between > "higher-order pattern unification" and "pattern matching") would be much > more complicated, but I'm no expert in the field. > > > > I didn't know the paper Simon cited, but note that Miller's higher-order > pattern unification (which has become bog standard in dependently-typed > langs) identifies a useful subset that is also efficient to check. It's > surprising that the authors do not compare the pattern fragment to the > identified fragment of their implementation (although they cite it in one > place as [16]). > > > > Anyway, unless someone comes up with a tricky counter-example for a RULE > that would be complicated to check, you should probably just give it a try. > > > > Cheers, > > Sebastian > > > > > > Am Mo., 14. Nov. 2022 um 12:32 Uhr schrieb J. Reinders < > jaro.reind...@gmail.com>: > > Thank you both for the quick responses. > > > > > Can you say precisely what you mean by "using stream fusion instead of > foldr/build fusion in base"? For example, do you have a prototype library > that demonstrates what you intend, all except concatMap? > > > > > > I believe the stream-fusion library [1] and in particular the > Data.List.Stream module [2] implements a version of Data.List from base > with stream fusion instead of foldr/build fusion. It is pretty old at this > point, so it may not completely match up with the current Data.List module > any more and it doesn’t use skip-less stream fusion yet. > > > > I now also see that #915 [3] tracks the exact issue of replacing > foldr/build fusion with stream fusion in base, but is closed because it > required more research at the time. And in that thread, Sebastian already > asked the same question as me 5 years ago [4]: > > > > > At least this could get rid of the concatMap roadblock, are there any > others I'm not aware of? > > > > [1] https://hackage.haskell.org/package/stream-fusion > > [2] > https://hackage.haskell.org/package/stream-fusion-0.1.2.5/docs/Data-List-Stream.html > > [3] https://gitlab.haskell.org/ghc/ghc/-/issues/915 > > [4] https://gitlab.haskell.org/ghc/ghc/-/issues/915#note_141373 > > > > > But what about > > > > > > concatMap (\x. Stream next (x*2 +x)) > > > > > > Then you want matching to succeed, with the substitution > > > f :-> (\p. p*2 +p) > > > > > > This is called "higher order matching" and is pretty tricky. > > > > > > First of all, I’d like to clarify I’ll write ‘unification variable’, but > that might be the wrong term. What I mean is a variable that is bound by a > ‘forall’ in a rewrite rule. So in the example program, I’ll call ‘f’ and > ’next’ unification variables and ‘x’ a local variable. > > > > Higher order matching sounds like it makes the problem too general > (although I’ll admit I haven’t looked into it fully). For this matching I > feel like the core is to change the free variable ‘x’ in the expression > ‘(x*2 +x)’ into a bound variable to get ‘\p -> p*2 +p’. That part sounds > very easy. The only problem that remains is when to actually perform this > change. I would suggest that this should happen when a unification variable > ‘f’ is applied to a locally bound variable ‘x’. The local variable ‘x’ > should only be allowed to occur in unification variables that are applied > to it. > > > > And indeed this seems to be what Sebastian suggests: > > > > > perhaps you could prevent that by saying that `x` may not occur freely > in `next` or `f`, but the paper explicitly *wants* `x` to occur in `next` > > > > > > The paper explicitly says that ‘x’ should *not* occur in ’next’ and ‘f’ > (except indirectly because ‘f’ is applied to ‘x’), so that doesn’t seem > like a problem to me. > > > > In a way I’m suggesting that function application could be used in > rewrite rules to indicate which local variables may scope over which > unification variables. If a unification variable is applied to a local > variable then the local variable may occur in that unification variable. It > should not only match on a literal application. > > > > I believe the reason that this is easier than higher order matching in > general because it is restricted to applications of unification variables > to locally bound variables. No other forms are required for the concatMap > rule. > > > > There can be some discussion about whether this syntax is really > desirable because it changes the way locally bound variables are treated in > rewrite rules, but I personally think the current behavior is not very > reliable anyway. And I don’t think many people are using rewrite rules that > contain local variables. But maybe it would be better to introduce special > syntax for indicating scoping in rewrite rules. Duncan Coutts also uses > this alternative notation: > > > > λx → Stream (⟨next⟩[]) (⟨e⟩[x]) > > > > But I’d guess it would be difficult to extend GHC’s parser to support > that syntax. Re-using function application seems preferable from that > perspective. Another alternative that I considered was this syntax: > > > > concatMap (\x -> Stream next e) = concatMap' next (\x -> e) > > > > Now the matching local variable name on the left and the right could be > used to infer that they are really the same and that ‘x’ should only be > allowed to scope over ‘e’. GHC could just take the intersection of the > scopes on the left and the right to deduce where the local variable ‘x’ > should be allowed to occur (in this case that intersection is just ‘e’). > But this syntax seems a bit more magical to me, so it isn’t my first > choice. This also leads to ambiguities if two locally bound variables on > the same side share the same name, but that could simply be rejected. > > > > Cheers, > > > > Jaro > > > >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
