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 branchto go down, you yourself hit a crossroad and need to decide how to writeit. (This is intended to be very meta!) Your choices are conditional branchingand pattern matching. Examples:

When confronted with such tasks, beginners mostly choose conditionalbranching by instinct, that is instinct trained (brainwashed) by inferiorlanguages that lack pattern matching, and therefore conditional branching seemsto 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 fieldsin it. If one single construct (pattern matching) covers the whole in onestroke, why split it into N predicates and N×M selectors (for extraction), onlyto re-combine them in always the same configuration?

Secondly, the correctness of a program for such a task requires two checks: have youcovered all cases, and in each case are you extracting the right fields? Inthe list example: you have to cover 2 cases; in case it is empty, you must notextract 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 tocover 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 thechecks to just parsing and type checking; it is so easy that compilers alwayscheck extraction and optionally check coverage. Conditional branching makes thechecks semantic, placing a heavier burden on humans, and currently compilersdon't give warnings.

I understand that for some tasks you just need the predicates and will notextract any field, and for some other tasks you know the extraction is correctand you do not need to test a predicate. It is true but rare. For example thisrare 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 isalso 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 smallpieces. I acknowledge that often a toolbox is simpler than a monolith, and so itis tempting to prefer the suite of predicates and selectors.

But the criterion for preferring the toolbox is when the small pieces areorthogonal (or nearly). You should be able to use each piece individually,and you should be able to combine any subset of the pieces in anyconfiguration flexibly. (Or nearly.) For example, the suite of fst andsnd is orthogonal: you may freely use one of them alone, or both of themtogether 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 notorthogonal: the valid use of fromJust mx relies on isNothingmx being false. fromVal and fromNeg are notorthogonal: you may not use them both on the same parameter, and you may noteven freely use one of them alone. Every selector may be orthogonal to its M-1sibling selectors but not to the other (N-1)×M selectors, and not to the Npredicates. The plentiful suite supports fairly few combined configurations,with the only prominent one illustrated in the previous section and replaceableby pattern matching. This toolbox is the shards of a sieve. Patternmatching is a monolith but at least a whole sieve. Ironically, a sieve inone intact piece is simpler than the collection of its shards.

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

In Natural Deduction, the introduction rules of ∨ (disjunction, logical or) are howto 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, with3 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, sofirst you argue that P, Q together cover everything (prove P∨Q; sometimes thisis 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 stillcommon sense and pretty clean.

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

The introduction rules resemble type checking of constructing anEither 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 anEither 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. Soactually, people adopt the terminology of Natural Deduction and continue to say“introduction rules” for the contructor rules and “elimination rule” for thecase-of rule.

Pattern matching for most other algebraic data types don't have directparallels in Natural Deduction, but this is just because Natural Deduction lackslogic operators for most algebraic data types. But they have indirect parallelsthrough mimicking the rules of Either. For example, here is theelimination 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 andE?

Natural Deduction offers a clean way to consume P∨Q, which extends to patternmatching as a clean way to consume Either P Q and other algebraicdata 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. Ihave not seen a formal logic that explains a suite of predicates andselectors. In this sense, pattern matching is also more fundamental than thesuite.


I have more Haskell Notes and Examples