Section. Preliminary setup [nbe-setup]

In this article, we will use Haskell as our meta-language. Haskell is a lazy language. Although laziness never harms the time complexity of programs (and can sometimes make asymptotic improvements!), thinking about the running cost of lazy programs is a nightmare compared to strict programs. Therefore we will turn on the Strict extension of GHC, which makes laziness an opt-in feature (by decorating binding variables or data fields with ~) rather than the default behaviour. Enabling Strict also makes porting the code in this article to other strict programming languages (say, C or OCaml) a lot easier, as there is no implicit laziness that our algorithms secretly rely on.

{-# LANGUAGE Strict #-}

-- Some other quality-of-life GHC extensions
{-# LANGUAGE InstanceSigs, PatternSynonyms, ViewPatterns, RecordWildCards #-}

module NbE where

-- In the last section of this article we will need mutable arrays.
import Data.Array.MArray
import Data.Array.ST
import GHC.ST

Note however, Strict doesn't change the behaviour of existing definitions from other modules, such as those from Prelude, so the built-in list type [a] remains to be lazy lists of lazy payloads.

type LazyList a = [a]

If we want strict lists, we can define our own data List a = Nil | Cons a (List a) in this module (or any other module with Strict enabled).

Since our topic is about the efficiency rather than the correctness of NbE, we will simply use untyped lambda calculus as our object language in this article. Consequently, our normalisers will not terminate on input programs that do not have a normal form -- we don't care. We are only interested in programs that do have normal forms.

We will use de Bruijn indices to represent variables formally (but we will still use named variable in our informal discussion). The following code is some basic definitions for the syntax of lambda calculus using de Bruijn indices. In this article I will assume that you are already familiar with them -- if not, try search 'tutorial of lambda calculus' or 'de Bruijn indices' online and you can find a lot of resources, such as this and this if you prefer code over maths. Otherwise you can skim over the definitions and go to the next section; nothing unusual here.

data Tm = Var Int | App Tm Tm | Abs Tm deriving Eq

infixl `App`

-- `subst s x t` substitutes `t` for every occurrence of `x` in `s`.
subst :: Tm -> Int -> Tm -> Tm
subst (Var n)   x t = if x == n then t else Var n
subst (App f a) x t = App (subst f x t) (subst a x t)
subst (Abs b)   x t = Abs (subst b (x + 1) (shift 0 1 t))

-- `shift x i t` increments all variables in `t` that are `>= x` by `i`.
shift :: Int -> Int -> Tm -> Tm
shift x 0 t = t
shift x i (Var n) = if n >= x then Var (n + i) else Var n
shift x i (App f a) = App (shift x i f) (shift x i a)
shift x i (Abs b) = Abs (shift (x+1) i b)

-- `beta b a` stands for beta-reduction for `(\. b) a` (substituting `a` for
-- variable of de Bruijn index 0 in `b`). Because `b` lives in one level deeper
-- than `a`, we use `shift 0 1` to bring `a` to the same level of `b`.
-- Also after substitution, we want to remove the lambda abstraction, so we
-- need to do `shift 0 (-1)` for the result of substitution.
beta :: Tm -> Tm -> Tm
beta b a = shift 0 (-1) (subst b 0 (shift 0 1 a))

-- `fv t` computes the biggest de Bruijn index of all free variables in a term
-- `t`. If a term has no free variables, the result is -1.
fv :: Tm -> Int
fv (Var n) = n
fv (Abs b) = max (-1) (fv b - 1)
fv (App f a) = max (fv f) (fv a)

-- `showTm ns t` computes the string representation of a term and the precedence
-- of the outermost syntactic constructor. The argument `ns` is the list of
-- names for the free variables.
showTm :: Int -> Tm -> (String, Int)
showTm ns (Var n) = ("x" ++ show (ns - n - 1), 100)
showTm ns (Abs b) =
  let (s, _) = showTm (ns + 1) b
  in ("\\x" ++ show ns ++ ". " ++ s, 0)
showTm ns (App f a) =
  let (s1, p1) = showTm ns f
      (s2, p2) = showTm ns a
      s1' = if p1 >= 50 then s1 else "(" ++ s1 ++ ")"
      s2' = if p2 > 50  then s2 else "(" ++ s2 ++ ")"
  in (s1' ++ " " ++ s2', 50)

instance Show Tm where
  show t = let n = fv t in fst (showTm (n+1) t)

-- >>> Abs (Var 0 `App` Var 0)
-- \x0. x0 x0

-- >>> Abs (Var 0 `App` Var 0) `App` (Abs (Var 0))
-- (\x0. x0 x0) (\x0. x0)

-- >>> Abs (Var 0 `App` Var 0) `App` (Abs (Var 0)) `App` (Abs (Var 0))
-- (\x0. x0 x0) (\x0. x0) (\x0. x0)

-- >>> Abs (Var 0 `App` Var 0) `App` (Abs (Abs (Var 1)) `App` Abs (Var 0))
-- (\x0. x0 x0) ((\x0. \x1. x0) (\x0. x0))