typecheck.scm

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