Tight Core, Open Edge
Chapter 13 · Part V

Unification and Search

Propagators narrowed a number from many directions. Unification does the same for structure — finding the assignment of unknowns that makes two structures agree — and search explores when more than one assignment could. A very open technique, guarded almost entirely at runtime.

A propagator cell asked, "what is the price?" and let many sources narrow the answer. This chapter asks a different question: "what assignment of unknowns makes these two structures the same?" Instead of merging numeric ranges, we merge structures that contain variables — and where the propagator settled on one answer, here there may be several, so we must search.

This is the machinery beneath a surprising range of tools. Type inference unifies a program's inferred types against its declared ones. Prolog and logic languages compute entirely by unification and backtracking. A package manager resolving versions searches an enormous space of assignments for one that satisfies every constraint. In the running system, it is how an order finds its way to a warehouse and a carrier: fulfillment routing is a search for an assignment of unknowns — which warehouse, which carrier, what cost — that makes the order match an available route and satisfies every constraint at once.

13.1 Structures With Unknowns

The data is a small, sealed set of forms — a closed structure, exactly as with the evaluator's syntax in Chapter 11. A term is a variable (an unknown to be solved for), an atom (a ground constant like a warehouse id), or a compound (a functor with argument terms, like route(Warehouse, Carrier, Cost)).

-- The structure is closed; the unknowns inside it are what we solve for.
union Term
  Var(name: String)                            -- an unknown
  Atom(value: String)                          -- a ground constant
  Compound(functor: String, args: Array[Term]) -- functor applied to argument terms
end

A substitution is the partial knowledge here, playing the role the range played for propagators: a map from variable names to the terms they have been bound to. Two operations use it — resolve, which follows a term through the current bindings until it reaches an unbound variable or a non-variable, and bind, which extends it with one more binding. Like the propagator's merge, a substitution only ever accumulates.

class Substitution
  create make() do bindings := {} end
feature
  bindings: Map[String, Term]

  bind(vname: String, t: Term): Substitution
  do bindings.put(vname, t)  result := this end

  resolve(t: Term): Term
  do
    match t of
      Var(name) then
        if bindings.contains_key(name) then result := resolve(bindings.get(name))
        else result := t end
      else
        result := t
    end
  end
end

13.2 Unification: Making Two Structures Agree

Unification takes two terms and a substitution, and returns either an extended substitution that makes the two terms identical, or a failure. Failure is data — a Result, as in Chapter 4 — not an exception, because failing to unify is an ordinary, expected outcome that the search above will handle.

-- Is t the variable called name?
function is_var(t: Term, name: String): Boolean
do
  match t of
    Var(name as n) then result := n = name
    else result := false
  end
end

function unify(a: Term, b: Term, s: Substitution): Result[Substitution, String]
do
  let x: Term := s.resolve(a)          -- follow existing bindings first
  let y: Term := s.resolve(b)
  match x of
    Var(name) if is_var(y, name) then
      result := create Ok[Substitution, String].make(s)                 -- X with X: nothing to bind
    Var(name) then
      result := create Ok[Substitution, String].make(s.bind(name, y))   -- bind the unknown
    Atom as ax then
      result := unify_atom(ax, y, s)
    Compound as cx then
      result := unify_compound(cx, y, s)
  end
end

A match clause reads straight into a variant's payload: Var(name) both selects the variable case and binds its name field to a local, with no intermediate v.name — the pattern is the value it destructures. The rules are simple and total over the sealed structure. A variable unifies with anything, by binding to it. The one exception is a variable meeting itself, which has nothing to learn: binding X to X would send resolve round in a circle forever. A guard — an if after the pattern — picks out that case, and when it does not hold the match falls through to the next clause. Two atoms unify only if they are equal; otherwise it is a clash, and clash is a failure, not a crash. Here a guard separates the agreeing atoms from the clashing ones:

function unify_atom(ax: Atom, y: Term, s: Substitution): Result[Substitution, String]
do
  match y of
    Var(name) then
      result := create Ok[Substitution, String].make(s.bind(name, ax))
    Atom(value as v) if v = ax.value then
      result := create Ok[Substitution, String].make(s)              -- atoms agree
    Atom(value as v) then
      result := create Err[Substitution, String].make("clash: " + ax.value + " vs " + v)
    Compound then
      result := create Err[Substitution, String].make("atom does not match a structure")
  end
end

The guarded Atom clause narrows to the agreeing case; the unguarded Atom clause beneath it catches the rest, so the match stays exhaustive over the closed structure even with a guard in play. Two compounds unify when their functors and arities match and their arguments unify pairwise — threading the substitution through, so a binding learned from the first argument constrains the rest. That recursion, and the occurs-check that stops a variable being bound to a structure containing itself, are what keep unification from producing a circular or inconsistent answer. They are the structural analogue of the propagator's ordered invariant: guardrails that catch an inconsistency the moment it would enter.

