Saturday, April 2, 2016

Unification: Things Pattern Matching Can't Do

This document is an answer to the question “Pattern Matching: Is There Anything it Can't Do?

Before we talk about the differences between pattern matching and unification, let’s talk about multiple assignment and destructuring assignment. Multiple assignment is a programming language feature that lets you assign multiple variables at once and assign different values to different variables. It might have a syntax like this:

x, y := 1, 2

There is a question about how to interpret the above statement. Should we view this as an assignment operator with two operands, one of which is the pair x,y and the other the pair 1,2, or should we view it as an operation with four independent operands: x, y, 1, and 2? If there are just two arguments, then you could replace either of them with a variable name and it would do the same thing:

t1 := x, y
t2 := 1, 2
t1 := t2

For most languages with multiple assignment, this does not do the same thing as the previous example (but with unification, it would).

There are languages such as Python and Go that choose an intermediate solution: the original expression has three operands: x, y, and the pair 1, 2. This one-sided solution is called destructuring assignment. Destructuring assignment is a one-sided form of multiple assignment where the phrase on the left is a syntactic structure that is part of the assignment operation and the expression on the right represents a value:

t1 := [1, 2]
[x, y] := t1  # destructuring assignment

The intermediate variable t1 is used to show that the expression on the right hand side represents a single value. This destructuring assignment still has three arguments, x, y, and t1. The clause [x, y] may look like a list constructor, but it is really part of the syntax of the assignment statement.

Pattern matching is a form of destructuring assignment that can be used in conditional contexts to affect flow of control. For example, in Scala and Rust there is a case statement that can be used to select one branch (and set of assignments) based on the pattern. Because pattern matching is an extension to destructuring assignment, I’ll continue to use the same symbol, “:=”. Here are some examples of pattern matching in a conditional context:

if [x, y] := [1, 2]
 then  # executes with x=1, y=2
 else  # does not execute
if [x, y] := [1, 2, 3]
 then  # does not execute because the match failed
 else  # executes, but x and y are unassigned

The clause on the left of the assignment operator is called the pattern. Just as for other destructuring assignments, the pattern is part of the syntax of the assignment and is not a data object on its own. On the right side is the match subject or just the subject.

Unification is both an equality predicate and a two-sided form of multiple assignment that matches a value to a value instead of a pattern to a value. It is a feature used in some logic programming languages such as Prolog and miniKanren to get the effect of logical equality. Let’s use the symbol “=” to represent unification:

[a, b] = [1, 2]  # succeeds and assigns a=1, b=2
[a, b] = [1, 2, 3]  # fails

This example makes unification look a lot like pattern matching, but there are important differences. What underlies the differences is this: unification is two-sided and works on logical variables, while pattern matching is one-sided and works on normal programming-language variables or normal single-assignment variables.

A logical variable is like a single-assignment variable but it can be used before it is assigned a value. In other words, it can be put in a structure, passed to a function, returned from a function, or have a predicate applied to it before ever being assigned. Pattern matching works on normal programming-language variables--mutable variables, or normal single-assignment variables.

For my examples, I’ll use the fictional programming language, Unobtainabol. Unobtainabol has all three kinds of variables, declared with the words “logical”, “mutable”, or, for a single-assignment variable, “constant”:

logical a, b
mutable x, y
constant i, j
[a, b] = [1, 2]  # unification assigns a=1, b=2
[x, y] := [11, 12]  # matching assigns x=11, y=12
[i, j] := [21, 22]  # matching assigns i=21, j=22

Unification is two-sided--it modifies variables on both sides:

logical a, b
mutable x, y
constant i, j
[a, 2] = [1, b]  # unification assigns a=1, b=2
[x, 12] := [11, y]  # error: accessing undefined variable y
[i, 22] := [21, j]  # error: accessing undefined constant j

In unification, both sides of the operation must be a term. A term in logic programming is not syntax but data, just like a list or a set. In fact, lists and sets are terms. A term is defined recursively as follows: a constant, a logical variable, or a structure where the parts are terms. Some examples:

[1, 2]
[1, [2, a]]

Once we have terms with logical variables, we need a word to describe data objects that do not contain logical variables: a constant term is a constant or a structure where the parts are constant terms. The right hand side of a pattern-matching statement must be a constant term.

