This post continues from an idea of Ryan Ingram’s in an email thread How to make code least strict?.
A pretty story
Pattern matching in function definitions is very handy and has a declarative feel. For instance,
Simply replace “
=” by “
==” to read such a set of pattern clauses (partial definitions) as a collection of properties specifying a
- The sum of an empty list equals zero
- The sum of a (non-empty) list
xplus the sum of the
Moreover, these properties define the
sum function, in that
sum is the least-defined function that satisfies these two properties.
Guards have a similar style and meaning:
=” by “
==” and guards by logical implication, we again have two properties that define
O, the lies!
This pretty story is a lie, as becomes apparent when we look at overlapping clauses.
For instance, we’re more likely to write
abs without the second guard:
A declarative of the second clause (∀ x. abs x == x) is false.
I’d more likely write
which is all the more deceptive, since “
otherwise” doesn’t really mean otherwise.
It’s just a synonym for “
Another subtle but common problem arises with definitions like the following, as pointed out by ChrisK in How to make code least strict?:
These three clauses read like independently true properties for
The first two clauses overlap, but their values agree, so what could possibly go wrong with a declarative reading?
The problem is that there are really three flavors of lists, not two. This definition explicitly addresses the nil and cons cases, leaving ⊥.
By the definition above, the value of ‘
zip  ⊥‘ is indeed
, which is consistent with each clause.
However, the value of ‘
zip ⊥ ‘ is ⊥, because Haskell semantics says that each clause is tried in order, and the first clause forces evaluation of
⊥ when comparing it with
This ⊥ value is inconsistent with reading the second clause as a property.
Swapping the first two clauses fixes the second example but breaks the first one.
Is it possible to fix
zip so that its meaning is consistent with these three properties?
We seem to be stuck with an arbitrary bias, with strictness in the first or second argument.
Or are we?