read


read or learn more

Unification versus Pattern Matching… to the death!

Dec 14, 2010

The number one question asked of me at The Conj1 was: what is unification?. Once I explained what unification was and how clojure.core.unify implemented it, the follow-up 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 forms2 match:

(if-match [[?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?

(if-match [[?a ?b] [1 ?a]] {'?a a '?b b})

; java.lang.Exception: 
;   Unable to resolve symbol: ?a in this context

Pattern matching, while powerful3 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.unify4, but I’ll save those for another day.

:f

  1. Besides, “Will you please go away?” ↩

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

  3. 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. ↩

  4. 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. ↩

Related posts:

  1. Pattern Matching vs. Destructuring… to the death!
  2. Pattern Matching vs. Destructuring… Electric Boogaloo
  3. Unifycle: A Unification Library for Clojure
  4. Unifycle phased out
  5. Clojure Obscura

11 Comments, Comment or Ping

  1. Scott

    Real world examples wanted.

    Also, only hundredths place precision on Scala experience? :)

    Dec 14th, 2010

  2. fogus

    @Scott

    I set the type to Float and couldn’t change it without recompiling the blog post! ;-)

    As for real-world examples, that will have to wait for another post. (Sorry)

    :F

    Dec 14th, 2010

  3. 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

  4. fogus

    @Paul Hobbs

    Matchure will work in that case also:

    (if-match [[?x ?x] [1 1]] x :no)
;=> 1

    So will Erlang:

    {A, A} = {1, 1}.
A.
%=> 1

    The failure of Haskell in this case (so to speak) is not a unification vs. matching problem but instead a by-product of Haskell’s implementation of pattern matching (linear).

    :F

    Dec 14th, 2010

  5. 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

  6. 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 non-productive 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.

    • Note, I think Erlang pattern matching is strictly speaking a little bit richer than ML pattern matching, but still nowhere near as rich as full unification.

    Dec 15th, 2010

  7. 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

  8. 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

  9. 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

  10. false

    … and then there is one-sided unification, which is often called matching – such that:

    aθ = b and aθ = a.

    Jul 6th, 2013

  11. pog

    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.

    Nov 27th, 2015

Reply to “Unification versus Pattern Matching… to the death!”