typecheck.scm

   1 (define (is-app? x)
   2   (and (list? x) (not (eq? (car x) 'lambda))))
   3
   4
   5 (define (is-lambda? x)
   6   (and (list? x) (eq? (car x) 'lambda)))
   7
   8 (define lambda-arg cadr)
   9 (define lambda-body caddr)
  10
  11 ; ('a, ('b, 'a))
  12 (define (env-lookup env x)
  13   (if (null? env) (error #f "empty env")                        ; it's a type equality
  14       (if (eq? (caar env) x)
  15           (cdar env)
  16           (env-lookup (cdr env) x))))
  17
  18 (define abs-arg cadr)
  19
  20 (define cur-tvar 0)
  21 (define (fresh-tvar)
  22   (begin
  23     (set! cur-tvar (+ cur-tvar 1))
  24     (string->symbol
  25      (string-append "t" (number->string (- cur-tvar 1))))))
  26
  27 (define (typecheck env x)
  28   (display "typechecking:\n\t")
  29   (display x)
  30   (display "\t")
  31   (display env)
  32   (display "\n")
  33   (let
  34       ((res
  35         (cond
  36          ((integer? x) (list '() 'int))
  37          ((boolean? x) (list '() 'bool))
  38          ((eq? x 'inc) (list '() '(abs int int)))
  39          ((symbol? x) (list '() (env-lookup env x)))
  40
  41          ((is-lambda? x)
  42           (let* ((new-env (cons (cons (lambda-arg x) (fresh-tvar)) env))
  43                  (body-type-res (typecheck new-env (lambda-body x)))
  44                  (subd-env (substitute (car body-type-res) new-env)))
  45             (display "lambda: ")
  46             (display body-type-res)
  47             (display "\n")
  48             (list (car body-type-res)
  49                   (list 'abs
  50                         (env-lookup subd-env (lambda-arg x))
  51                         (cadr body-type-res)))))
  52
  53          ((is-app? x) ; (f a)
  54           (let* ((arg-type-res (typecheck env (cadr x)))
  55                                         ; typecheck f with the knowledge that f : a -> x
  56                  (func-type-res (typecheck env (car x)))
  57                  (func-type (cadr func-type-res))
  58                  (c (unify func-type
  59                            (list 'abs
  60                                  (cadr arg-type-res)
  61                                  (fresh-tvar))))
  62                  (new-env (substitute c env))
  63                  (resolved-func-type (env-lookup new-env (car x))))
  64             (display "is-app:\n")
  65             (display c)
  66             (display "\n")
  67             (display new-env)
  68             (display "\n")
  69             (display resolved-func-type)
  70             (display "\n")
  71             (display arg-type-res)
  72             (display "\n")
  73             (if (abs? resolved-func-type)
  74                 (list (append c
  75                               (unify (cadr arg-type-res)
  76                                      (cadr resolved-func-type)))
  77                       (caddr resolved-func-type))
  78                 (error #f "wah")))))))
  79     (display "result of ")
  80     (display x)
  81     (display ":\n\t")
  82     (display (cadr res))
  83     (display "[")
  84     (display (car res))
  85     (display "]\n")
  86     res))
  87
  88
  89 (define (abs? t)
  90   (and (list? t) (eq? (car t) 'abs)))
  91
  92 (define (tvar? t)
  93   (and (not (list? t)) (not (concrete? t)) (symbol? t)))
  94
  95 (define (concrete? t)
  96   (case t
  97     ('int #t)
  98     ('bool #t)
  99     (else #f)))
 100
 101                                         ; returns a list of pairs of constraints
 102 (define (unify a b)
 103   (cond ((eq? a b) '())
 104         ((or (tvar? a) (tvar? b)) (list (cons a b)))
 105         ((and (abs? a) (abs? b))
 106          (append (unify (cadr a) (cadr b))
 107                  (unify (caddr a) (caddr b))))
 108         (else (error #f "could not unify"))))
 109
 110                                         ; takes a list of constraints and a type environment, and makes it work
 111 (define (substitute c env)
 112   (let ((go (lambda (x) (let ((tv (cdr x))
 113                               (n (car x)))
 114                           ;; (display tv)
 115                           ;; (display "\n")
 116                           ;; (display n)
 117                           (cons n (fold-left
 118                                    (lambda (a y)
 119                                      ;; (display y)
 120                                      ;; (display ":")
 121                                      ;; (display a)
 122                                      (cond ((eq? a (car y)) (cdr y))
 123                                            ((eq? a (cdr y)) (car y))
 124                                            (else a)))
 125                                    tv c))))))
 126   (map go env)))