Unification
This is the chapter this whole course's own framing has been pointing toward. Unification looks, at a glance, like Haskell's pattern matching — both languages check whether a value has a certain shape and bind pieces of it to names. They are not the same mechanism, and the difference is real and structural.
What Unification Actually Does
Two terms unify if they can be made identical by substituting values for variables. X = 5 doesn't assign — it attempts to unify the unbound variable X with 5, which succeeds by binding X. 5 = 5 succeeds trivially (already identical); 5 = 6 fails outright — no substitution could ever make them equal.
Unifying Two Variables
When both sides are unbound, unification succeeds by linking them — if either is later bound to something concrete, the other becomes bound too. Genuinely different from every other language's own assignment, which always gives a value to a variable, never links two unknowns to each other.
Unifying Compound Terms — Structural Matching
Genuinely comparable to Haskell's own pattern matching on a constructor's shape — same functor name, same arity required, corresponding arguments unified pairwise.
The Central Contrast — Bidirectional vs. One-Directional
Here's the explicit, promised reveal: haskell1-7's own pattern matching always matches a known, already-computed value against a pattern — the pattern side can never "reach backwards" and solve for an unknown piece of the value being matched. Prolog's unification has no such asymmetry at all. There is no "the pattern" and "the value" in Prolog — only two terms being made equal, in either order, or with variables on both sides at once. Genuinely bidirectional, where Haskell's matching is genuinely one-directional.
A Concrete Demonstration — Solving What Pattern Matching Never Could
X is bound to g(Z) — a compound term that itself still contains an unbound variable — and later, Z gets unified with 3, retroactively completing X's own value. Values can be partially known and progressively refined. Haskell's pattern matching has no equivalent to this "partially solved, filled in later" behavior at all — matching there is all-or-nothing against an already-complete value.
The Unification Algorithm, Briefly
A real, honest technical note: the full unification algorithm includes an "occurs check" to detect a variable unifying with a term that contains itself — but SWI-Prolog, by default, does not perform this check, for performance reasons. Worth naming plainly rather than glossing over, matching this site's established pattern of honest technical caveats.
| Aspect | Haskell pattern matching (haskell1-7) | Prolog unification |
|---|---|---|
| Direction | one-directional — value vs. pattern | bidirectional — no fixed roles |
| Can solve for unknowns on both sides | no | yes |
| Partially-bound compound results | not possible | routine (X bound to g(Z), Z unbound) |
= as an imperative assignment is the single most common early Prolog mistake — prolog1-7's own is/=/== chapter builds directly on getting this distinction right now.
X = f(X) should, in principle, fail — a variable can never legitimately unify with a term containing itself. Without the occurs check, SWI-Prolog instead silently creates a cyclic term by default. Genuinely surprising behavior, not a bug, worth knowing about before it causes real confusion.
Coding Challenges
In swipl, unify point(X, Y) with point(7, 9) and then, separately, unify point(7, 9) with point(X, Y) (reversed order), showing both produce identical bindings.
📄 View solutionWrite a single query that unifies pair(X, Y) with pair(f(Z), 10) and then unifies Z with 42 in the same query (using a comma), printing the final bindings for X, Y, and Z.
📄 View solutionWrite a short comment giving a concrete example of a task unification can do that Haskell's pattern matching genuinely cannot, explaining specifically what "bidirectional" buys in that example.
📄 View solutionChapter 3 Quick Reference
- = attempts unification, not assignment — two terms unify if a substitution can make them identical
- Two unbound variables unify by linking together, not by one taking a value from the other
- Compound terms unify structurally — same functor, same arity, arguments unified pairwise
- THE central contrast: unification is bidirectional (no fixed pattern/value roles), Haskell's own pattern matching (haskell1-7) is strictly one-directional
- A variable can be bound to a compound term that itself still contains unbound variables, refined later — no Haskell pattern-matching equivalent
- SWI-Prolog skips the occurs check by default — X = f(X) creates a cyclic term rather than failing
- Next chapter: backtracking and the search tree — how multiple answers actually get explored