stlc.rkt

(define (synthesize-type env e)
  (match e
    ;; Literals
    [(? integer? i) 'int]
    [(? boolean? b) 'bool]
    ;; Look up a type variable in an environment
    [(? symbol? x) (hash-ref env x)]
    ;; Lambda w/ annotation
    [`(lambda (,x : ,A) ,e)
     ;; I know the type is A -> B, where B is the type of e when I
     ;; assume the typing environment env [ x ↦ A ]
     (define B (synthesize-type (hash-set env x A) e))
     `(,A -> ,B)]
    ;; Arbitrary expression
    [`(,e : ,t)
     (let ([e-t (synthesize-type env e)])
       (if (equal? e-t t)
           t
           (error (format "types ~a and ~a are not equal" t e-t))))]
    ;; Application
    [`(,e1 ,e2)
     (match (synthesize-type env e1)
       ;; MUST be an arrow type; otherwise we are trying to call
       ;; something that isn't a function! This is a type error.
       [`(,A -> ,B)
        ;; now the type of e2 has to match A
        (let ([e2-t (synthesize-type env e2)])
          (if (equal? e2-t A)
              ;; we return type B
              B
              ;; type error!
              (error (format "actual input type ~a does not match expected input type ~a" e2-t A))))]
       [_ (error "not an arrow type")])]))