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)
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 (subd-env (substitute-env (car body-type-res) new-env)))
80 (display body-type-res)
84 (list (car body-type-res)
86 (env-lookup subd-env (lambda-arg x))
87 (cadr body-type-res)))))
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))
96 (func-c (unify func-type
100 (cs (append func-c (car arg-type-res) (car func-type-res)))
102 (resolved-func-type (substitute cs func-type))
103 (resolved-return-type (caddr resolved-func-type)))
104 ;; (display "app:\n")
107 ;; (display func-type)
109 ;; (display resolved-func-type)
111 ;; (display arg-type-res)
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 ")
125 (cadr (check '() (normalize prog))))
129 (and (list? t) (eq? (car t) 'abs)))
132 (and (not (list? t)) (not (concrete? t)) (symbol? t)))
134 (define (concrete? t)
140 ; returns a list of pairs of constraints
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"))))
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)
158 (if (not (tvar? (car c)))
160 (get-concrete (cdr c)))))
168 (define (substitute-env cs env)
169 (map (lambda (x) (cons (car x) (substitute cs (cdr x)))) env))
174 (define (consolidate x y)
178 (else (if (member (car b) a)
180 (cons (car b) (merge a (cdr b)))))))
181 (define (overlap? a b)
182 (if (or (null? a) (null? b))
184 (if (fold-left (lambda (acc v)
185 (or acc (eq? v (car a))))
188 (overlap? (cdr a) b))))
192 (else (let* ((a (car y))
202 (filter (lambda (b) (not (eq? b (cdr merged)))) x)
205 (consolidate removed (cons (car merged) (cdr y)))
206 (consolidate (cons a x) (cdr y)))))))