2 (and (list? x) (>= (length x) 2) (not (eq? (car x) 'lambda))))
5 (and (list? x) (eq? (car x) 'lambda)))
7 (define lambda-arg caadr)
8 (define lambda-body caddr)
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)
15 (env-lookup (cdr env) x))))
22 (set! cur-tvar (+ cur-tvar 1))
24 (string-append "t" (number->string (- cur-tvar 1))))))
27 (define (normalize prog) ; (+ a b) -> ((+ a) b)
29 ((lambda? prog) '(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)
37 (define (typecheck prog)
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)))
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)
57 (list (car body-type-res)
59 (env-lookup subd-env (lambda-arg x))
60 (cadr body-type-res)))))
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))
69 (func-c (unify func-type
73 (cs (append func-c (car arg-type-res) (car func-type-res)))
75 (resolved-func-type (substitute cs func-type))
76 (resolved-return-type (caddr resolved-func-type)))
80 ;; (display func-type)
82 ;; (display resolved-func-type)
84 ;; (display arg-type-res)
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 ")
93 ;; (display (cadr res))
95 ;; (display (car res))
98 (cadr (check '() (normalize prog))))
102 (and (list? t) (eq? (car t) 'abs)))
105 (and (not (list? t)) (not (concrete? t)) (symbol? t)))
107 (define (concrete? t)
113 ; returns a list of pairs of constraints
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"))))
123 ; TODO: what's the most appropriate substitution?
124 ; should all constraints just be limited to a pair?
125 (define (substitute cs t)
129 (if (not (tvar? (car c)))
139 (define (substitute-env cs env)
140 (map (lambda (x) (cons (car x) (substitute cs (cdr x)))) env))
145 (define (consolidate x y)
149 (else (if (member (car b) a)
151 (cons (car b) (merge a (cdr b)))))))
152 (define (overlap? a b)
153 (if (or (null? a) (null? b))
155 (if (fold-left (lambda (acc v)
156 (or acc (eq? v (car a))))
159 (overlap? (cdr a) b))))
163 (else (let* ((a (car y))
173 (filter (lambda (b) (not (eq? b (cdr merged)))) x)
176 (consolidate removed (cons (car merged) (cdr y)))
177 (consolidate (cons a x) (cdr y)))))))