Archive for 11th September 2010

## Lazier functional programming, part 1

This post is inspired by a delightful insight from Luke Palmer. I’ll begin with some motivation, and then propose a puzzle.

Consider the following definition of our familiar conditional:

```ifThenElse :: Bool → a → a → a
ifThenElse True  t f = t
ifThenElse False t f = f```

In a strict language, where there are only two boolean values, these two clauses have a straightforward reading. (The reading is less straightforward when patterns overlap, as mentioned in Lazier function definitions by merging partial values.) In a non-strict language like Haskell, there are three distinct boolean values, not two. Besides `True` and `False`, `Bool` also has a value ⊥, pronounced “bottom” for being at the bottom of the information ordering. For an illustration and explanation of information ordering, see Merging partial values.

Note: In Haskell code, ⊥ is sometimes denoted by “`undefined`“, which can be confusing, because the meaning is defined precisely. There are many other ways to denote ⊥ in Haskell, and it is impossible to determine whether or not an arbitrary Haskell expression denotes ⊥. I’ll generally use “⊥” in place of “`undefined`” in this post, as well as for the corresponding semantic value.

The two-clause definition above only addresses two of the three possible boolean values explicitly. What, if anything, does it say indirectly about the meaning of an application like “`ifThenElse ⊥ 3 5`“?

The Haskell language standard gives an operational answer to this question. Clauses are examined, using pattern matching to select a clause and instantiate that clause’s variables. In case more than one clause matches, the earlier one is chosen.

Pattern matching has three possible outcomes:

• A single substitution, providing variable bindings that specialize the patterns in a clause’s left-hand side (LHS) to coincide with the actual call. The matching uses semantic, not syntactic, equality and can require forcing evaluation of previously unevaluated thunks (delayed computations).
• Proof of the nonexistence of such a substitution.
• Neither conclusion, due to an error or nontermination during evaluation.

In this example, the effort to match `True` against ⊥ leads to the third outcome. For Haskell as currently defined, the result of the application in such a case is then defined to be ⊥ also. Which is to say that `ifThenElse` is strict (in its first argument).

So strictness is the Haskell answer, but is it really the answer we want? Are there alternatives that might better fit the spirit of non-strict functional programming?

Continue reading ‘Lazier functional programming, part 1’ »