## 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:xs` equals `x` plus the sum of the `xs`.

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’ »

## Merging partial values

Last year I stumbled across a simple representation for partial information about values, and wrote about it in two posts, A type for partial values and Implementing a type for partial values. Of particular interest is the ability to combine two partial values into one, combining the information present in each one.

More recently, I played with unambiguous choice, described in the previous post.

This post combines these two ideas. It describes how to work with partial values in Haskell natively, i.e., without using any special representation and without the use restrictions of unambiguous choice. I got inspired to try removing those restrictions during stimulating discussions with Thomas Davie, Russell O’Connor others in the #haskell gang.