DBL.lhs

The de Bruijn index and level of a bound variable sum up to the number of
enclosing lambdas: i+l=n. 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).

The following works well, but `depth` must be supplied by the user. If depth
is abstracted over, is forced to be monormorphic type, and won't typecheck.

> lam' e     = \h x -> e (x,h)
> app' e1 e2 = \h -> e1 h (e2 h)

> eval' t    = t ()

> t1 = let depth = s (s z)
>      in lam' (lam' (app' (p (p depth)) (p depth)))

> -- if depth < lambdas, type error
> -- if depth > lambdas, open term, reflected in type