Unification versus Pattern Matching… to the death!
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. ↩
10 Comments, Comment or Ping
Scott
Real world examples wanted.
Also, only hundredths place precision on Scala experience? :)
Dec 14th, 2010
fogus
@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
Dec 14th, 2010
Paul Hobbs
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…
Dec 14th, 2010
fogus
@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
Dec 14th, 2010
Philipp Meier
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?
Dec 15th, 2010
James Iry
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.
Dec 15th, 2010
Frank Shearar
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.
May 26th, 2011
Nick Knowlson
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!
Aug 29th, 2012
false
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.
Jul 6th, 2013
false
… and then there is onesided unification, which is often called matching – such that:
aθ = b and aθ = a.
Jul 6th, 2013
Reply to “Unification versus Pattern Matching… to the death!”