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:
Example: mx
is a Maybe
value. If it is
Nothing
, answer one thing; if it is a Just x
, answer
another thing based on x
.
conditional branching | pattern matching |
---|---|
g mx = if isNothing mx then "nada" else show (fromJust mx) |
g mx = case mx of Nothing -> "nada" Just x -> show x |
g mx | isNothing mx = "nada" | otherwise = show (fromJust mx) |
g Nothing = "nada" g (Just x) = show x |
Example: xs
is a list. If it is empty, answer one thing; if not,
answer another thing based on its head and tail.
conditional branching | pattern matching |
---|---|
f xs = if null xs then "nada" else show (head xs) ++ f (tail xs) |
f xs = case xs of [] -> "nada" hxs:txs -> show hxs ++ f txs |
f xs | null xs = "nada" | otherwise = show (head xs) ++ f (tail xs) |
f [] = "nada" f (hxs:txs) = show hxs ++ f txs |
Example: e
is of some simple expression type:
data E = Val{fromVal::Integer} | Neg{fromNeg::E} | Add{fromAdd0, fromAdd1 :: E} isVal Val{} = True isVal _ = False isNeg Neg{} = True isNeg _ = False isAdd Add{} = True isAdd _ = False
Evaluate e
: if it is a Val
, answer the integer in it;
if it is a Neg
, recurse and put a minus sign; if it is an Add
,
recurse and add.
conditional branching | pattern matching |
---|---|
eval e = if isVal e then fromVal e else if isNeg e then - eval (fromNeg e) else eval (fromAdd0 e) + eval (fromAdd1 e) |
eval e = case e of Val n -> n Neg e0 -> - eval e0 Add e0 e1 -> eval e0 + eval e1 |
eval e | isVal e = fromVal e | isNeg e = - eval (fromNeg e) | isAdd e = eval (fromAdd0 e) + eval (fromAdd1 e) |
eval (Val n) = n eval (Neg e0) = - eval e0 eval (Add e0 e1) = eval e0 + eval e1 |
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.
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:
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
:
v :: Either P Q
x::P
, check E0::C
(code for the Left x
case and may use x
)
y::Q
, check E1::C
(code for the Right y
case and may use y
)
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:
xs :: [P]
E0::C
(code for the []
case)
hxs::P
and txs::[P]
,
check E1::C
(code for the hxs:txs
case and may use hxs
and
txs
)
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