Semantics for de Bruijn levels

Question

There is an exceptionally simple way to embed simply typed lambda calculus with de Bruijn indices in a functional host language (discussed by Carette, Kiselyov & Shan, and by Kiselyov). The construction here, expressed in Haskell, is from Kiselyov's paper:

z :: (a, b) -> a
z (x, _) = x

s :: (a -> b) -> (c, a) -> b
s v (_, h) = v h

lam :: ((a, b) -> c) -> b -> a -> c
lam e h x = e (x, h)

app :: (a -> b -> c) -> (a -> b) -> a -> c
app e1 e2 h = e1 h (e2 h)

eval :: (() -> a) -> a
eval e = e ()

So, for example eval (lam (lam (app z (s z)))) 2 succ evaluates to 3, as our lam expression eval's to the Haskell value \x -> \f -> f x.

This embedding uses de Bruijn indices: to find the binder of a variable, count upward from the variable. I am curious about whether there is an analogous embedding of de Bruijn levels, where to find a variable's binder we count downward. Concretely, \x -> \f -> f x would be represented in such an embedding as lam' (lam' (app' (s' z') z')).

The above embedding uses (as Kiselyov notes) nothing beyond the Hindley-Milner subset of Haskell 2010. It is not obvious to me whether de Bruijn levels can be implemented in such a simple type system. Indeed, it seems quite difficult: the environment tuples built by lam would need to be turned inside-out, or our variables would need to behave differently depending on the depth of the environment tuple. If we only had variables of one type, we could use lists; given that our variables have multiple types, do we require HLists?

======

Late edit to expand on the points in the last paragraph...

One way to think about de Bruijn levels is that lam append's (rather than cons's) to the environment. This way, from the perspective of a variable, the head of the environment (in a closed term) will always correspond to the highest lam. In terms of homogeneous lists:

zL :: [a] -> a
zL (x:h) = x

sL :: ([a] -> b) -> [a] -> b
sL v (_:h) = v h

lamL :: ([a] -> b) -> [a] -> a -> b
lamL e h x = e (h++[x])

appL :: ([a] -> b -> c) -> ([a] -> b) -> [a] -> c
appL e1 e2 h = e1 h (e2 h)

evalL :: ([a] -> b) -> b
evalL e = e []

This models de Bruijn levels, in the sense that lamL (lamL (sL zL)) [] 2 3 evaluates to 3. But it isn't simply typed lambda calculus, since it only allows variables of one type -- e.g., lamL (lamL (appL (sL zL) zL)) is a type error.

To allow variables of multiple types, we can use HList:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeOperators #-}

import Data.HList

zH :: HList (a ': b) -> a
zH (HCons x h) = x

sH :: (HList a -> b) -> HList (c ': a) -> b
sH v (HCons _ h) = v h

lamH :: HAppendList a '[b] =>
        (HList (HAppendListR a '[b]) -> c) -> HList a -> b -> c
lamH e h x = e (hAppendList h (HCons x HNil))

appH :: (HList a -> b -> c) -> (HList a -> b) -> HList a -> c
appH e1 e2 h = e1 h (e2 h)

Then lamH (lamH (appH (sH zH) zH)) HNil 2 succ evaluates to 3, as desired. But this is a significantly heavier-duty approach than the embedding we began with. Do de Bruijn levels require all this artillery?

Answer 1

Here is a provisional answer. The de Bruijn index and level of a bound variable sum up to the number of enclosing lambdas: $i+l=n_\lambda$. Since the index can be recovered from the level by subtraction, levels can be implemented as 'predecessor' indices p:

z :: (a, b) -> a
z (x, _) = x

s :: (a -> b) -> (c, a) -> b
s v (_, h) = v h

-- ^^^ as above

p :: (((), a) -> b) -> a -> b
p v h = v ((), h)

-- (p . s) v == v

app :: (a -> b -> c -> d) -> (a -> b -> c) -> a -> b -> d
app e1 e2 v h = e1 v h (e2 v h)

-- app manages an extra bit of context: the number of enclosing lambdas

lam :: (((a, b) -> c) -> (d, e) -> f) ->
       (b -> c) -> e -> d -> f
lam e v h x = e (s v) (x, h)

-- lam increments that context

eval :: (((a, env) -> a) -> () -> b) -> b
eval t = t z ()

-- evaluating closed terms...the starting context is z

This seems reasonable, and terms with just one variable (and arbitrary numbers of lambdas) behave as expected. But the type-checker chokes on terms with distinct variables -- e.g., app (p . p) p, our representation of the open term $21$, gives an 'infinite type' error.

To see why, let's consider a concrete evaluated closed term, eval $ lam (lam (app (p . p) p)). If you churn through the reductions by hand, eventually you end up with the following:

\x f -> s (s z) ((), ((), (f, (x, ())))) (s (s z) ((), (f, (x, ()))))

If both occurrences of s (s z) are polymorphic, this appears well-typed, and can be further simplified, to \x f -> f x, as desired (well, our de Bruijn level representation of this term is $\lambda\lambda 21$... close enough!). The problem, it seems, is that the Haskell type-checker insists that the two occurrences of s (s z) have the same monomorphic type, and therefore seems related to the absence of 'first-class polymorphism' in Haskell.

It is not obvious to me how 'deep' the problem here goes -- whether it can be massaged in Haskell; and if not, whether the implementation here can be coherently stated in, e.g., System F (Hindley-Milner seems out due to the need for first-class polymorphism).