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