typecheck.scm

   1 (load "ast.scm")
   2 (load "stdlib.scm")
   3
   4 (define (abs? t)
   5   (and (list? t) (eq? (car t) 'abs)))
   6
   7 (define (tvar? t)
   8   (and (not (list? t))
   9        (not (concrete? t))
  10        (symbol? t)))
  11
  12 (define (concrete? t)
  13   (and (symbol? t)
  14        (char-upper-case? (string-ref (symbol->string t) 0))))
  15
  16 (define (pretty-type t)
  17   (cond ((abs? t)
  18          (string-append
  19           (if (abs? (cadr t))
  20               (string-append "(" (pretty-type (cadr t)) ")")
  21               (pretty-type (cadr t)))
  22           " -> "
  23           (pretty-type (caddr t))))
  24         (else (symbol->string t))))
  25
  26 (define (pretty-constraints cs)
  27   (string-append "{"
  28                  (fold-left string-append
  29                             ""
  30                             (map (lambda (c)
  31                                    (string-append
  32                                     (pretty-type (car c))
  33                                     ": "
  34                                     (pretty-type (cdr c))
  35                                     ", "))
  36                                  cs))
  37                  "}"))
  38
  39                                         ; ('a, ('b, 'a))
  40 (define (env-lookup env n)
  41   (if (null? env) (error #f "empty env" env n)                  ; it's a type equality
  42       (if (eq? (caar env) n)
  43           (cdar env)
  44           (env-lookup (cdr env) n))))
  45
  46 (define (env-insert env n t)
  47   (cons (cons n t) env))
  48
  49 (define abs-arg cadr)
  50
  51 (define cur-tvar 0)
  52 (define (fresh-tvar)
  53   (begin
  54     (set! cur-tvar (+ cur-tvar 1))
  55     (string->symbol
  56      (string-append "t" (number->string (- cur-tvar 1))))))
  57
  58 (define (last xs)
  59   (if (null? (cdr xs))
  60       (car xs)
  61       (last (cdr xs))))
  62
  63 (define (normalize prog) ; (+ a b) -> ((+ a) b)
  64   (case (ast-type prog)
  65     ('lambda
  66                                         ; (lambda (x y) (+ x y)) -> (lambda (x) (lambda (y) (+ x y)))
  67         (if (> (length (lambda-args prog)) 1)
  68             (list 'lambda (list (car (lambda-args prog)))
  69                   (normalize (list 'lambda (cdr (lambda-args prog)) (caddr prog))))
  70             (list 'lambda (lambda-args prog) (normalize (caddr prog)))))
  71     ('app
  72      (if (null? (cddr prog))
  73          `(,(normalize (car prog)) ,(normalize (cadr prog))) ; (f a)
  74          (normalize `(,(list (normalize (car prog)) (normalize (cadr prog)))
  75                       ,@(cddr prog))))) ; (f a b)
  76     ('let
  77         (append (list 'let
  78                       (map (lambda (x) `(,(car x) ,(normalize (cadr x))))
  79                            (let-bindings prog)))
  80                 (map normalize (let-body prog))))
  81     (else (ast-traverse normalize prog))))
  82
  83 (define (builtin-type x)
  84   (case x
  85     ('+ '(abs Int (abs Int Int)))
  86     ('- '(abs Int (abs Int Int)))
  87     ('* '(abs Int (abs Int Int)))
  88     ('! '(abs Bool Bool))
  89     ('= '(abs Int (abs Int Bool)))
  90     ('bool->int '(abs Bool Int))
  91     ('print '(abs String Void))
  92     (else (error #f "Couldn't find type for builtin" x))))
  93
  94 (define (check-let dls env x)
  95
  96   ; acc is a pair of (env . annotated bindings)
  97   (define (process-component acc comps)
  98     (let*
  99                                         ; create a new env with tvars for each component
 100                                         ; e.g. scc of (x y)
 101                                         ; scc-env = ((x . t0) (y . t1))
 102         ([scc-env
 103           (fold-left
 104            (lambda (acc c)
 105              (env-insert acc c (fresh-tvar)))
 106            (car acc) comps)]
 107                                         ; typecheck each component
 108          [type-results
 109           (map
 110            (lambda (c)
 111              (let ([body (cadr (assoc c (let-bindings x)))])
 112                (check dls scc-env body)))
 113            comps)]
 114                                         ; collect all the constraints in the scc
 115          [cs
 116           (fold-left
 117            (lambda (acc res c)
 118              (constraint-merge
 119               (constraint-merge
 120                                         ; unify with tvars from scc-env
 121                                         ; result ~ tvar
 122                (~ (env-lookup scc-env c) (cadr res))
 123                (car res))
 124               acc))
 125            '() type-results comps)]
 126                                         ; substitute *only* the bindings in this scc
 127          [new-env
 128           (map (lambda (x)
 129                  (if (memv (car x) comps)
 130                      (cons (car x) (substitute cs (cdr x)))
 131                      x))
 132                scc-env)]
 133
 134          [annotated-bindings (append (cdr acc) ; the previous annotated bindings
 135                                      (map list
 136                                           comps
 137                                           (map caddr type-results)))])
 138       (cons new-env annotated-bindings)))
 139                                         ; takes in the current environment and a scc
 140                                         ; returns new environment with scc's types added in
 141   (let* ([components (reverse (sccs (graph (let-bindings x))))]
 142          [results (fold-left process-component (cons env '()) components)]
 143          [new-env (car results)]
 144          [annotated-bindings (cdr results)]
 145
 146          [body-results (map (lambda (body) (check dls new-env body)) (let-body x))]
 147          [let-type (cadr (last body-results))]
 148          [cs (fold-left (lambda (acc cs) (constraint-merge acc cs)) '() (map car body-results))]
 149
 150          [annotated `((let ,annotated-bindings ,@(map caddr body-results)) : ,let-type)])
 151     (list cs let-type annotated)))
 152
 153 (define (check-app dls env x)
 154   (if (eqv? (car x) (cadr x))
 155                                         ; recursive function (f f)
 156                                         ; TODO: what about ((f a) f)????
 157       (let* ([func-type (env-lookup env (car x))]
 158              [return-type (fresh-tvar)]
 159              [other-func-type `(abs ,func-type ,return-type)]
 160              [cs (~ func-type other-func-type)]
 161              [resolved-return-type (substitute cs return-type)]
 162
 163              [annotated `(((,(car x) : ,func-type)
 164                            (,(cadr x) : ,func-type)) : ,resolved-return-type)])
 165         (list cs resolved-return-type annotated)))
 166
 167                                         ; regular function
 168   (let* ([arg-type-res (check dls env (cadr x))]
 169          [arg-type (cadr arg-type-res)]
 170          [func-type-res (check dls env (car x))]
 171          [func-type (cadr func-type-res)]
 172
 173                                         ; f ~ a -> t0
 174          [func-c (~
 175                   (substitute (car arg-type-res) func-type)
 176                   `(abs ,arg-type ,(fresh-tvar)))]
 177          [cs (constraint-merge
 178               (constraint-merge func-c (car arg-type-res))
 179               (car func-type-res))]
 180
 181          [resolved-func-type (substitute cs func-type)]
 182          [resolved-return-type (caddr resolved-func-type)]
 183
 184          [annotated `((,(caddr func-type-res)
 185                        ,(caddr arg-type-res)) : ,resolved-return-type)])
 186
 187     (if (abs? resolved-func-type)
 188         (let ((return-type (substitute cs (caddr resolved-func-type))))
 189           (list cs return-type annotated))
 190         (error #f "not a function"))))
 191
 192 (define (check-case dls env x)
 193
 194   (define (check-match switch-type x)
 195
 196     (define (get-bindings product-types pattern)
 197       (define (go product-type product)
 198         (case (ast-type product)
 199           ['var (list (cons product product-type))]
 200                                         ; an inner pattern match
 201           ['app (let* ([inner-sum (car product)]
 202                        [inner-sums (cdr (assoc product-type dls))]
 203                        [inner-product-types (cdr (assoc inner-sum inner-sums))])
 204                   (get-bindings inner-product-types product))]
 205           [else '()]))
 206       (flat-map go product-types (cdr pattern)))
 207
 208
 209     (let ([pattern (car x)]
 210           [expr (cadr x)])
 211       (case (ast-type pattern)
 212         ['app
 213                                         ; a pattern match with bindings
 214           (let ([sum (assoc (car pattern) (cdr (assoc switch-type dls)))])
 215             (unless sum (error #f "can't pattern match ~a with ~a" switch-type pattern))
 216             (let* ([names (cdr pattern)]
 217                    [product-types (cdr sum)]
 218                    [new-env (append (get-bindings product-types pattern) env)])
 219
 220               (check dls new-env expr)))]
 221                                         ; pattern match with binding and no constructor
 222         ['var (check dls (env-insert env pattern switch-type) expr)]
 223                                         ; a pattern match without bindings
 224         [else (check dls env expr)])))
 225
 226   (let* ([switch-type-res (check dls env (case-switch x))]
 227          [switch-type (cadr switch-type-res)]
 228
 229          [case-expr-type-res (map (lambda (x) (check-match switch-type x)) (case-cases x))]
 230          [case-expr-types (map cadr case-expr-type-res)]
 231
 232          [case-expr-equality-cs (fold-left constraint-merge '()
 233                                            (map (lambda (t) (~ t (car case-expr-types)))
 234                                                 (cdr case-expr-types)))]
 235
 236          [resolved-type (substitute case-expr-equality-cs (car case-expr-types))]
 237
 238          [annotated `((case ,(caddr switch-type-res)
 239                         ,@(map (lambda (c e et)
 240                                  `(,c ((,e : ,et))))
 241                                (map car (case-cases x))
 242                                (map cadr (case-cases x))
 243                                case-expr-types)) : ,resolved-type)]
 244
 245          [cs (fold-left constraint-merge '()
 246                         (cons (car switch-type-res) case-expr-equality-cs))])
 247     (list cs resolved-type annotated)))
 248
 249 ; returns a list (constraints type annotated)
 250 (define (check dls env x)
 251   (define (make-result cs type)
 252     (list cs type `(,x : ,type)))
 253   ;; (display "check: ")
 254   ;; (display x)
 255   ;; (display "\n\t")
 256   ;; (display env)
 257   ;; (newline)
 258   (let
 259       ((res
 260         (case (ast-type x)
 261           ('int-literal (make-result '() 'Int))
 262           ('string-literal (make-result '() 'String))
 263           ('builtin (make-result '() (builtin-type x)))
 264
 265           ('if
 266            (let* ((cond-type-res (check dls env (cadr x)))
 267                   (then-type-res (check dls env (caddr x)))
 268                   (else-type-res (check dls env (cadddr x)))
 269                   (then-eq-else-cs (~ (cadr then-type-res)
 270                                       (cadr else-type-res)))
 271                   (cs (constraint-merge
 272                        (car then-type-res)
 273                        (constraint-merge (~ (cadr cond-type-res) 'Bool)
 274                                          (constraint-merge (car else-type-res)
 275                                                            then-eq-else-cs))))
 276                   (return-type (substitute cs (cadr then-type-res)))
 277                   [annotated `((if ,(caddr cond-type-res)
 278                                    ,(caddr then-type-res)
 279                                    ,(caddr else-type-res)) : ,return-type)])
 280              (list cs return-type annotated)))
 281
 282           ('var (make-result '() (env-lookup env x)))
 283           ('let (check-let dls env x))
 284
 285
 286           ('lambda
 287               (let* ([new-env (env-insert env (lambda-arg x) (fresh-tvar))]
 288
 289                      [body-type-res (check dls new-env (lambda-body x))]
 290                      [cs (car body-type-res)]
 291                      [subd-env (substitute-env (car body-type-res) new-env)]
 292                      [arg-type (env-lookup subd-env (lambda-arg x))]
 293                      [resolved-arg-type (substitute cs arg-type)]
 294
 295                      [lambda-type `(abs ,resolved-arg-type ,(cadr body-type-res))]
 296
 297                      [annotated `((lambda (,(lambda-arg x)) ,(caddr body-type-res)) : ,lambda-type)])
 298
 299                 (list (car body-type-res) ; constraints
 300                       lambda-type  ; type
 301                       annotated)))
 302
 303
 304           ('app (check-app dls env x))
 305           ['case (check-case dls env x)])))
 306
 307
 308     ;; (display "result of ")
 309     ;; (display x)
 310     ;; (display ":\n\t")
 311     ;; (display (pretty-type (cadr res)))
 312     ;; (display "\n\t[")
 313     ;; (display (pretty-constraints (car res)))
 314     ;; (display "]\n")
 315     res))
 316
 317 (define (init-adts-env prog)
 318   (flat-map data-tors-type-env (program-data-layouts prog)))
 319
 320                                         ; we typecheck the lambda calculus only (only single arg lambdas)
 321 (define (typecheck prog-without-stdlib)
 322   (let* ([prog (append stdlib prog-without-stdlib)]
 323          [expanded (expand-pattern-matches prog)])
 324     (cadr (check (program-data-layouts prog)
 325                  (init-adts-env expanded)
 326                  (normalize (program-body expanded))))))
 327
 328
 329                                         ; before passing annotated types onto codegen
 330                                         ; we need to restore the pre-normalization structure
 331                                         ; (this is important for function arity etc)
 332 (define (denormalize orig normed)
 333
 334   (define (collapse-lambdas n x)
 335     (case n
 336       [0 x]
 337       [else
 338        (let* ([inner-lambda (lambda-body (ann-expr x))]
 339               [arg (lambda-arg (ann-expr x))]
 340               [inner-collapsed (ann-expr (collapse-lambdas (- n 1) inner-lambda))])
 341          `((lambda ,(cons arg (lambda-args inner-collapsed))
 342              ,(lambda-body inner-collapsed)) : ,(ann-type x)))]))
 343
 344   (define (collapse-apps n x)
 345     (case n
 346       [-1 (error #f "nullary functions not handled yet")]
 347       [0 x]
 348       [else
 349        (let* ([inner-app (car (ann-expr x))]
 350               [inner-collapsed (collapse-apps (- n 1) inner-app)])
 351          `(,(append (ann-expr inner-collapsed) (cdr (ann-expr x))) : ,(ann-type x)))]))
 352
 353   (case (ast-type orig)
 354     ['lambda
 355         (let ([collapsed (collapse-lambdas (- (length (lambda-args orig)) 1) normed)])
 356           `((lambda ,(lambda-args (ann-expr collapsed))
 357               ,(denormalize (lambda-body orig)
 358                             (lambda-body (ann-expr collapsed)))) : ,(ann-type collapsed)))]
 359     ['app
 360      (let ([collapsed (collapse-apps (- (length orig) 2) normed)])
 361        `(,(map (lambda (o n) (denormalize o n)) orig (ann-expr collapsed))
 362          : ,(ann-type collapsed)))]
 363     ['let
 364         `((let ,(map (lambda (o n) (list (car o) (denormalize (cadr o) (cadr n))))
 365                      (let-bindings orig)
 366                      (let-bindings (ann-expr normed)))
 367             ,@(map denormalize
 368                    (let-body orig)
 369                    (let-body (ann-expr normed)))) : ,(ann-type normed))]
 370     ['if `((if ,@(map denormalize (cdr orig) (cdr (ann-expr normed))))
 371            : ,(ann-type normed))]
 372     ['case `((case ,(denormalize (case-switch orig) (case-switch (ann-expr normed)))
 373                ,@(map (lambda (o n) (cons (car o) (denormalize (cadr o) (cadr n))))
 374                       (case-cases orig) (case-cases (ann-expr normed))))
 375              : ,(ann-type normed))]
 376     [else normed]))
 377
 378 (define ann-expr car)
 379 (define ann-type caddr)
 380
 381                                         ; prerequisites: expand-pattern-matches
 382 (define (annotate-types prog)
 383   (denormalize
 384    (program-body prog)
 385    (caddr (check (program-data-layouts prog)
 386                  (init-adts-env prog)
 387                  (normalize (program-body prog))))))
 388
 389
 390                                         ; returns a list of constraints
 391 (define (~ a b)
 392   (let ([res (unify? a b)])
 393     (if res
 394         res
 395         (error #f
 396                (format "couldn't unify ~a ~~ ~a" a b)))))
 397
 398 (define (unify? a b)
 399   (cond [(eq? a b) '()]
 400         [(tvar? a) (list (cons a b))]
 401         [(tvar? b) (list (cons b a))]
 402         [(and (abs? a) (abs? b))
 403          (let* [(arg-cs (unify? (cadr a) (cadr b)))
 404                 (body-cs (unify? (substitute arg-cs (caddr a))
 405                                  (substitute arg-cs (caddr b))))]
 406            (constraint-merge body-cs arg-cs))]
 407         [else #f]))
 408
 409 (define (substitute cs t)
 410   (cond
 411    [(tvar? t)
 412     (if (assoc t cs)
 413         (cdr (assoc t cs))
 414         t)]
 415    [(abs? t) `(abs ,(substitute cs (cadr t))
 416                    ,(substitute cs (caddr t)))]
 417    [else t]))
 418
 419                                         ; applies substitutions to all variables in environment
 420 (define (substitute-env cs env)
 421   (map (lambda (x) (cons (car x) (substitute cs (cdr x)))) env))
 422
 423                                         ; composes constraints a onto b and merges, i.e. applies a to b
 424                                         ; a should be the "more important" constraints
 425 (define (constraint-merge a b)
 426   (define (f cs constraint)
 427     (cons (car constraint)
 428           (substitute cs (cdr constraint))))
 429
 430   (define (most-concrete a b)
 431     (cond
 432      [(tvar? a) b]
 433      [(tvar? b) a]
 434      [(and (abs? a) (abs? b))
 435       `(abs ,(most-concrete (cadr a) (cadr b))
 436             ,(most-concrete (caddr a) (caddr b)))]
 437      [(abs? a) b]
 438      [(abs? b) a]
 439      [else a]))
 440
 441                                         ; for any two constraints that clash, e.g. t1 ~ abs t2 t3
 442                                         ; and t1 ~ abs int t3
 443                                         ; prepend the most concrete version of the type to the
 444                                         ; list of constraints
 445   (define (clashes)
 446     (define (gen acc x)
 447       (if (assoc (car x) a)
 448           (cons (cons (car x) (most-concrete (cdr (assoc (car x) a))
 449                                              (cdr x)))
 450                 acc)
 451           acc))
 452     (fold-left gen '() b))
 453
 454   (define (union p q)
 455     (append (filter (lambda (x) (not (assoc (car x) p)))
 456                     q)
 457             p))
 458   (append (clashes) (union a (map (lambda (z) (f a z)) b))))
 459
 460
 461 ;;                                      ; a1 -> a2 ~ a3 -> a4;
 462 ;;                                      ; a1 -> a2 !~ Bool -> Bool
 463 ;;                                      ; basically can the tvars be renamed
 464 (define (types-equal? x y)
 465   (let ([cs (unify? x y)])
 466     (if (not cs) #f
 467         (let*
 468             ([test (lambda (acc c)
 469                      (and acc
 470                           (tvar? (car c)) ; the only substitutions allowed are tvar -> tvar
 471                           (tvar? (cdr c))))])
 472           (fold-left test #t cs)))))
 473
 474                                         ; input: a list of binds ((x . y) (y . 3))
 475                                         ; returns: pair of verts, edges ((x y) . (x . y))
 476