Section. Weak-applicative-order normalisation [nbe-nf1]

Following our plan, let's define a new function wnf1 :: Tm -> Tm for normalising a term to WNF. The way this function works is a bit similar to nf0, if we see an application, we reduce the function and the argument to WNF, and if the WNF of the function is a lambda abstraction, we do a beta-reduction and re-normalise to WNF. The difference from nf0 is that when wnf1 sees a lambda abstraction, it doesn't do anything (whereas nf0 would continue to normalise under the binder).

wnf1 :: Tm -> Tm
wnf1 (App f a) =
  let f' = wnf1 f
      ~a' = wnf1 a
  in case f' of
       Abs b -> wnf1 (betaL b a')
       _ -> App f' a'
wnf1 t = t

Note that the variable a' is annotated with ~, which makes a' lazily evaluated (if b doesn't use its argument, a' = wnf1 a will not be computed). We also need to use a version of beta that is lazy in its second argument. Until someone designs 'strictness polymorphism' and implements it in GHC, we have no choice but to duplicate our beta and subst functions with a ~ annotation in the arguments that we'd like to be lazy:

betaL :: Tm -> Tm -> Tm
betaL b ~a = shift 0 (-1) (substL b 0 (shift 0 1 a))

substL :: Tm -> Int -> Tm -> Tm
substL (Var n)   x ~t = if x == n then t else Var n
substL (App f a) x ~t = App (substL f x t) (substL a x t)
substL (Abs b)   x ~t = Abs (substL b (x + 1) (shift 0 1 t))

Just to check our laziness annotation is working as expected:

-- >>> betaL (Abs (Var 0)) undefined
-- \x0. x0

-- >>> beta (Abs (Var 0)) undefined
-- Prelude.undefined

Our new function for full normalisation then uses wnf1 to compute weak normal forms in the case of a function application:

nf1 :: Tm -> Tm
nf1 (Var v) = Var v
nf1 (Abs b) = Abs (nf1 b)
nf1 (App f a) =
  let f' = wnf1 f
      ~a' = wnf1 a
  in case f' of
       Abs b -> nf1 (betaL b a')
       _ -> App (reify1 f') (reify1 a')

When the weak normal form f' of the function is not a lambda abstraction, we need to turn the weak normal forms f' and a' into (full) normal forms. This is done by the following function that triggers normalisation under lambda abstractions:

reify1 :: Tm -> Tm
reify1 (Var v) = Var v
reify1 (Abs b) = Abs (reify1 (wnf1 b))
reify1 (App f a) = App (reify1 f) (reify1 a)

One thing to notice is that an alternative definition of nf1 is simply:

nf1' :: Tm -> Tm
nf1' = reify1 . wnf1

The explicit definition nf1 above is the fused version of these two functions composed together. The fused version nf1 is slightly more efficient than nf1' because it avoids building the intermediate weak normal form built by wnf1 and consumed by reify1. Deriving the fused normalising function from wnf1 and reify1 is usually easy, so in the rest of this article we will focus on optimising wnf1 and reify1 and define normalisation as their composition.

To see the improvement of our new normaliser nf1 over nf0, let's construct a term (\x. x expensiveTm) (\x. c0) and let expensiveTm be the conjunction of a large number of Church Boolean values of truth.

-- A term that is expensive to normalise
expensiveTm :: Int -> Tm
expensiveTm n = Abs (churchNum n `App` (cAnd `App` cTrue) `App` cTrue)

-- Church encoding of Boolean values
cTrue, cFalse :: Tm
cTrue = Abs (Abs (Var 1))
cFalse = Abs (Abs (Var 0))

-- Conjunction of Boolean values
cAnd :: Tm
cAnd = Abs (Abs (Abs (Abs (Var 3 `App` (Var 2 `App` Var 1 `App` Var 0) `App` Var 0))))

-- `churchNum n` is `cinc` applied to zero `n` times.
churchNum :: Int -> Tm
churchNum n = foldr (\_ r -> cinc `App` r) c0 [1 .. n]

-- This takes a lot of time to compute
-- >>> nf0 $ (Abs (Var 0 `App` expensiveTm 10000)) `App` Abs c0

-- This takes less than a second to compute on my machine
-- >>> nf1 $ (Abs (Var 0 `App` expensiveTm 10000)) `App` Abs c0
-- \x0. \x1. x1

Great, our optimisation worked (at least for this particular term)! We may call the normaliser nf1 weak-applicative-order normalisation with meta-level laziness. Meta-level laziness refers to the fact that function arguments are reduced lazily through the laziness of our meta-language, Haskell.