In code that is two small functions. unify_compound handles the three ways a compound can meet another term; unify_args is the pairwise recursion, carrying each argument's substitution into the next so learning accumulates left to right:

function unify_compound(cx: Compound, y: Term, s: Substitution): Result[Substitution, String]
do
  match y of
    Var(name) then result := create Ok[Substitution, String].make(s.bind(name, cx))
    Atom then result := create Err[Substitution, String].make("structure vs atom")
    Compound as cy then
      if cx.functor = cy.functor and cx.args.length = cy.args.length then
        result := unify_args(cx.args, cy.args, s, 0)       -- functor + arity agree; check the args
      else
        result := create Err[Substitution, String].make("functor / arity mismatch")
      end
  end
end

-- Unify arguments left to right, threading each result substitution into the next.
function unify_args(xs: Array[Term], ys: Array[Term], s: Substitution, i: Integer): Result[Substitution, String]
do
  if i >= xs.length then
    result := create Ok[Substitution, String].make(s)       -- all arguments agreed
  else
    match unify(xs.get(i), ys.get(i), s) of
      Ok as ok then result := unify_args(xs, ys, ok.value, i + 1)   -- carry bindings forward
      Err as e then result := create Err[Substitution, String].make(e.error)
    end
  end
end

The occurs-check named above — refusing to bind a variable to a structure that contains it — is elided here for brevity; a production unifier performs it in the Var case before binding.

Note also that bind extends the substitution in place. The search below gets its "undo" by starting each candidate from a fresh Substitution and discarding it on failure. A search that backtracks part-way through a tree of choices would need bind to return an extended copy instead, so that the state before the choice survives.

13.3 Routing by Unification

An order presents its structure with a destination zone and the items it needs, and each fulfillment route is a pattern over that structure with the unknowns left open. Unifying the order against a route either fails (this route cannot serve this order) or succeeds with the unknowns bound. A route pattern like route("zone-a", Warehouse, Carrier, Cost) unified against an order in zone A binds Warehouse, Carrier, and Cost to whatever that route offers — computing the assignment rather than looking it up, and running in whichever direction the knowns allow.

The power over a hand-written matcher is the same power the DSL had over hand-written handlers: routes are data. New routes are new patterns added to a table, never edits to the router. The set of ways an order can be fulfilled is open, and unification is the engine that matches an order against all of them uniformly.

13.5 The Technique That Lives on Guardrails

How much of unification and search can be guarded by the type system? Very little. The bindings are discovered at runtime; whether any assignment exists is unknown until the search runs; whether the search even terminates is not a fact any signature carries. The compiler can still prove what it proves anywhere — that the match over terms is exhaustive, and that every function returns a value of its declared type — but none of that says whether a search will find anything, or whether what it finds is any good. The type of route tells you it returns a Result[Substitution, String]; but whether the substitution is usable or not is a different question.

So the guarantees are carried, almost in their entirety, by contracts. The variant routes.length - i is a proof of termination: a search whose bound must shrink on every step, and can never fall below zero, cannot run forever, which is the single most important thing to guarantee about any search. And the postcondition satisfies_domain holds every committed solution to satisfies_constraints, refusing to return an answer that type-checks but cannot ship.

Unification and search sit at the far end of the spectrum: open structure, discovered bindings, nondeterministic control, and a type system that can vouch for almost none of it. What keeps such a computation reliable is entirely runtime — failure as data, a variant that proves it ends, and a contract that a committed solution satisfies the domain. This is the flexibility tradition at its most extreme, and the constraint tradition, in the form of a few contracts, is exactly what makes it usable.

13.6 The Edge of the Frontier

Part V explored flexibility in two dimensions the earlier parts did not reach. Propagators opened the topology of computation, letting knowledge arrive from any direction. Unification and search opened its structure and control — objects with unknowns, and a nondeterministic hunt for the assignment that fits. Both left the type system nearly behind, and both stayed reliable only because a small, well-placed contract sat at the one point where an inconsistency could enter.

That is the whole spectrum, now traversed end to end: from a sealed order state whose every case the compiler checks, to a backtracking search the compiler can barely see, with contracts as the connective tissue at every step between. We have seen what it is to constrain, to compose, and to open — and, at each opening, what it costs and what buys the cost back.

Which leaves the final question, the one no technique answers on its own. For the actual decision in front of you — given a type, module, or boundary in a system — do you constrain, or do you open? That is judgment, and Part VI turns it into a working checklist for making the call.