Section. Inefficiency of applicative-order normalisation [nbe-applicative-inefficiency]

The normaliser nf0 can be inefficient for a number of reasons.

First of all, in the case nf0 (App f a) above, nf0 normalises the argument a to a' before applying a' to the function, but it is totally possible that f doesn't use its argument at all, so the effort spent on computing a' is wasted. This problem isn't hard to fix in Haskell: we can make the normalisation of the argument (i.e. the variable a' in nf0) lazy by annotating a' with ~, which is the syntax of Haskell to make let-bindings lazy when Strict is enabled.

Secondly, we normalised the function f as well before substituting the (normalised) argument a', but we still need to re-normalise after substitution, so we normalised the function body twice:

1. when we don't have the argument, and

2. when the argument is instantiated to a'.

This can be inefficient in some situations; for example, consider a term of the form

(\x. x expensiveTm) (\y. M)  -- where y doesn't occur in M

where normalising the function body x expensiveTm is expensive. However, if we know the argument x will be instantiated to the constant function \y. M, the function body becomes (\y. M) expensiveTm, which would enable us to avoid normalising expensiveTm as long as we manage to fix the inefficiency of normalising unused arguments mentioned in the last paragraph.

The last point about why we don't want to fully normalise the function f in fact is another reason why we don't want to normalise the argument a, because in the function body of f, the argument a may be used as a function as well! For example, consider the term

(\y. y (\z. M))  (\x. x ExpensiveTm)

In \y. y (\z. M), the argument y is not unused, but we still don't want to full normalise its concrete argument \x. x ExpensiveTm before substituting it for y, because the argument \x. x ExpensiveTm will be used as a function after substitution.