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 (x y) (+ x y)) -> (lambda (x) (lambda (y) (+ x y)))
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)))))
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)
41 (map (lambda (x) (cons (car x) (normalize (cdr x))))
43 (map normalize (let-body prog))))
46 (define (builtin-type x)
48 ('+ '(abs int (abs int int)))
49 ('- '(abs int (abs int int)))
50 ('* '(abs int (abs int int)))
52 ('bool->int '(abs bool int))
55 ; we typecheck the lambda calculus only (only single arg lambdas)
56 (define (typecheck prog)
58 ;; (display "check: ")
66 ((integer? x) (list '() 'int))
67 ((boolean? x) (list '() 'bool))
68 ((builtin-type x) (list '() (builtin-type x)))
69 ((symbol? x) (list '() (env-lookup env x)))
71 (let ((new-env (fold-left
74 (env-insert acc (car bind) (fresh-tvar))
76 (env-insert acc (car bind) (cadr t))))
77 env (let-bindings x))))
78 (check new-env (last (let-body x)))))
82 (let* ((new-env (env-insert env (lambda-arg x) (fresh-tvar)))
83 (body-type-res (check new-env (lambda-body x)))
84 (cs (car body-type-res))
85 (subd-env (substitute-env (car body-type-res) new-env))
86 (arg-type (env-lookup subd-env (lambda-arg x)))
87 (resolved-arg-type (substitute cs arg-type)))
88 ;; (display "lambda:\n\t")
93 ;; (display resolved-arg-type)
95 (list (car body-type-res)
98 (cadr body-type-res)))))
101 (let* ((arg-type-res (check env (cadr x)))
102 (arg-type (cadr arg-type-res))
103 (func-type-res (check env (car x)))
104 (func-type (cadr func-type-res))
107 (func-c (unify func-type
112 (consolidate func-c (car arg-type-res))
113 (car func-type-res)))
115 (resolved-func-type (substitute cs func-type))
116 (resolved-return-type (caddr resolved-func-type)))
117 ;; (display "app:\n")
120 ;; (display func-type)
122 ;; (display resolved-func-type)
124 ;; (display arg-type-res)
126 (if (abs? resolved-func-type)
127 (let ((return-type (substitute cs (caddr resolved-func-type))))
128 (list cs return-type))
129 (error #f "not a function")))))))
130 ;; (display "result of ")
133 ;; (display (cadr res))
135 ;; (display (car res))
138 (cadr (check '() (normalize prog))))
142 (and (list? t) (eq? (car t) 'abs)))
145 (and (not (list? t)) (not (concrete? t)) (symbol? t)))
147 (define (concrete? t)
153 ; returns a list of pairs of constraints
155 (cond ((eq? a b) '())
156 ((or (tvar? a) (tvar? b)) (~ a b))
157 ((and (abs? a) (abs? b))
158 (consolidate (unify (cadr a) (cadr b))
159 (unify (caddr a) (caddr b))))
160 (else (error #f "could not unify"))))
162 ; TODO: what's the most appropriate substitution?
163 ; should all constraints just be limited to a pair?
164 (define (substitute cs t)
165 ; gets the first concrete type
166 ; otherwise returns the last type variable
168 (define (get-concrete c)
169 (let ((last (null? (cdr c))))
170 (if (not (tvar? (car c)))
172 (substitute cs (car c))
176 (get-concrete (cdr c))))))
179 (substitute cs (cadr t))
180 (substitute cs (caddr t))))
189 (define (substitute-env cs env)
190 (map (lambda (x) (cons (car x) (substitute cs (cdr x)))) env))
195 (define (consolidate x y)
199 (else (if (member (car b) a)
201 (cons (car b) (merge a (cdr b)))))))
202 (define (overlap? a b)
203 (if (or (null? a) (null? b))
205 (if (fold-left (lambda (acc v)
206 (or acc (eq? v (car a))))
209 (overlap? (cdr a) b))))
213 (else (let* ((a (car y))
223 (filter (lambda (b) (not (eq? b (cdr merged)))) x)
226 (consolidate removed (cons (car merged) (cdr y)))
227 (consolidate (cons a x) (cdr y)))))))