;;; This file contains the code that is in the figures of the draft chapter 13 ;;; of "Essentials of Programming Languages". ;;; ;;; Copyright (c) 1994, D. Friedman, M. Wand, and C. Haynes ;;; Section 1 (define domains (compose cdr tcons->types)) (define range (compose car tcons->types)) (define integer-type (make-tcons 'int '())) (define boolean-type (make-tcons 'bool '())) (define type-of-datum (lambda (datum) (if (integer? datum) integer-type boolean-type))) (define proc-type? (lambda (type) (and (tcons? type) (eq? '-> (tcons->name type))))) (define make-proc-type (lambda (domain-types range-type) (make-tcons '-> (cons range-type domain-types)))) (define match-types (letrec ((same-type? (lambda (type1 type2) (let ((types1 (tcons->types type1)) (types2 (tcons->types type2))) (and (eq? (tcons->name type1) (tcons->name type2)) (= (length types1) (length types2)) (andmap2 same-type? types1 types2)))))) (lambda (type1 type2) (if (not (same-type? type1 type2)) (type-error "Incompatible types:" type1 type2))))) (define match-types-pairwise (lambda (types1 types2) (for-each match-types types1 types2))) (define andmap2 (lambda (predicate list1 list2) (or (null? list1) (and (predicate (car list1) (car list2)) (andmap2 predicate (cdr list1) (cdr list2)))))) (define type-error (lambda ls (display "Type error: ") (display (car ls)) (newline) (for-each (lambda (type) (displayln (unparse-type type))) (cdr ls)) (error))) (define type-of-exp (lambda (exp tenv) (trace-entry exp) (let ((answer (variant-case exp (lit (datum) (type-of-datum datum)) (varref (var) (apply-tenv tenv var)) (if (test-exp then-exp else-exp) (let ((test-exp-type (type-of-exp test-exp tenv)) (then-exp-type (type-of-exp then-exp tenv)) (else-exp-type (type-of-exp else-exp tenv))) (match-types test-exp-type boolean-type) (match-types then-exp-type else-exp-type) then-exp-type)) (app (rator rands) (type-of-app (type-of-exp rator tenv) (types-of-rands rands tenv))) (let (decls body) (type-of-exp body (extend-tenv (map decl->var decls) (types-of-let-rands decls tenv) tenv))) (letrec (decls body) (for-each (compose check-letrec-decl-exp decl->exp) decls) (type-of-exp body (letrec-tenv decls tenv))) (assert (type exp) (type-of-assert type exp tenv)) (proc (formals body) (type-of-proc formals body tenv)) (else (error "Invalid abstract syntax:" exp))))) (trace-exit answer) answer))) (define types-of-rands (lambda (rands tenv) (map (lambda (rand) (type-of-exp rand tenv)) rands))) (define trace-depth-counter 0) (define trace-type-of-exp #t) (define trace-entry (lambda (exp) (if trace-type-of-exp (begin (set! trace-depth-counter (+ trace-depth-counter 1)) (displayln trace-depth-counter " Entering with " (unparse exp)))))) (define trace-exit (lambda (type) (if trace-type-of-exp (begin (displayln trace-depth-counter " Leaving with " (unparse-type type)) (set! trace-depth-counter (- trace-depth-counter 1)))))) (define type-of-app (lambda (rator-type rand-types) (if (proc-type? rator-type) (match-types-pairwise (domains rator-type) rand-types) (type-error "Not a procedure type:" rator-type)) (range rator-type))) (define types-of-let-rands (lambda (decls tenv) (types-of-rands (map decl->exp decls) tenv))) (define check-letrec-decl-exp (lambda (exp) (if (not (and (assert? exp) (proc? (assert->exp exp)))) (error "Invalid declaration expression:" exp)))) (define letrec-tenv (lambda (decls tenv) (let ((vars (map decl->var decls)) (assert-exps (map decl->exp decls))) (let ((var-types (map assert->type assert-exps))) (let ((new-tenv (extend-tenv vars var-types tenv))) (for-each (lambda (assert-exp) (type-of-exp assert-exp new-tenv)) assert-exps) new-tenv))))) (define type-of-assert (lambda (assert-type exp tenv) (variant-case exp (proc (formals body) (if (proc-type? assert-type) (if (= (length formals) (length (domains assert-type))) (match-types (range assert-type) (type-of-exp body (extend-tenv formals (domains assert-type) tenv))) (error "Domain does not match formals" formals assert-type)) (type-error "Assert type is not a procedure type:" assert-type))) (else (match-types (type-of-exp exp tenv) assert-type))) assert-type)) (define type-of-proc (lambda (formals body tenv) (error "Procedure not inside an assert:" formals body))) ;;; Section 2 -- no code ;;; Section 3 (define type-of-app (lambda (rator-type rand-types) (let ((range-type (fresh-app-tvar))) (match-types rator-type (make-proc-type rand-types range-type)) range-type))) (define types-of-let-rands (lambda (decls tenv) (let ((vars (map decl->var decls)) (exps (map decl->exp decls))) (let ((bound-variable-types (map fresh-var-tvar vars))) (match-types-pairwise bound-variable-types (types-of-rands exps tenv)) bound-variable-types)))) (define letrec-tenv (lambda (decls tenv) (let ((vars (map decl->var decls)) (exps (map decl->exp decls))) (let ((bound-variable-types (map fresh-var-tvar vars))) (let ((new-tenv (extend-tenv vars bound-variable-types tenv))) (match-types-pairwise bound-variable-types (types-of-rands exps new-tenv)) new-tenv))))) (define check-letrec-decl-exp (lambda (exp) (if (not (or (proc? exp) (and (assert? exp) (proc? (assert->exp exp))))) (error "Invalid declaration expressions:" exp)))) (define type-of-assert (lambda (assert-type exp tenv) (match-types assert-type (type-of-exp exp tenv)) assert-type)) (define type-of-proc (lambda (formals body tenv) (let ((domain-types (map fresh-var-tvar formals))) (let ((range-type (type-of-exp body (extend-tenv formals domain-types tenv)))) (make-proc-type domain-types range-type))))) (define match-types (lambda (type1 type2) (unify type1 type2))) (define-record tvar (cell name app?)) (define app-index 0) (define var-list '()) (define fresh-tvar (lambda (app? name) (make-tvar (make-cell '*unbound*) (string->symbol name) app?))) (define fresh-app-tvar (lambda () (set! app-index (+ 1 app-index)) (fresh-tvar #t (string-append "t" (number->string app-index))))) (define fresh-var-tvar (lambda (var) (let ((index (count-occurrences var var-list))) (set! var-list (cons var var-list)) (fresh-tvar #f (string-append "t" (symbol->string var) (if (zero? index) "" (string-append "^" (number->string index)))))))) (define tvar-binding (compose cell-ref tvar->cell)) (define tvar-unbound? (lambda (tvar) (eq? (tvar-binding tvar) '*unbound*))) (define trace-tvar-bindings #t) (define bind-tvar! (lambda (tvar type) (if trace-tvar-bindings (displayln " Binding tvar " (tvar->name tvar) " to " (unparse-type type))) (cell-set! (tvar->cell tvar) type))) (define tvar-end-value (lambda (tvar) (if (tvar-unbound? tvar) tvar (let ((binding (tvar-binding tvar))) (if (tcons? binding) binding (let ((type (tvar-end-value binding))) (bind-tvar! tvar type) type)))))) (define type-dispatch (lambda (type ctvar-proc tcons-proc) (let ((value (if (tvar? type) (tvar-end-value type) type))) (if (tvar? value) (ctvar-proc value) (tcons-proc value))))) (define unify (lambda (type1 type2) (type-dispatch type1 (lambda (ctvar1) (unify-tvar ctvar1 type2)) (lambda (tcons1) (type-dispatch type2 (lambda (ctvar2) (unify-tvar ctvar2 tcons1)) (lambda (tcons2) (let ((types1 (tcons->types tcons1)) (types2 (tcons->types tcons2))) (if (and (= (length types1) (length types2)) (eq? (tcons->name tcons1) (tcons->name tcons2))) (for-each unify types1 types2) (type-error "Unify failure:" tcons1 tcons2))))))))) (define unify-tvar (lambda (ctvar type) (type-dispatch type (lambda (ctvar2) (if (not (eq? ctvar ctvar2)) (if (tvar->app? ctvar2) (bind-tvar! ctvar2 ctvar) (bind-tvar! ctvar ctvar2)))) (lambda (tcons) (if (occurs-in-type? ctvar tcons) (type-error "Unify-tvar occur check failure:" ctvar tcons) (bind-tvar! ctvar tcons)))))) (define occurs-in-type? (lambda (ctvar type) (type-dispatch type (lambda (ctvar2) (eq? ctvar ctvar2)) (lambda (tcons) (ormap (lambda (type) (occurs-in-type? ctvar type)) (tcons->types tcons)))))) ;;; Section 4 (define-record forall (gens body)) (define build-tscheme (lambda (type tenv) (letrec ((list-gens (lambda (type) (type-dispatch type (lambda (ctvar) (if (occurs-free-in-tenv? ctvar tenv) '() (list ctvar))) (lambda (tcons) (apply append (map list-gens (tcons->types tcons)))))))) (let ((gens (list-gens type))) (if (null? gens) type (make-forall gens type)))))) (define instantiate-tscheme (lambda (tscheme) (letrec ((loop (lambda (gens body) (if (null? gens) body (loop (cdr gens) (instantiate-type body (car gens) (fresh-instantiated-tvar (car gens)))))))) (loop (forall->gens tscheme) (forall->body tscheme))))) (define instantiate-type (lambda (type tvar fresh-tvar) (letrec ((f (lambda (type) (type-dispatch type (lambda (ctvar) (if (eq? tvar ctvar) fresh-tvar ctvar)) (lambda (tcons) (make-tcons (tcons->name tcons) (map f (tcons->types tcons)))))))) (f type)))) (define-record tvar (cell name app? inst-count)) (define fresh-tvar (lambda (app? name) (make-tvar (make-cell '*unbound*) (string->symbol name) app? (make-cell 0)))) (define fresh-instantiated-tvar (lambda (tvar) (let ((cell (tvar->inst-count tvar))) (let ((count (cell-ref cell))) (cell-set! cell (+ 1 count)) (fresh-tvar (tvar->app? tvar) (string-append (symbol->string (tvar->name tvar)) "|char'137" (number->string count))))))) (define extend-tenv (lambda (vars tschemes old-tenv) (append (map cons vars tschemes) old-tenv))) (define trace-generic-variable-instantiations #t) (define apply-tenv (lambda (tenv var) (let ((x (assq var tenv))) (if (pair? x) (let ((binding (cdr x))) (if (forall? binding) (let ((answer (instantiate-tscheme (cdr x)))) (if trace-generic-variable-instantiations (displayln " Type of var " var " instantiated to " (unparse-type answer))) answer) binding)) (error "Variable not bound:" var))))) (define occurs-free-in-tenv? (lambda (ctvar tenv) (ormap (lambda (pair) (let ((binding (cdr pair))) (and (not (forall? binding)) (occurs-in-type? ctvar binding)))) tenv))) (define types-of-let-rands (lambda (decls tenv) (let ((vars (map decl->var decls)) (exps (map decl->exp decls))) (let ((bound-variable-types (map fresh-var-tvar vars))) (match-types-pairwise bound-variable-types (types-of-rands exps tenv)) (map (lambda (type) (build-tscheme type tenv)) bound-variable-types))))) (define letrec-tenv (lambda (decls tenv) (let ((vars (map decl->var decls)) (exps (map decl->exp decls))) (let ((bound-variable-types (map fresh-var-tvar vars))) (let ((new-tenv (extend-tenv vars bound-variable-types tenv))) (match-types-pairwise bound-variable-types (types-of-rands exps new-tenv)) (extend-tenv vars (map (lambda (type) (build-tscheme type tenv)) bound-variable-types) tenv)))))) (define type-of-assert (lambda (assert-type exp tenv) (let ((type (build-sharing-type assert-type))) (match-types type (type-of-exp exp tenv)) type))) (define build-sharing-type (lambda (type) (let ((lookup (let ((var-table '())) (lambda (var) (let ((x (assq var var-table))) (if (pair? x) (cdr x) (let ((new-tvar (fresh-var-tvar var))) (set! var-table (cons (cons var new-tvar) var-table)) new-tvar))))))) (letrec ((f (lambda (type) (variant-case type (tvarref (var) (lookup var)) (tcons (name types) (make-tcons name (map f types))))))) (f type)))))