fyusuf-a
fyusuf-a

Reputation: 255

What is strictness?

In Haskell, I try to understand the notion of strictness. I understand that

const x y = x

is strict on the first argument but not on the second. But is

 ifFun pred cons alt = if pred then cons else alt

strict? It is strict on the first argument. I understand that the fact that cons and alt are evaluated depending on the value of pred. Does that mean the function is not strict on those arguments?

Upvotes: 1

Views: 326

Answers (1)

Daniel Wagner
Daniel Wagner

Reputation: 152707

"Strict" is one of those words that has a precise technical meaning that has been coopted by the community to mean something a bit less formal. Here's the technical definition.

Function f is strict if f ⊥ = ⊥.

Here ⊥ is the standard symbol for an undefined computation; generally in denotational semantics there is just one and all undefined computations are indistinguishable from each other, but in Haskell as a concession to practicality we have many different kinds that can be distinguished: exceptions, infinite loops, pattern match failures, and so on. For the purposes of this answer, we'll consider them all equal.

Let's ask if const is strict. We have

const = \x -> \y -> x

hence

const ⊥ = \y -> ⊥ ≠ ⊥

and therefore const is not strict. But, oh, we've lost some very important communication power here! There is a good sense in which, when applied to undefined behavior, const doesn't behave well. So many people will say "strict in the nth argument" and we'll pretty much understand what they mean. It isn't obvious how to define what they mean formally, but a half-decent first stab at it goes something like this:

If function f has m arguments, then it is strict in the nth argument for some nm when ∀ a1, ..., am. f a1 a2 ... a(n-1) ⊥ a(n+1) ... am = ⊥.

(Aside: why isn't this quite right? For many functions -- including const -- we can't statically know how many arguments it has. Although const looks like it might be a two-argument function, const id () () is perfectly well typed and applies const to three arguments.)

Now we can say something like "const is strict on its first argument" and have it mean what we want it to mean (provided, as above, that const actually is a two-argument function), because ∀y. const ⊥ y = ⊥ does indeed hold.

We now also have the tools to address your question about ifFun, namely: is ifFun strict on its second argument? That is, can we cook up pred and alt such that

ifFun pred ⊥ alt ≠ ⊥ -- ?

I think it's clear we can do so, since:

ifFun False ⊥ () = if False then ⊥ else () = () ≠ ⊥

A similar argument shows that ifFun is "not strict on its third argument" in the popular understanding of this phrase (again modulo the provisos discussed above), but is "strict on its first argument".

Upvotes: 7

Related Questions