Start typechecker

diff --git a/typecheck.scm b/typecheck.scm
new file mode 100644 (file)
index 0000000..a396a24
--- /dev/null
+++ b/typecheck.scm
@@ -0,0 +1,126 @@
+(define (is-app? x)
+  (and (list? x) (not (eq? (car x) 'lambda))))
+
+
+(define (is-lambda? x)
+  (and (list? x) (eq? (car x) 'lambda)))
+
+(define lambda-arg cadr)
+(define lambda-body caddr)
+
+; ('a, ('b, 'a))
+(define (env-lookup env x)
+  (if (null? env) (error #f "empty env")                       ; it's a type equality
+      (if (eq? (caar env) x)
+         (cdar env)
+         (env-lookup (cdr env) x))))
+
+(define abs-arg cadr)
+
+(define cur-tvar 0)
+(define (fresh-tvar)
+  (begin
+    (set! cur-tvar (+ cur-tvar 1))
+    (string->symbol
+     (string-append "t" (number->string (- cur-tvar 1))))))
+
+(define (typecheck env x)
+  (display "typechecking:\n\t")
+  (display x)
+  (display "\t")
+  (display env)
+  (display "\n")
+  (let
+      ((res
+       (cond
+        ((integer? x) (list '() 'int))
+        ((boolean? x) (list '() 'bool))
+        ((eq? x 'inc) (list '() '(abs int int)))
+        ((symbol? x) (list '() (env-lookup env x)))
+
+        ((is-lambda? x)
+         (let* ((new-env (cons (cons (lambda-arg x) (fresh-tvar)) env))
+                (body-type-res (typecheck new-env (lambda-body x)))
+                (subd-env (substitute (car body-type-res) new-env)))
+           (display "lambda: ")
+           (display body-type-res)
+           (display "\n")
+           (list (car body-type-res)
+                 (list 'abs
+                       (env-lookup subd-env (lambda-arg x))
+                       (cadr body-type-res)))))
+        
+        ((is-app? x) ; (f a)
+         (let* ((arg-type-res (typecheck env (cadr x)))
+                                       ; typecheck f with the knowledge that f : a -> x
+                (func-type-res (typecheck env (car x)))
+                (func-type (cadr func-type-res))
+                (c (unify func-type
+                          (list 'abs
+                                (cadr arg-type-res)
+                                (fresh-tvar)))) 
+                (new-env (substitute c env))
+                (resolved-func-type (env-lookup new-env (car x))))
+           (display "is-app:\n")
+           (display c)
+           (display "\n")
+           (display new-env)
+           (display "\n")
+           (display resolved-func-type)
+           (display "\n")
+           (display arg-type-res)
+           (display "\n")
+           (if (abs? resolved-func-type)
+               (list (append c
+                             (unify (cadr arg-type-res)
+                                    (cadr resolved-func-type)))
+                     (caddr resolved-func-type))
+               (error #f "wah")))))))
+    (display "result of ")
+    (display x)
+    (display ":\n\t")
+    (display (cadr res))
+    (display "[")
+    (display (car res))
+    (display "]\n")
+    res))
+
+
+(define (abs? t)
+  (and (list? t) (eq? (car t) 'abs)))
+
+(define (tvar? t)
+  (and (not (list? t)) (not (concrete? t)) (symbol? t)))
+
+(define (concrete? t)
+  (case t
+    ('int #t)
+    ('bool #t)
+    (else #f)))
+
+                                       ; returns a list of pairs of constraints
+(define (unify a b)
+  (cond ((eq? a b) '())
+       ((or (tvar? a) (tvar? b)) (list (cons a b)))
+       ((and (abs? a) (abs? b))
+        (append (unify (cadr a) (cadr b))
+                (unify (caddr a) (caddr b))))
+       (else (error #f "could not unify"))))
+
+                                       ; takes a list of constraints and a type environment, and makes it work
+(define (substitute c env)
+  (let ((go (lambda (x) (let ((tv (cdr x))
+                             (n (car x)))
+                         ;; (display tv)
+                         ;; (display "\n")
+                         ;; (display n)
+                         (cons n (fold-left
+                                  (lambda (a y)
+                                    ;; (display y)
+                                    ;; (display ":")
+                                    ;; (display a)
+                                    (cond ((eq? a (car y)) (cdr y))
+                                          ((eq? a (cdr y)) (car y))
+                                          (else a)))
+                                  tv c))))))
+  (map go env)))