3 (define (env-lookup env n)
4 (if (null? env) (error #f "empty env") ; it's a type equality
7 (env-lookup (cdr env) n))))
9 (define (env-insert env n t)
10 (cons (cons n t) env))
17 (set! cur-tvar (+ cur-tvar 1))
19 (string-append "t" (number->string (- cur-tvar 1))))))
27 (define (normalize prog) ; (+ a b) -> ((+ a) b)
29 ((lambda? prog) (list 'lambda (lambda-arg prog) (normalize (lambda-body 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)
36 (map (lambda (x) (cons (car x) (normalize (cdr x))))
38 (map normalize (let-body prog))))
42 (define (typecheck prog)
44 ;; (display "check: ")
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)))
57 (let ((new-env (fold-left
60 (env-insert acc (car bind) (fresh-tvar))
62 (env-insert acc (car bind) (cadr t))))
63 env (let-bindings x))))
64 (check new-env (last (let-body 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)
76 (list (car body-type-res)
78 (env-lookup subd-env (lambda-arg x))
79 (cadr body-type-res)))))
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))
88 (func-c (unify func-type
92 (cs (append func-c (car arg-type-res) (car func-type-res)))
94 (resolved-func-type (substitute cs func-type))
95 (resolved-return-type (caddr resolved-func-type)))
99 ;; (display func-type)
101 ;; (display resolved-func-type)
103 ;; (display arg-type-res)
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 ")
112 ;; (display (cadr res))
114 ;; (display (car res))
117 (cadr (check '() (normalize prog))))
121 (and (list? t) (eq? (car t) 'abs)))
124 (and (not (list? t)) (not (concrete? t)) (symbol? t)))
126 (define (concrete? t)
132 ; returns a list of pairs of constraints
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"))))
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)
150 (if (not (tvar? (car c)))
152 (get-concrete (cdr c)))))
160 (define (substitute-env cs env)
161 (map (lambda (x) (cons (car x) (substitute cs (cdr x)))) env))
166 (define (consolidate x y)
170 (else (if (member (car b) a)
172 (cons (car b) (merge a (cdr b)))))))
173 (define (overlap? a b)
174 (if (or (null? a) (null? b))
176 (if (fold-left (lambda (acc v)
177 (or acc (eq? v (car a))))
180 (overlap? (cdr a) b))))
184 (else (let* ((a (car y))
194 (filter (lambda (b) (not (eq? b (cdr merged)))) x)
197 (consolidate removed (cons (car merged) (cdr y)))
198 (consolidate (cons a x) (cdr y)))))))