Weak head normal form
An expression is in weak head normal form (WHNF), if it is either:
- a constructor (eventually applied to arguments) like
Just (square 42)or
- a built-in function applied to too few arguments (perhaps none) like
- or a lambda abstraction
\x -> expression.
Note that the arguments do not themselves have to be fully evaluated for an expression to be in weak head normal form; thus, while
square 42 can be reduced to
42 * 42 (which can itself be reduced to a normal form of
Just (square 42) is in WHNF without further evaluation. Similarly,
(+) (2 * 3 * 4) is in WHNF, even though
2 * 3 * 4 could be reduced to the normal form
An exception is the case of a fully applied constructor for a data type with some fields declared as strict; the arguments for these fields then also need to be in WHNF.
The above definition might seem to treat built-in functions differently from functions defined via lambda abstraction. However, the distinction does not matter to semantics. If a lambda abstraction is applied to "too few arguments", then evaluating the application just means substituting arguments for some of the lambda abstraction's variables, which always halts with the result a now-unapplied lambda abstraction.