Section. NbE with lazy shifting of de Bruijn indices [nbe-nf6]

Very similar to the example of Tree' that we used earlier to demonstrate lazy tagging on trees, we will need lists storing lazy tags that represent shift offsets that are logically applied to the de Bruijn indices. For this we define a type SList a of lists with lazy tags of shift indices. We will use this type to replace LazyList a that we used before to represent lazy substitutions.

data SList a = Nil | Cons_ Int ~a (SList a) deriving Show

The type of values (weak normal forms with lazy substitutions) is the same as before, except that we now use SList:

data Val6 = Closure6 Tm Subst6 | Spine6 Int (SList Val6)
type Subst6 = SList Val6

We will have more than one types that support index shifting, so this time let's define a typeclass with a single member function shift0 i v that shifts all de Bruijn indices in v by i. (We won't need the general case shift x i v of shifting de Bruijn indices greater than or equal to x by i.)

class Shift0 a where
  shift0 :: Int -> a -> a

Shifting a list with lazy tags only remembers the offset i lazily without actually performing the shifting operations. It is clearly O(1). In contrast, previously in shift0List we needed to map over the list to shift every element.

instance Shift0 a => Shift0 (SList a) where
  shift0 :: Shift0 a => Int -> SList a -> SList a
  shift0 i Nil = Nil
  shift0 i (Cons_ j v vs) = Cons_ (i + j) v vs

Shifting a value is easy too. For a closure, we use shift0 for SList to shift the lazy substitution, and for a spine, we shift the variable immediately and use shift0 for SList to shift the list of arguments.

instance Shift0 Val6 where
  shift0 :: Int -> Val6 -> Val6
  shift0 i (Closure6 b sub) = Closure6 b (shift0 i sub)
  shift0 i (Spine6 j as) = Spine6 (i + j) (shift0 i as)

To make our life later easier, this time let's use pattern synonyms of Haskell to make lazy tagging transparent. The type ListView a is the functor that captures the shape of a list (with lazy payloads but strict structure).

data ListView a x = NilView | ConsView ~a x

A SList a is logically a list of a viewed from the following function, where we push the lazy tag down (c.f. the push function in the earlier example of lazy tagging for binary trees):

viewSList :: Shift0 a => SList a -> ListView a (SList a)
viewSList Nil = NilView
viewSList (Cons_ i v vs)
  | i /= 0 = ConsView (shift0 i v) (shift0 i vs)
  | otherwise = ConsView v vs

Now we define a pattern synonym Cons v vs: when we use the pattern Cons v vs to match again an element as :: SList a, it will automatically applies viewSList to as. And when we use Cons v vs to construct an element of type SList a, the lazy tag is going to be set to 0. Using this pattern, the user interface of SList will be exactly the same as an ordinary list.

pattern Cons :: Shift0 a => a -> SList a -> SList a
pattern Cons v vs <- (viewSList -> ConsView v vs) where
  Cons ~v vs = Cons_ 0 v vs

We will need some standard list-processing function for SList in the future, but they are easy:

lookupSL :: Shift0 a => SList a -> Int -> a
lookupSL Nil _ = error "index out of range"
lookupSL (Cons v vs) i = if i == 0 then v else lookupSL vs (i-1)

foldrSL :: Shift0 a => (a -> r -> r) -> r -> SList a -> r
foldrSL f r Nil = r
foldrSL f r (Cons v vs) = f v (foldrSL f r vs)

dropSL :: Shift0 a => Int -> SList a -> SList a
dropSL 0 as = as
dropSL i Nil = Nil
dropSL i (Cons _ as) = dropSL (i-1) as

Our new weak normaliser is the same as wnf3 except that it uses the new data type Val6 for values:

wnf6 :: Tm -> Subst6 -> Val6
wnf6 (Var n) sub = lookupSL sub n
wnf6 (Abs b) sub = Closure6 b sub
wnf6 (App f a) sub =
  let f' = wnf6 f sub
      ~a' = wnf6 a sub
  in case f' of
       Closure6 b sub' -> wnf6 b (Cons a' sub')
       Spine6 v as -> Spine6 v (Cons a' as)

Similarly reify6 is the same as reify2 except it uses the new data type Val6:

reify6 :: Val6 -> Tm
reify6 (Closure6 t sub) = Abs (reify6 (wnf6 t (Cons (Spine6 0 Nil) (shift0 1 sub))))
reify6 (Spine6 v as) = foldrSL (\a r -> r `App` reify6 a) (Var v) as

The function reflect6 is the same as reflect2:

reflect6 :: Int -> Subst6
reflect6 n = foldr (\x rs -> Cons (Spine6 x Nil) rs) Nil [0 .. n]

These give us the new normaliser nf6, which is defunctional NbE with de Bruijn indices (rather than levels). Because of lazy tagging, the shift operations have O(1) complexity, so this version has the same asymptotic complexity as nf5 (the version using de Bruijn levels) on all input, but of course the constant factor nf6 is slightly bigger than nf6.

nf6 :: Tm -> Tm
nf6 t = let n = fv t
        in reify6 (wnf6 t (reflect6 n))

-- >>> nf6 ((cmul `App` c2 `App` (cinc `App` c2)) `App` Var 0 `App` Var 1)
-- x1 (x1 (x1 (x1 (x1 (x1 x0)))))

-- >>> nf6 (cmul `App` c2 `App` (cinc `App` c2))
-- \x0. \x1. x0 (x0 (x0 (x0 (x0 (x0 x1)))))