Unification function

[Lysxia]

Does unbound have a unification function? If not, does that seem like a good addition? To be precise, I'm looking for a function such that, given two terms t0, t1, finds a substitution s such that substs s t0 `aeq` t1, if it exists.

[lambdageek]

Unbound itself does not have a unification function. It is of course possible to write one over terms built up with unbound.

I suspect that a complete first-order unification algorithm probably doesn't belong within unbound-generics itself (for the reason that there are a fair number of extensions that people often want on top of plain vanilla first-order unification - residual constraints, various extensions to deal with limited forms of higher-order terms, etc). That said we can probably have more primitive operations in unbound for the kinds of things that first order unification algorithms may want to do with terms. (Or maybe some of our binding forms are useful but too slow - we should think about making them more effective)

I wrote a fairly generic first-order unification algorithm for a project that I worked on a couple of years ago (https://github.com/ppaml-op3/insomnia/blob/master/src/Insomnia/Unify.hs) and maybe that's a useful starting point for you? (Note that I represented unification variables distinctly from unbound's Names - that seemed like the right choice at the time). However, if I had to do it over again, I probably should have used unification-fd

[Lysxia]

Thanks for the helpful answer! I can get by with a simple solution for the moment, but those references will certainly be useful.