Unification versus Pattern Matching… to the death!
by fogus
The number one question asked of me at The Conj^{1} was: what is unification?. Once I explained what unification was and how clojure.core.unify implemented it, the followup question was inevitably: how is unification different from pattern matching?. You see, Drew Colthorp wrote a fantastic pattern matching library called Matchure that creates bindings based on the way that structural forms^{2} match:
(ifmatch [[?a ?b] [1 2]] {'?a a '?b b})
;=> {?a 1, ?b 2}
That is, the bindings a
and b
are created based on the way that the structural template containing the “variables” [?a ?b]
matches with the actual form [1 2]
. The core.unify library works similarly to Matchure for this specific case, as shown below:
(unify '[?a ?b] [1 2])
;=> {?b 2, ?a 1}
So what the heck do we need unification for? The answer lies in the question: what happens when there is a variable element on both sides of the match?
(ifmatch [[?a ?b] [1 ?a]] {'?a a '?b b})
; java.lang.Exception:
; Unable to resolve symbol: ?a in this context
Pattern matching, while powerful^{3} does not handle the case where matching variables appear on both sides of the check. However, this scenario is exactly where unification shines:
(unify '[?a ?b] '[1 ?a])
;=> {?b 1, ?a 1}
And there we have it — the fundamental difference between unification and pattern matching. There are of course vast differences between the implementations of Matchure and core.unify^{4}, but I’ll save those for another day.
:f

Besides, “Will you please go away?” ↩

I’ll bet Drew gets asked all the time: What is the difference between pattern matching and destructuring? :p ↩

Having used Scala over the past 2.75 years, I must say that I’ve grown to feel exquisite sadness whenever I use a language without pattern matching. ↩

One huge difference that should be immediately apparent, is that Matchure does binding while core.unify does not. I plan to add binding sooner rather than later. ↩
Comments
Real world examples wanted.
Also, only hundredths place precision on Scala experience? :)
@Scott
I set the type to Float and couldn’t change it without recompiling the blog post! ;)
As for realworld examples, that will have to wait for another post. (Sorry)
:F
Unification also works with duplication of variables:
(unify ‘[?a ?a] [1 1])
Does matchure handle this case? I that for some reason Haskell doesn’t allow this…
@Paul Hobbs
Matchure will work in that case also:
So will Erlang:
The failure of Haskell in this case (so to speak) is not a unification vs. matching problem but instead a byproduct of Haskell’s implementation of pattern matching (linear).
:F
So can pattern matching considered a special case of unification? Or, if not, what is a case that work with pattern matching but not with unification?
All – There’s a lot of excellent learning material on Prolog, one of the grandfathers of unification. The core of Prolog is tiny and easy to learn and the style of programming is eye opening. One way to look at Prolog is that when you write a rule you are writing multiple functions: not just from args to result but result to arg. If you prefer to stay Lispy then there’s the Reasoned Schemer which shows how to implement a subset of Kanren.
All of typical ML style pattern matching can be compiled down to a series of nested if/else if/else (or cond or whatever) blocks*. Importantly, once a criterion has been matched a later criterion can only cause the whole pattern to succeed or fail to match. There’s no backtracking to see if something else would have worked.
Unification requires recursion, backtracking, and an accumulation of satisfied and unsatisfied goals. It’s a form of search.
A single pattern match produces at most one match – it binds at most one value to each variable. Unification may produce a stream of potentially infinitely many variable/value pairs that satisfy the constraints. In a Turing complete logic language unification can also get stuck in a nonproductive infinite loop whereas ML style pattern matching cannot (Scala extractors and Haskell views make infinite loops possible, but they’re a bit ancillary to the core concept of pattern matching).
@Philipp Meier – pattern matching is a very limited special case of unification. There’s nothing that can be expressed in pattern matching that can’t also be expressed in a unification language.
James, I think you’re conflating unification with resolution.
Indeed, Prolog’s SLD resolution is a form of search, and uses backtracking both to find the first answer/resolution and to return additional answers (or fail).
Unification itself doesn’t require backtracking at all.
Just want to thank fogus as well as all the commenters here – I’ve been struggling with this exact question and this has helped a ton. Thanks!
There are 3 notions:
Unification – which involves two terms a,b with variables, producing a most general unifier θ such that aθ = bθ.
Matching – which also invloves two terms with variables, but which produces a substitution θ such that aθ = b.
And then there is pattern matching, it involves one variable free term and one term with variables.
Pattern matching as both a special case of unification as well as a special case of matching. However, matching is not a special case of unification.
… and then there is onesided unification, which is often called matching – such that:
aθ = b and aθ = a.
Gah! None of this even answered what Unification actually is.
@James Iry got the closest to providing a coherent description of what the darn concept actually is: “A single pattern match produces at most one match – it binds at most one value to each variable. Unification may produce a stream of potentially infinitely many variable/value pairs that satisfy the constraints. “
So unification is binding values that meet certain constraints to some given variables (including undefined ones)? What the friggin’ heck.