Unification and Search

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.

13.2 Unification: Making Two Shapes 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.

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
      when Var(name) then
        result := create Ok[Substitution, String].make(s.bind(name, y))   -- bind the unknown
      when Atom as ax then
        result := unify_atom(ax, y, s)
      when 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 shape it destructures. The rules are simple and total over the sealed structure. A variable unifies with anything, by binding to it. Two atoms unify only if they are equal; otherwise it is a clash, and clash is a failure, not a crash. Here a guard — an if after the pattern — separates the agreeing atoms from the clashing ones, falling through to the next clause when it does not hold:

function unify_atom(ax: Atom, y: Term, s: Substitution): Result[Substitution, String]
  do
    match y of
      when Var(name) then
        result := create Ok[Substitution, String].make(s.bind(name, ax))
      when Atom(value: v) if v = ax.value then
        result := create Ok[Substitution, String].make(s)              -- atoms agree
      when Atom(value: v) then
        result := create Err[Substitution, String].make("clash: " + ax.value + " vs " + v)
      when Compound as c 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.

13.3 Routing by Unification

Now the domain. An order presents a shape — its destination zone, its weight class, the items it needs — and each fulfillment route is a pattern over that shape 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: this warehouse, this carrier, this cost. 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.4 Search: When More Than One Fits

Usually several routes unify with an order, and not all of them will hold up: a route may match structurally but the warehouse is out of stock, or the carrier cannot meet the deadline. So we search — try a candidate, check whether its bindings satisfy the domain constraints, and if not, backtrack and try the next. This is the nondeterminism at the heart of logic programming: commit tentatively, and undo on failure.

-- Try each route; the first whose bindings satisfy every constraint wins.
function route(order: Term, routes: Array[Term]): Result[Substitution, String]
  do
    from
      let i: Integer := 0
      let found: Boolean := false
      result := create Err[Substitution, String].make("no eligible route")
    invariant
      in_range: 0 <= i and i <= routes.length
    variant
      routes.length - i                       -- the search is bounded: it must end
    until
      i >= routes.length or found
    do
      match unify(order, routes.get(i), create Substitution.make()) of
        when Ok as s then
          if satisfies_constraints(s.value) then
            result := create Ok[Substitution, String].make(s.value)   -- commit to this route
            found := true
          end
          -- else: bindings don't satisfy stock/deadline — fall through and backtrack
        when Err as e then
          -- structural mismatch — backtrack and try the next route
      end
      i := i + 1
    end
  end

The essential moves are all here: unify to propose an assignment, test it against the domain, keep it if it holds, and otherwise advance to the next candidate. A richer search would explore a tree rather than a list — routes whose choices open further choices — but the shape is the same: propose, check, backtrack. And whether it seeks the first valid route or the cheapest, the searching itself is the same machinery.

13.5 The Technique That Lives on Guardrails

Unification and search are the most open construction in the book, and it is worth being exact about how little the type system can promise inside them. 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. Everything the compiler proved through Part II — exhaustive states, total functions, values well-formed by construction — is, in the interior of a search, simply unavailable. The type of route tells you it returns a Result[Substitution, String]; it cannot tell you the substitution is any good.

So the guarantees are carried, almost in their entirety, by runtime guardrails — and every one of them is visible in the code above. Failure is data, so a clash or a dead end is an ordinary value the search consumes, not a crash. The variant routes.length - i is a proof of termination: a search that cannot decrease its bound cannot run forever, which is the single most important thing to guarantee about any search. And satisfies_constraints is the domain postcondition that a committed solution must meet — the guardrail that turns "unifies structurally" into "is actually a route we can honor", refusing to return an answer that type-checks but cannot ship.

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 — many sources, many directions, over time. Unification and search opened its structure and control — shapes 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 constraint — a monotone merge, an ordering invariant, a termination variant, a solution postcondition — 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 only question that finally matters, the one no technique answers on its own. For the actual decision in front of you — this type, this module, this seam in this system — do you constrain, or do you open? That is judgment, and it is Part VI. The next chapter turns the whole book into a working checklist for making that call.