Lazier function definitions by merging partial values
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,
sum [] = 0
sum (x:xs) = x + sum xs
Simply replace “=” by “==” to read such a set of pattern clauses (partial definitions) as a collection of properties specifying a sum function:
- The sum of an empty list equals zero
- The sum of a (non-empty) list
x:xsequalsxplus the sum of thexs.
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:
abs x | x < 0 = -x
abs x | x >= 0 = x
Replacing “=” by “==” and guards by logical implication, we again have two properties that define abs:
x < 0 ==> abs x == -x
x >= 0 ==> abs x == x
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:
abs x | x < 0 = -x
abs x = x
A declarative of the second clause (∀ x. abs x == x) is false.
I’d more likely write
abs x | x < 0 = -x
| otherwise = x
which is all the more deceptive, since “otherwise” doesn’t really mean otherwise.
It’s just a synonym for “True“.
Another subtle but common problem arises with definitions like the following, as pointed out by ChrisK in How to make code least strict?:
zip :: [a] -> [b] -> [(a,b)]
zip [] _ = []
zip _ [] = []
zip (x:xs') (y:ys') = (x,y) : zip xs' ys'
These three clauses read like independently true properties for zip.
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?
Continue reading ‘Lazier function definitions by merging partial values’ »