What is Weak Head Normal Form?

Question

What does Weak Head Normal Form (WHNF) mean? What does Head Normal form (HNF) and Normal Form (NF) mean?

The familiar seq function evaluates an expression to what we call head normal form (abbreviated HNF). It stops once it reaches the outermost constructor (the "head"). This is distinct from normal form (NF), in which an expression is completely evaluated.

You will also hear Haskell programmers refer to weak head normal form (WHNF). For normal data, weak head normal form is the same as head normal form. The difference only arises for functions, and is too abstruse to concern us here.

I have read a few resources and definitions (Haskell Wiki and Haskell Mail List and Free Dictionary) but I don't get it. Can someone perhaps give an example or provide a layman definition?

I am guessing it would be similar to:

WHNF = thunk : thunk

HNF = 0 : thunk 

NF = 0 : 1 : 2 : 3 : []

How do seq and ($!) relate to WHNF and HNF?

Update

I am still confused. I know some of the answers say to ignore HNF. From reading the various definitions it seems that there is no difference between regular data in WHNF and HNF. However, it does seem like there is a difference when it comes to a function. If there was no difference, why is seq necessary for foldl'?

Another point of confusion is from the Haskell Wiki, which states that seq reduces to WHNF, and will do nothing to the following example. Then they say that they have to use seq to force the evaluation. Is that not forcing it to HNF?

Common newbie stack overflowing code:
myAverage = uncurry (/) . foldl' (\(acc, len) x -> (acc+x, len+1)) (0,0)
People who understand seq and weak head normal form (whnf) can immediately understand what goes wrong here. (acc+x, len+1) is already in whnf, so the seq (in the definition of foldl'), which reduces a value to whnf, does nothing to this. This code will build up thunks just like the original foldl example, they'll just be inside a tuple. The solution is just to force the components of the tuple, e.g.
myAverage = uncurry (/) . foldl' 
          (\(acc, len) x -> acc `seq` len `seq` (acc+x, len+1)) (0,0)

-Haskell Wiki on Stackoverflow

user_7806457 · Answer

In an implementation of graph reduction, lazy evaluation to HNF forces you to deal with the name capture problem of lambda calculus, whereas lazy evaluation to WHNF lets you avoid it.

This is explained in Chapter 11 of The Implementation of Functional Programming Languages by Simon Peyton Jones.

user_1888743 · Answer

I realize this is an old question, but here is an explicit mathematical definition of WHNF, HNF, and NF. In the pure lambda calculus:

A term is in NF if it is of the form
```
λ x1. λ x2. ... λ xn. (x t1 t2 ... tm)
```
where x is a variable, and t1, t2, ..., tm are in NF.
A term is in HNF if it is of the form
```
λ x1. λ x2. ... λ xn. (x e1 e2 ... em)
```
where x is a variable, and e1, e2, ..., em are arbitrary terms.
A term is in WHNF if it is either a lambda term λ x. e for any term e or if it is of the form
```
x e1 e2 ... em
```
where x is a variable and e1, e2, ..., em are arbitrary terms.

Now consider a programming language with constructors a,b,c... of arity na, nb, nc..., which means that whenever t1, t2, ..., tm are in NF, then the term a t1 t2 ... tm where m = na is a redex and can be evaluated. For example, the addition constructor + in Haskell has arity 2, because it only evaluates when it is given two arguments in normal form (in this case integers, which can themselves be considered as nullary constructors).

A term is in NF if it is of the form
```
λ x1. λ x2. ... λ xn. (x t1 t2 ... tm)
```
where x is either a variable or a constructor of arity n with m < n, and t1, t2, ..., tm are in NF.
A term is in HNF if it is of the form
```
λ x1. λ x2. ... λ xn. (x e1 e2 ... em)
```
where x is either a variable or a constructor of arity n, and e1, e2, ... em are arbitrary terms so long as the first n arguments are not all in NF.
A term is in WHNF if it is either a lambda term λ x. e for any term e or if it is of the form
```
x e1 e2 ... em
```
where x is either a variable or a constructor of arity n, and e1, e2, ... em are arbitrary terms so long as the first n arguments are not all in NF.

In particular, any term in NF is in HNF, and any term in HNF is in WHNF, but not conversely.

user_7194773 · Answer

Head normal form means there is no head redex

(λx.((λy.y+x)b))b

Reduces to: R, for redex (and yes there's another redex inside it but this is irrelevant). This is a head redex because it's the leftmost redex (the only redex), and there are no lambda terms before it (variables or lambda expressions (applications or abstractions)), only 0 to n abstractors (if R is a redex (λx.A)B the abstractor of R is λx), in this case 0.

Because there's a head redex it is not in HNF and it is therefore also not in NF because there's a redex.

WHNF means that it is a lambda abstraction or in HNF. The above is not in HNF and it is not a lambda abstraction, but an application, and is therefore not in WHNF.

λx.((λy.y+x)b)b is in WHNF

It is a lambda abstraction, but not in HNF because there is a head λx.Rb

Reduce to λx.((b+x)b). There is no redex therefore it is in normal form.

Consider λx.((λy.zyx)b), it simplifies to λx.R, so it is not in HNF. λx.(k(λy.zyx)b) simplifies to λx.kR therefore it is in HNF but not NF.

All NF are in HNF and WHNF. All HNF are WHNF.

What is Weak Head Normal Form?

Update

9 Answers