Normalization by evaluation -- aka magic

nbe.rkt

#lang typed/racket
(define-type Term (U VAR LAM APP))
(struct: VAR ([x : String]) #:transparent)
(struct: LAM ([x : String] [m0 : Term]) #:transparent)
(struct: APP ([m1 : Term] [m2 : Term]) #:transparent)

(define-type Sem (U TM FUN))
(struct: TM ([l : (Integer -> Term)]))
(struct: FUN ([f : ((-> Sem) -> Sem)]))

(define: (down [s : Sem] [n : Integer]) : Term
  (match s
    [(TM l) (l n)]
    [(FUN f) 
     (LAM (format "g~a" n)
          (down (f (λ () (TM (λ (n*) (VAR (format "g~a" n)))))) (add1 n)))]))

(define: (eval [m : Term] [ρ : (String -> Sem)]) : Sem
  (match m
    [(VAR x) (ρ x)]
    [(LAM x m0) 
     (FUN (λ (d) (eval m0 (λ (x*) (if (string=? x x*) (d) (ρ x*))))))]
    [(APP m1 m2) 
     (match (eval m1 ρ)
       [(TM l) (TM (λ (n) (APP (l n) (down (eval m2 ρ) n))))]
       [(FUN f) (f (λ () (eval m2 ρ)))])]))

(define: (norm [m : Term]) : Term
  (down (eval m (λ (x) (TM (λ (n) (VAR x))))) 0))

(norm (LAM "z"
           (APP (LAM "x" (VAR "x"))
                (LAM "y" (VAR "y")))))