A Crossroad at A Branch

Albert Y. C. Lai, trebla [at] vex [dot] net

Practice

Whenever your program hits a branching point and needs to decide which branch to go down, you yourself hit a crossroad and need to decide how to write it. (This is intended to be very meta!) Your choices are conditional branching and pattern matching. Examples:

When confronted with such tasks, beginners mostly choose conditional branching by instinct, that is instinct trained (brainwashed) by inferior languages that lack pattern matching, and therefore conditional branching seems to be the only way. But I argue that we should use pattern matching.

Firstly, the task is to tell apart N cases, and in each case extract and use M fields in it. If one single construct (pattern matching) covers the whole in one stroke, why split it into N predicates and N×M selectors (for extraction), only to re-combine them in always the same configuration?

Secondly, the correctness of a program for such a task requires two checks: have you covered all cases, and in each case are you extracting the right fields? In the list example: you have to cover 2 cases; in case it is empty, you must not extract anything; and in case it is non-empty, you may extract 2 fields, but you have to mind their types. In the E example, you have to cover 3 cases; in case it is a Val, you may only extract 1 field, not 2, and it is a number, not a subexpression. Pattern matching reduces the checks to just parsing and type checking; it is so easy that compilers always check extraction and optionally check coverage. Conditional branching makes the checks semantic, placing a heavier burden on humans, and currently compilers don't give warnings.

I understand that for some tasks you just need the predicates and will not extract any field, and for some other tasks you know the extraction is correct and you do not need to test a predicate. It is true but rare. For example this rare use of head is correct:

  map head (group [1, 1, 1, 4, 4, 1, 1])
= [1, 4, 1]

I am saying that if a task uses both the predicates and the extraction functions, then it is much clearer and simpler to use pattern matching.

Philosophy

Besides bringing the practical benefits mentioned above, pattern matching is also more sound than a suite of N predicates and N×M selectors. Here is why.

Before I begin, I note that pattern matching is a monolith, a package deal, and the suite of predicates and selectors is a toolbox, a collection of small pieces. I acknowledge that often a toolbox is simpler than a monolith, and so it is tempting to prefer the suite of predicates and selectors.

But the criterion for preferring the toolbox is when the small pieces are orthogonal (or nearly). You should be able to use each piece individually, and you should be able to combine any subset of the pieces in any configuration flexibly. (Or nearly.) For example, the suite of fst and snd is orthogonal: you may freely use one of them alone, or both of them together on the same tuple (or none of them, but that's too easy).

The problem with predicates and selectors is that they are not orthogonal, not nearly enough. fromJust and isNothing are not orthogonal: the valid use of fromJust mx relies on isNothing mx being false. fromVal and fromNeg are not orthogonal: you may not use them both on the same parameter, and you may not even freely use one of them alone. Every selector may be orthogonal to its M-1 sibling selectors but not to the other (N-1)×M selectors, and not to the N predicates. The plentiful suite supports fairly few combined configurations, with the only prominent one illustrated in the previous section and replaceable by pattern matching. This toolbox is the shards of a sieve. Pattern matching is a monolith but at least a whole sieve. Ironically, a sieve in one intact piece is simpler than the collection of its shards.

Pattern matching as embodied in the case-of expression is also in a clean—though not obvious—relation with the constructors. (Whereas selectors, being partial functions, are in a rough—though obvious—relation with the constructors.) This relation parallels that in Natural Deduction between elimination rules and introduction rules.

In Natural Deduction, the introduction rules of ∨ (disjunction, logical or) are how to reach a conclusion P∨Q:

(do one of the following)
prove P, then claim that this proves P∨Q
prove Q, then claim that this proves P∨Q

The elimination rule of ∨ is how to use P∨Q to reach another conclusion C:

do these: then claim that this proves C

The introduction rules border on “duh”. The elimination rule looks hard, with 3 subproofs to do and whatnot, but you have known and done it as case analysis: to prove C, you may recognize that there are only two cases P, Q to consider, so first you argue that P, Q together cover everything (prove P∨Q; sometimes this is trivial, like x<0 ∨ x≥0, and you skip it), then you assume P to prove C, and assume Q to prove C, done. The rule is a bit long to state and read, but it is still common sense and pretty clean.

More importantly, the introduction rules say how to produce a compound sentence like P∨Q from its ingredients, and the elimination rule says how to consume a compound sentence like P∨Q and use its ingredients. This brings us to…

The introduction rules resemble type checking of constructing an Either P Q value:

(do one of the following)
check x::P, then claim Left x :: Either P Q
check y::Q, then claim Right y :: Either P Q

The elimination rule resembles type checking of pattern matching an Either P Q value to obtain another value of type C:

do these: then claim case v of { Left x -> E0; Right y -> E1 } :: C

These extend the Natural Deduction rules to include program code. So actually, people adopt the terminology of Natural Deduction and continue to say “introduction rules” for the contructor rules and “elimination rule” for the case-of rule.

Pattern matching for most other algebraic data types don't have direct parallels in Natural Deduction, but this is just because Natural Deduction lacks logic operators for most algebraic data types. But they have indirect parallels through mimicking the rules of Either. For example, here is the elimination rule of lists:

do these: then claim case xs of { [] -> E0; hxs:txs -> E1 } :: C

Exercise: Can you write down the elimination rules of Maybe P and E?

Natural Deduction offers a clean way to consume P∨Q, which extends to pattern matching as a clean way to consume Either P Q and other algebraic data types. Many other formal logics differ in syntax but agree in essence, for example both Sequent Calculus and Hilbert Calulus say: assume P, prove C; assume Q, prove C. In effect, these formal logics explain pattern matching. I have not seen a formal logic that explains a suite of predicates and selectors. In this sense, pattern matching is also more fundamental than the suite.


I have more Haskell Notes and Examples