Semantics for de Bruijn levels
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) -&gt; a
z (x, _) = x

s :: (a -&gt; b) -&gt; (c, a) -&gt; b
s v (_, h) = v h

-- ^^^ as above

p :: (((), a) -&gt; b) -&gt; a -&gt; b
p v h = v ((), h)

-- (p . s) v == v

app :: (a -&gt; b -&gt; c -&gt; d) -&gt; (a -&gt; b -&gt; c) -&gt; a -&gt; b -&gt; 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) -&gt; c) -&gt; (d, e) -&gt; f) -&gt;
       (b -&gt; c) -&gt; e -&gt; d -&gt; f
lam e v h x = e (s v) (x, h)

-- lam increments that context

eval :: (((a, env) -&gt; a) -&gt; () -&gt; b) -&gt; 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 -&gt; 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 -&gt; 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).