NOTE: Practical issue in de Bruijn indices

What's the order of indices? It means we have two choices

1. converts λy.λx.x to λλ1
2. converts λy.λx.x to λλ0

and the second one is better in practice! Because with this encoding, we can work with prepending-list better.

Let's see how this works, first, we need a conversion from surface/concrete syntax to our core form.

(: depth : Sexp -> Nonnegative-Integer)
(define (depth t)
  (match t
    [`(λ (,x) ,body) (add1 (depth body))]
    [`(,f ,a) (max (depth f) (depth a))]
    [else 0]))
(: convert : (->* (Sexp) ((Immutable-HashTable Symbol Nonnegative-Integer))
                  term))
(define (convert t [name->index (make-immutable-hash '())])
  (match t
    [`(λ (,x) ,body)
     (S.lam (convert body (hash-set name->index (cast x Symbol) (depth body))))]
    [`(,t1 ,t2) (S.app (convert t1 name->index) (convert t2 name->index))]
    [x (S.var (hash-ref name->index (cast x Symbol)))]))

This is boring, anyway just record how depth we go that far and refer them back for variables.

1. variable case: we use a helper function =proj=(stands for projection in environment). I will go back to this core function later.

2. application case:

   1. evaluate function to get the value of function.
   2. evaluate argument to get the value of argument.

   Then we have two cases.

   1. value of lambda case: apply lift host-lambda to get result
   2. Not a lambda: prepare a stuck application form.
3. lambda case: create a host-lambda, which will evaluate its body(binder) with extended environment!

(: eval : Env Term -> Val)
(define (eval env t)
  (match t
    [(S.var i) (proj env i)]
    [(S.app t u)
     (let ([t- (eval env t)]
           [u- (eval env u)])
       (match t-
         [(V.lam f) (f u-)]
         [else (V.app t- u-)]))]
    [(S.lam binder)
     (V.lam (λ (u) (eval (cons u env) binder)))]))

Here, since environment is prepended, we can simply count down the counter recorded in the variable. When the counter is zero, the value is what we are looking for, or it's a stuck variable.

(define (proj env i)
  (match env
    ; returns a stuck since we don't always have value in environment in lambda calculus
    [null (V.var i)]
    [(cons v env) (if (= i 0) v (proj env (sub1 i)))]))