typed-recursion.rkt

#lang plait

(define-type Type
  [TNum]
  [TFun (arg : Type) (ret : Type)])

(define-type Exp
  [varE (s : Symbol)]
  [numE (n : Number)]
  [letrecE (s : Symbol) (t : Type) (e : Exp) (body : Exp)]
  [letE (s : Symbol) (e : Exp) (body : Exp)]
  [lamE (arg : Symbol) (t : Type) (body : Exp)]
  [appE (e1 : Exp) (e2 : Exp)]
  )

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


(interp : (Exp -> Exp))
(define (interp e)
  (type-case Exp e
    [(varE s) (error 'runtime "unknown symbol")]
    [(numE n) (numE n)]
    [(letE s e body)
     ; run body[s |-> (interp e)]
     (interp (subst body s (interp e)))]
    [(letrecE s t e body)
     ; run (letE s e[s |-> (letrecE s t e s)] body)
     (interp
      (letE s (subst e s (letrecE s t e (varE s)))
            body))]
    [(lamE id typ body) (lamE id typ body)]
    [(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 (lamE-body e1V))
              (id (lamE-arg e1V))
              (argV (interp e2))]
       (interp (subst body id argV)))]
    ))

(define loopy (letrecE 'f (TFun (TNum) (TNum))
                             (lamE 'x (TNum) (appE (varE 'f) (varE 'x))) (appE (varE 'f) (numE 10))))


(define-type-alias TEnv (Hashof Symbol Type))
(define mt-env (hash empty)) ;; "empty environment"


(define (lookup (n : TEnv) (s : Symbol))
  (type-case (Optionof Type) (hash-ref n s)
             [(none) (error 'type-error "unrecognized symbol")]
             [(some v) v]))

(extend : (TEnv Symbol Type -> TEnv))
(define (extend old-env new-name value)
  (hash-set old-env new-name value))


(define (type-of env e)
  (type-case Exp e
             [(varE s) (lookup env s)]
             [(numE n) (TNum)]
             [(lamE arg typ body)
              (TFun typ (type-of (extend env arg typ) body))]
             [(letE id e body)
              (let [(type-e (type-of env e))]
                (type-of (extend env id type-e) body))]
             [(letrecE id t e body)
              (letrec [(extended-tenv (extend env id t))
                       (type-e (type-of extended-tenv e))
                       (type-body (type-of extended-tenv body))]
                ; check that type-e = t
                (if (equal? type-e t)
                    type-body
                    (error 'type-error "invalid recursive type")))]
             [(appE e1 e2)
              (let [(t-e1 (type-of env e1))
                    (t-e2 (type-of env e2))]
                (type-case Type t-e1
                           [(TFun tau1 tau2)
                            (if (equal? tau1 t-e2)
                                tau2
                                (error 'type-error "invalid function call"))]
                           [else (error 'type-error "invalid function call")]))]))



(test (interp (appE (lamE 'x (TNum) (varE 'x)) (numE 10))) (numE 10))
(test (interp (letrecE 's (TNum) (numE 10) (varE 's))) (numE 10))
(test (interp (letrecE 's (TFun (TNum) (TNum)) (lamE 'x (TNum) (varE 'x)) (appE (varE 's) (numE 10)))) (numE 10))