Because unification has terms on both sides, there is the possibility of unifying two unassigned variables to each other:

logical a, b
[a, 1] = [b, 1]  # unifies a=b but a and b are unassigned
a = b  # unifies a=b but a and b are unassigned
b = 1  # assigns a=1, b=1

A common way of viewing this is that a=b creates a constraint on a and b. A constraint is a predicate that is asserted of logical variables--possibly before they are assigned--and prevents any assignment to those variables that violates the predicate. Prolog only has equality constraints, but other logic languages have other sorts of constraints, such as non-equality, less-than/greater-than, member of a set, etc.

Let’s borrow some terminology from variable scoping and say that a lexically restricted assignment is one in which the only variables that can be assigned are those that appear syntactically in the assignment statement. Normal assignment is lexically restricted--only the variable on the left of the assignment statement can change (a variable can be aliased, but you still have only one variable with multiple names).

Pattern matching is lexically-restricted, unification is not. Consider:

logical a, b, x
x = [a, b]
x = [1, 2]  # succeeds and sets a=1, b=2, x=[1, 2]

The second unification binds the variables a and b which do not appear in the statement.

Another consequence of logical variables is that unification is non-sequential--bindings can happen in any order and the outcome is the same. For example given:

logical a, b, c
a = b
b = c
c = 1

You can do the three unifications in any order and get the same final result: all three variables equal to 1. Pattern matching, like assignment, is sequential:

mutable x, y
x := 1
y := x

If you reverse the order of the pattern-matching statements, the first one will cause an error because x will be undefined at the point of use.

A related feature is that unification is idempotent. The same unification can be done any number of times and it doesn’t change the ultimate outcome, either the success/failure outcome or the binding of variables on success:

logical a, b
a = b
a = b
a = 1
b = 1
b = a

This is not true for pattern matching with mutable variables:

mutable x, y
x := 1
x := x+1

The end result of this is that x=2, but if you repeat the second pattern-matching statement then the end result would be x=3.

Pattern matching with single-assignment variables is not idempotent either with the usual implementation:

constant i
i := 1  # succeeds
i := 1  # error -- i is already assigned

However, there is a variation where patterns are allowed to have constants in the term and it acts like a restriction:

constant i, j
[1, i, j, 4] := [1, 2, 3, 4]  # succeeds, sets i=2, j=3
[4, i, j, 1] := [1, 2, 3, 4]  # fails -- constants do not match up

With this feature, patterns on single-assignment variables are idempotent:

constant i
i := 1  # succeeds
i := 1  # succeeds by matching constant to literal

But in general, pattern matching is not idempotent.

We typically think of pattern matching as a feature that assigns variables, but only if the match subject has a certain structure. In other words, we generally think that every value that matches a certain pattern must be structurally equivalent, but this is not true. In Python, for example the following both succeed even though the values on the right are not structurally equivalent (the code is actual Python, which means that “=” represents destructuring assignment):

a, b = (1, 2)
a, b = [1, 2]

This is a way in which pattern matching is more expressive than unification: patterns can have special syntax that let a single pattern match a broader variety of structures. For example, you could define a syntax x<=expr that means, “if there is no member to match against x, then succeed anyway and assign the default value expr to x.” For example:

mutable x, y
[x, y<=10] := [1, 2]  # succeeds, sets x=1, y=2
[x, y<=10] := [1]  # succeeds, sets x=1, y=10

So, with all of that, here is a summary of the differences:

pattern matching
Matches a syntactic pattern to a data object.
Matches a data object to a data object.
mutable variables or single-assignment variables
logical variables
one-sided: Only assigns to variables on the left.
two-sided: Assigns in both directions.
No constraints are created.
Can create equality constraints.
lexically restricted: Only assigns to variables that occur syntactically in the statement.
lexically unrestricted: Assigns to variables that do not occur syntactically in the statement.
sequential--Assignments must occur in the presented order.
non-sequential--Assignments can be done in any order.
non-idempotent--Assignments cannot generally be repeated.
idempotent--Assignments can be repeated without changing the effect.
A single pattern can match different terms with different structures.
A term can only match another term with the same structure.