typecheck.scm

   1 (load "ast.scm")
   2                                         ; ('a, ('b, 'a))
   3 (define (env-lookup env n)
   4   (if (null? env) (error #f "empty env")                        ; it's a type equality
   5       (if (eq? (caar env) n)
   6           (cdar env)
   7           (env-lookup (cdr env) n))))
   8
   9 (define (env-insert env n t)
  10   (cons (cons n t) env))
  11
  12 (define abs-arg cadr)
  13
  14 (define cur-tvar 0)
  15 (define (fresh-tvar)
  16   (begin
  17     (set! cur-tvar (+ cur-tvar 1))
  18     (string->symbol
  19      (string-append "t" (number->string (- cur-tvar 1))))))
  20
  21 (define (last xs)
  22   (if (null? (cdr xs))
  23       (car xs)
  24       (last (cdr xs))))
  25
  26
  27 (define (normalize prog) ; (+ a b) -> ((+ a) b)
  28   (cond
  29    ((lambda? prog) (list 'lambda (lambda-arg prog) (normalize (lambda-body prog))))
  30    ((app? prog)
  31     (if (null? (cddr prog))
  32         (cons (normalize (car prog)) (normalize (cdr prog))) ; (f a)
  33         (normalize (cons (cons (car prog) (list (cadr prog))) (cddr prog))))) ; (f a b)
  34    ((let? prog)
  35     (append (list 'let
  36                   (map (lambda (x) (cons (car x) (normalize (cdr x))))
  37                        (let-bindings prog)))
  38             (map normalize (let-body prog))))
  39    (else prog)))
  40
  41
  42 (define (typecheck prog)
  43   (define (check env x)
  44     ;; (display "check: ")
  45     ;; (display x)
  46     ;; (display "\n")
  47     (let
  48         ((res
  49           (cond
  50            ((integer? x) (list '() 'int))
  51            ((boolean? x) (list '() 'bool))
  52            ((eq? x 'inc) (list '() '(abs int int)))
  53            ((eq? x '+)   (list '() '(abs int (abs int int))))
  54            ((symbol? x) (list '() (env-lookup env x)))
  55
  56            ((let? x)
  57             (let ((new-env (fold-left
  58                             (lambda (acc bind)
  59                               (let ((t (check
  60                                         (env-insert acc (car bind) (fresh-tvar))
  61                                         (cadr bind))))
  62                                 (env-insert acc (car bind) (cadr t))))
  63                             env (let-bindings x))))
  64               (check new-env (last (let-body x)))))
  65
  66
  67            ((lambda? x)
  68             (let* ((new-env (cons (cons (lambda-arg x) (fresh-tvar)) env))
  69                    (body-type-res (check new-env (lambda-body x)))
  70                    (subd-env (substitute-env (car body-type-res) new-env)))
  71               ;; (display "lambda: ")
  72               ;; (display body-type-res)
  73               ;; (display "\n")
  74               ;; (display subd-env)
  75               ;; (display "\n")
  76               (list (car body-type-res)
  77                     (list 'abs
  78                           (env-lookup subd-env (lambda-arg x))
  79                           (cadr body-type-res)))))
  80
  81            ((app? x) ; (f a)
  82             (let* ((arg-type-res (check env (cadr x)))
  83                    (arg-type (cadr arg-type-res))
  84                    (func-type-res (check env (car x)))
  85                    (func-type (cadr func-type-res))
  86
  87                                         ; f ~ a -> t0
  88                    (func-c (unify func-type
  89                                   (list 'abs
  90                                         arg-type
  91                                         (fresh-tvar))))
  92                    (cs (append func-c (car arg-type-res) (car func-type-res)))
  93
  94                    (resolved-func-type (substitute cs func-type))
  95                    (resolved-return-type (caddr resolved-func-type)))
  96               ;; (display "app:\n")
  97               ;; (display cs)
  98               ;; (display "\n")
  99               ;; (display func-type)
 100               ;; (display "\n")
 101               ;; (display resolved-func-type)
 102               ;; (display "\n")
 103               ;; (display arg-type-res)
 104               ;; (display "\n")
 105               (if (abs? resolved-func-type)
 106                   (let ((return-type (substitute cs (caddr resolved-func-type))))
 107                     (list cs return-type))
 108                   (error #f "not a function")))))))
 109       ;; (display "result of ")
 110       ;; (display x)
 111       ;; (display ":\n\t")
 112       ;; (display (cadr res))
 113       ;; (display "[")
 114       ;; (display (car res))
 115       ;; (display "]\n")
 116       res))
 117   (cadr (check '() (normalize prog))))
 118
 119
 120 (define (abs? t)
 121   (and (list? t) (eq? (car t) 'abs)))
 122
 123 (define (tvar? t)
 124   (and (not (list? t)) (not (concrete? t)) (symbol? t)))
 125
 126 (define (concrete? t)
 127   (case t
 128     ('int #t)
 129     ('bool #t)
 130     (else #f)))
 131
 132                                         ; returns a list of pairs of constraints
 133 (define (unify a b)
 134   (cond ((eq? a b) '())
 135         ((or (tvar? a) (tvar? b)) (~ a b))
 136         ((and (abs? a) (abs? b))
 137          (consolidate (unify (cadr a) (cadr b))
 138                       (unify (caddr a) (caddr b))))
 139         (else (error #f "could not unify"))))
 140
 141
 142                                         ; TODO: what's the most appropriate substitution?
 143                                         ; should all constraints just be limited to a pair?
 144 (define (substitute cs t)
 145                                         ; gets the first concrete type
 146                                         ; otherwise returns the last type variable
 147   (define (get-concrete c)
 148     (if (null? (cdr c))
 149         (car c)
 150         (if (not (tvar? (car c)))
 151             (car c)
 152             (get-concrete (cdr c)))))
 153   (fold-left
 154    (lambda (t c)
 155      (if (member t c)
 156          (get-concrete c)
 157          t))
 158    t cs))
 159
 160 (define (substitute-env cs env)
 161   (map (lambda (x) (cons (car x) (substitute cs (cdr x)))) env))
 162
 163 (define (~ a b)
 164   (list (list a b)))
 165
 166 (define (consolidate x y)
 167   (define (merge a b)
 168     (cond ((null? a) b)
 169           ((null? b) a)
 170           (else (if (member (car b) a)
 171                     (merge a (cdr b))
 172                     (cons (car b) (merge a (cdr b)))))))
 173   (define (overlap? a b)
 174     (if (or (null? a) (null? b))
 175         #f
 176         (if (fold-left (lambda (acc v)
 177                          (or acc (eq? v (car a))))
 178                        #f b)
 179             #t
 180             (overlap? (cdr a) b))))
 181
 182   (cond ((null? y) x)
 183         ((null? x) y)
 184         (else (let* ((a (car y))
 185                      (merged (fold-left
 186                               (lambda (acc b)
 187                                 (if acc
 188                                     acc
 189                                     (if (overlap? a b)
 190                                         (cons (merge a b) b)
 191                                         #f)))
 192                               #f x))
 193                      (removed (if merged
 194                                   (filter (lambda (b) (not (eq? b (cdr merged)))) x)
 195                                   x)))
 196                 (if merged
 197                     (consolidate removed (cons (car merged) (cdr y)))
 198                     (consolidate (cons a x) (cdr y)))))))