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))))
47 ; we typecheck the lambda calculus only (only single arg lambdas)
48 (define (typecheck prog)
50 ;; (display "check: ")
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)))
65 (let ((new-env (fold-left
68 (env-insert acc (car bind) (fresh-tvar))
70 (env-insert acc (car bind) (cadr t))))
71 env (let-bindings x))))
72 (check new-env (last (let-body x)))))
76 (let* ((new-env (env-insert env (lambda-arg x) (fresh-tvar)))
77 (body-type-res (check new-env (lambda-body x)))
78 (cs (car body-type-res))
79 (subd-env (substitute-env (car body-type-res) new-env))
80 (arg-type (env-lookup subd-env (lambda-arg x)))
81 (resolved-arg-type (substitute cs arg-type)))
82 ;; (display "lambda:\n\t")
87 ;; (display resolved-arg-type)
89 (list (car body-type-res)
92 (cadr body-type-res)))))
95 (let* ((arg-type-res (check env (cadr x)))
96 (arg-type (cadr arg-type-res))
97 (func-type-res (check env (car x)))
98 (func-type (cadr func-type-res))
101 (func-c (unify func-type
106 (consolidate func-c (car arg-type-res))
107 (car func-type-res)))
109 (resolved-func-type (substitute cs func-type))
110 (resolved-return-type (caddr resolved-func-type)))
111 ;; (display "app:\n")
114 ;; (display func-type)
116 ;; (display resolved-func-type)
118 ;; (display arg-type-res)
120 (if (abs? resolved-func-type)
121 (let ((return-type (substitute cs (caddr resolved-func-type))))
122 (list cs return-type))
123 (error #f "not a function")))))))
124 ;; (display "result of ")
127 ;; (display (cadr res))
129 ;; (display (car res))
132 (cadr (check '() (normalize prog))))
136 (and (list? t) (eq? (car t) 'abs)))
139 (and (not (list? t)) (not (concrete? t)) (symbol? t)))
141 (define (concrete? t)
147 ; returns a list of pairs of constraints
149 (cond ((eq? a b) '())
150 ((or (tvar? a) (tvar? b)) (~ a b))
151 ((and (abs? a) (abs? b))
152 (consolidate (unify (cadr a) (cadr b))
153 (unify (caddr a) (caddr b))))
154 (else (error #f "could not unify"))))
156 ; TODO: what's the most appropriate substitution?
157 ; should all constraints just be limited to a pair?
158 (define (substitute cs t)
159 ; gets the first concrete type
160 ; otherwise returns the last type variable
162 (define (get-concrete c)
163 (let ((last (null? (cdr c))))
164 (if (not (tvar? (car c)))
166 (substitute cs (car c))
170 (get-concrete (cdr c))))))
173 (substitute cs (cadr t))
174 (substitute cs (caddr t))))
183 (define (substitute-env cs env)
184 (map (lambda (x) (cons (car x) (substitute cs (cdr x)))) env))
189 (define (consolidate x y)
193 (else (if (member (car b) a)
195 (cons (car b) (merge a (cdr b)))))))
196 (define (overlap? a b)
197 (if (or (null? a) (null? b))
199 (if (fold-left (lambda (acc v)
200 (or acc (eq? v (car a))))
203 (overlap? (cdr a) b))))
207 (else (let* ((a (car y))
217 (filter (lambda (b) (not (eq? b (cdr merged)))) x)
220 (consolidate removed (cons (car merged) (cdr y)))
221 (consolidate (cons a x) (cdr y)))))))