haskelllambda-calculusreductionpartial-applicationweak-head-normal-form

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


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.


Solution

  • 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.