search

wrengr / unification-fd

Generic functions for single-sorted first-order structural unification
Other
40 stars 11 forks source link

Can `applyBindings` affect the semantics/result? #80

Closed bladyjoker closed 4 months ago

bladyjoker commented 4 months ago

I'm using applyBindings pervasively in https://github.com/mlabs-haskell/lambda-buffers/blob/401f8a920a557c71440795174da199a1e128c4f9/lambda-buffers-compiler/src/LambdaBuffers/Compiler/MiniLog/UniFdSolver.hs#L254.

It was very difficult to understand what's happening, but without it the whole thing just doesn't work. On multiple occasions I tried to debug this, and from what I can tell the 'variable sharing' business makes some unification (as on one side there's a variable) succeed when it shouldn't. This is 'fixed' by using applyBindings throughout to resolve any term completely so it doesn't contain shared variables.

I'd appreciate some advice here as it's my impressions that applyBindings should NOT be able to affect the semantics of a unification-fd program.

Thanks!

bladyjoker commented 4 months ago

I think I got it, the https://github.com/mlabs-haskell/lambda-buffers/blob/401f8a920a557c71440795174da199a1e128c4f9/lambda-buffers-compiler/src/LambdaBuffers/Compiler/MiniLog/UniFdSolver.hs#L186 was implemented naively. Closing!

wrengr commented 3 months ago

Sorry it took so long to get back to you on this.

As you say, applyBindings should only affect the operational semantics of structure sharing, and shouldn't affect the logical semantics (except perhaps in some corner cases where it triggers an occurs check that would otherwise be avoided). For what I think your duplicateTerm intends to do, you should be able to just call freshen instead.

If you're still having any issues, do feel free to file another ticket (and I should be able to respond promptly now).