An implementation of the lambda calculus via substitution

lambda-subst.rkt

#lang plait

; interpreter for lambda calculus with numbers
(define-type LExp
  [varE (s : Symbol)]
  [numE (n : Number)]
  [lamE (x : Symbol) (body : LExp)]
  [appE (e : LExp) (arg : LExp)])

(define-type Value
  [funV (arg : Symbol) (body : LExp)]
  [numV (n : Number)])

(define (get-arg v)
  (type-case Value v
    [(funV arg body) arg]
    [else (error 'runtime "invalid")]))

(define (get-body v)
  (type-case Value v
    [(funV arg body) body]
    [else (error 'runtime "invalid")]))

; perform e1[x |-> e2]
(subst : (LExp Symbol LExp -> LExp))
(define (subst e1 x e2)
  (type-case LExp e1
    [(varE s) (if (symbol=? s x) 
                  e2 
                  (varE s))]
    [(numE n) (numE n)]
    [(lamE id body) 
    (if (symbol=? x id) 
      (lamE id body)              ; shadowing case
      (lamE id (subst body x e2)))]
    [(appE e1App e2App) 
     (appE (subst e1App x e2) 
           (subst e2App x e2))]))

(define (interp e)
  (type-case LExp e
    [(varE s) (error 'runtime "unbound symbol")]
    [(lamE id body) (funV id body)]
    [(numE n) (numV n)]
    [(appE e1 e2)
     ; run e1 to get (lambda (id) body)
     ; run e2 to get a value argV
     ; run body[id |-> v]
     (letrec [(e1V (interp e1))
              (body (get-body e1V))
              (id (get-arg e1V))
              (argV (interp e2))]
       (type-case Value argV
         [(funV argId argBody)
          (interp (subst body id (lamE argId argBody)))]
         [(numV n)
          (interp (subst body id (numE n)))]))]))

(test (interp (appE (lamE 'x (varE 'x)) (numE 10))) (numV 10))
(test (interp (appE (lamE 'x (varE 'x)) (lamE 'y (varE 'y)))) (funV 'y (varE 'y)))
(test (interp (appE (lamE 'x (lamE 'x (varE 'x))) (numE 10))) (funV 'x (varE 'x)))