Why is a built-in function applied to too few arguments considered to be in weak head normal form?

14
votes

The Haskell definition says:

An expression is in weak head normal form (WHNF), if it is either:

  • a constructor (eventually applied to arguments) like True, Just (square 42) or (:) 1
  • a built-in function applied to too few arguments (perhaps none) like (+) 2 or sqrt.
  • or a lambda abstraction \x -> expression.

Why do built-in functions receive special treatment? According to lambda calculus, there is no difference between a partially applied function and any other function, because at the end we have only one argument functions.

2
haskelllambda-calculusreductionpartial-applicationweak-head-normal-form
I took the liberty to edit that Haskell wiki page with an explanation of why this distinction between built-ins and lambdas doesn't matter to semantics. (And also a note about a subtlety with strict constructor fields.) – Ørjan Johansen
BTW that wiki page is not actually part of Haskell's official definition. However the official report doesn't even mention the issue, seemingly preferring to assume readers know denotational semantics... – Ørjan Johansen

2 Answers

22
votes

A normal function applied to an argument, like the following:

(\x y -> x + 1 : y) 1

Can be reduced, to give:

\y -> 1 + 1 : y

In the first expression, the "outermost" thing was an application, so it was not in WHNF. In the second, the outermost thing is a lambda abstraction, so it is in WHNF (even though we could do more reductions inside the function body).

Now lets consider the application of a built-in (primitive) function:

(+) 1

Because this is a built-in, there's no function body in which we can substitute 1 for the first parameter. The evaluator "just knows" how to evaluate fully "saturated" applications of (+), like (+) 1 2. But there's nothing that can be done with a partially applied built-in; all we can do is produce a data structure describing "apply (+) to 1 and wait for one more argument", but that's exactly what the thing we're trying to reduce is. So we do nothing.

Built-ins are special because they're not defined by lambda calculus expressions, so the reduction process can't "see inside" their definition. Thus, unlike normal functions applications, built-in function applications have to be "reduced" by just accumulating arguments until they are fully "saturated" (in which case reduction to WHNF is by running whatever the magic implementation of the built-in is). Unsaturated built-in applications cannot be reduced any further, and so are already in WHNF.

3
votes

Consider

Prelude> let f n = [(+x) | x <- [1..]] !! n
Prelude> let g = f 20000000 :: Int -> Int

g is at this point not in WHNF! You can see this by evaluating, say, g 3, which takes a noticable lag because you need WHNF before you can apply an argument. That's when the list is traversed in search for the right built-in function. But afterwards, this choice is then fixed, g is WHNF (and indeed NF: that's the same for lambdas, perhaps what you meant with your question) and thus any subsequent calls will give a result immediately.