Unification

Unification, written &, combines two descriptions of a value into one that satisfies both, or reports that they conflict. The rule is always: keep everything both sides say, and fail if they disagree.

  • A value and a shape: the value, if the shape allows it. This is validation: 20 & (Int & >= 18) is 20.
  • Two shapes: a shape that requires both. Int & >= 18 is itself Int unified with >= 18.
  • Two values: their merge if they agree; #{:a => 1} & #{:a => 2} conflicts on a.
  • Incomplete data: a value with the known fields filled in and the rest still open, completed as more data is unified in.

A failed unification is a never value carrying the reasons (which field, which rule), not an exception. When both sides are known at compile time, the compiler reports the conflict instead.

Pattern matching is one-sided unification, and it is also how a rule matches facts in a store and how a query matches facts in a relation. The idea comes from logic programming and from typed feature structures.