# 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:

• 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
```

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)
```
```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)
```
```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.

## 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:
• prove P∨Q
• assume P, prove C
• assume Q, prove C
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:
• check `v :: Either P Q`
• assume `x::P`, check `E0::C` (code for the `Left x` case and may use `x`)
• assume `y::Q`, check `E1::C` (code for the `Right y` case and may use `y`)
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:
• check `xs :: [P]`
• check `E0::C` (code for the `[]` case)
• assume `hxs::P` and `txs::[P]`, check `E1::C` (code for the `hxs:txs` case and may use `hxs` and `txs`)
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