system-f.rkt

#lang plait

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; an implementation of System F


;;; abstract syntax
(define-type typ
  (funT [arg : typ] [ret : typ])
  (identT [id : Symbol])
  (numT)
  (forallT [id : Symbol] [body : typ]))

(define-type expr
  (identF [id : Symbol])
  (numF [n : Number])
  (lamF [arg : Symbol] [t : typ] [body : expr])
  (appF [e1 : expr] [e2 : expr])
  (tlamF [id : Symbol] [body : expr])
  (tappF [e1 : expr] [t : typ]))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; interpret system-f
;;; erase all types and run it using the lambda calculus interpreter

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; type checker

;;; performs substitution t1[x |-> t2]
(define (tsubst t1 x t2)
  (type-case typ t1
             [(funT arg ret)
              (funT (tsubst arg x t2) (tsubst ret x t2))]
             [(numT) (numT)]
             [(identT id)
              (if (equal? id x)
                  t2
                  (identT id))]
             [(forallT id body)
              ; check for shadowing
              (if (equal? x id)
                  (forallT id body) ; shadowing case, do nothing
                  (forallT id (tsubst body x t2))
                  )]))

;;; compute the DeBruijn indexed version of a term for checking
;;; alpha equivalence. this is a helper function for type-eq?
(debruijn : (typ String -> typ))
(define (debruijn t c)
  (type-case typ t
             [(numT) (numT)]
             [(funT t1 t2)
              (funT (debruijn t1 c) (debruijn t2 c))]
             [(identT x) (identT x)]
             [(forallT id body)
              (let* ([new-name (string-append c "x")]
                     [subst-body (debruijn (tsubst body id (identT (string->symbol new-name)))
                                           new-name)])
                (forallT (string->symbol new-name) subst-body))]
             ))

;;; check if t1 and t2 are equivalent types up to alpha renaming
(define (type-eq? t1 t2)
  (equal? (debruijn t1 "x") (debruijn t2 "x")))

;;; test type-eq?
(test (type-eq? (forallT 'X (identT 'X))
                (forallT 'Y (identT 'Y)))
      #t)

(test (type-eq? (forallT 'X (forallT 'Y (funT (identT 'X) (identT 'Y))))
                (forallT 'Z (forallT 'W (funT (identT 'Z) (identT 'W)))))
      #t)

(test (type-eq? (forallT 'X (forallT 'X (funT (identT 'X) (identT 'X))))
                (forallT 'Y (forallT 'X (funT (identT 'X) (identT 'X)))))
      #t)

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

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

(type-of : (TEnv expr -> typ))
(define (type-of env e)
  (type-case expr e
             [(identF x)
              (type-case (Optionof typ) (hash-ref env x)
                         [(some t) t]
                         [(none) (error 'type "unbound identifier")])]
             [(numF n) (numT)]
             [(lamF id t body)
              (funT t (type-of (extend env id t) body))]
             [(appF e1 e2)
              (let [(t-e1 (type-of env e1))
                    (t-e2 (type-of env e2))]
                (type-case typ t-e1
                           [(funT tau1 tau2)
                            (if (type-eq? tau1 t-e2)
                                tau2
                                (begin
                                  (display tau1)
                                  (display tau2)
                                  (error 'type-error "invalid function call: cannot unify")))]
                           [else (error 'type-error "invalid function call")]))]
             [(tlamF id body)
              (forallT id (type-of env body))]
             [(tappF e t)
              (type-case typ (type-of env e)
                         [(forallT id body)
                          (tsubst body id t)]
                         [else (error 'type "invalid type application")])]))

(define (type-check? e)
  (try
   (begin
     (type-of mt-env e)
     #t)
   (λ () #f)))

; type check the identity function
; ((ΛX.(λx:X.x)) [Num]) 10
(define id (tlamF 'X
                  (lamF 'x (identT 'X) (identF 'x))))
(test (type-check? (appF
                    (tappF id (numT))
                    (numF 10)))
      #t)

; type check self applicataion
; λx:(∀X.X->X). ((x [∀X.X->X]) x)
(define ∀X.X->X (forallT 'X (funT (identT 'X) (identT 'X))))
(test (type-check? (lamF 'x ∀X.X->X
                         (appF (tappF (identF 'x) ∀X.X->X)
                               (identF 'x))))
      #t)