| ;; based on: | |
| ;; | |
| ;; robin milner, "a theory of type polymorphism in programming", | |
| ;; journal of computer and system sciences 17(3), 348–375, 1978 | |
| ;; | |
| ;; paper: | |
| ;; https://www.pure.ed.ac.uk/ws/portalfiles/portal/15143545/1_s2.0_0022000078900144_main.pdf | | | ;; | | | ;; luis damas and robin milner, "principal type-schemes for functional | | | ;; programs", popl '82, 207–212, 1982 | |
| ;; | |
| ;; paper: | |
| ;; https://steshaw.org/hm/milner-damas.pdf | |
| ;; | |
| ;; this is an adaptation of milners algorithm w for a small ml-like | | | ;; language represented directly as scheme s-expressions | |
| ;; | |
| ;; the central judgement is: | |
| ;; | |
| ;; w(gamma, e) = (s, tau) | |
| ;; | |
| ;; gamma is the typing environment, e is the expression, s is the | | | ;; substitution produced by inference and tau is the inferred monotype | | | ;; | | | ;; unknown types are represented by fresh metavariables and application | | | ;; introduces a fresh result variable and generates the constraint | |
| ;; | |
| ;; tau1 ~ tau2 -> alpha | |
| ;; | |
| ;; which is solved by unification. substitutions are composed as w | |
| ;; recursively traverses the term | |
| ;; | |
| ;; let-polymorphism is represented explicitly with type schemes: | |
| ;; | |
| ;; forall a1 ... an. tau | |
| ;; | |
| ;; variables free in tau but not in gamma are generalised at let | | | ;; bindings. every later use is instantiated with fresh metavariables. | | | ;; this is the machinery that gives the usual principal types for | |
| ;; expressions such as: | |
| ;; | |
| ;; let id = fun x -> x in | |
| ;; (id 1, id true) | |
| ;; | |
| ;; whose inferred result is: | |
| ;; | |
| ;; int * bool | |
| ;; | |
| ;; while: | |
| ;; | |
| ;; id : forall a. a -> a | |
| ;; | |
| ;; remains polymorphic | |
| ;; | |
| ;; unification computes a most-general unifier as the occurs check rejects | |
| ;; recursive equations such as: | |
| ;; | |
| ;; a ~ a -> b | |
| ;; | |
| ;; which would otherwise describe an infinite type | |
| ;; | |
| ;; the damas–milner result concerns principal type-schemes: for the | |
| ;; relevant purely applicative ml fragment, the inferred scheme is | | | ;; principal, meaning every other valid typing is an instance of it | | | ;; | | | ;; this impl extends the small core with tuples, lists, | | | ;; primitive operators, sequencing, and letrec. these are impl | | | ;; extensions using the same inference machinery rather than a claim that | | | ;; every surface construct below appears verbatim in milner's presentation | | | ;; | | | ;; recursive bindings use a provisional monotype, constrain it against | | | ;; the inferred definition, and only then generalise the resulting type | |
| ;; | |
| ;; supported expressions: | |
| ;; | |
| ;; 42 | |
| ;; #t | |
| ;; #f | |
| ;; x | |
| ;; (lambda (x) e) | |
| ;; (f x) | |
| ;; (let ((x e)) body) | |
| ;; (letrec ((x e)) body) | |
| ;; (if c t e) | |
| ;; (begin e1 e2 ...) | |
| ;; (tuple e1 e2 ...) | |
| ;; nil | |
| ;; (cons x xs) | |
| ;; (head xs) | |
| ;; (tail xs) | |
| ;; (null? xs) | |
| ;; (+ x y) | |
| ;; (- x y) | |
| ;; (* x y) | |
| ;; (/ x y) | |
| ;; (< x y) | |
| ;; (<= x y) | |
| ;; (> x y) | |
| ;; (>= x y) | |
| ;; (= x y) | |
| ;; (and x y) | |
| ;; (or x y) | |
| ;; (not x) | |
| (define (type-error tag . args) | |
| (apply error (cons tag args))) | |
| (define (member-symbol? x xs) | |
| (cond | |
| ((null? xs) #f) | |
| ((eq? x (car xs)) #t) | |
| (else (member-symbol? x (cdr xs))))) | |
| (define (filter-list p xs) | |
| (cond | |
| ((null? xs) '()) | |
| ((p (car xs)) | |
| (cons (car xs) | |
| (filter-list p (cdr xs)))) | |
| (else | |
| (filter-list p (cdr xs))))) | |
| (define (fold-left f acc xs) | |
| (if (null? xs) | |
| acc | |
| (fold-left f | |
| (f acc (car xs)) | |
| (cdr xs)))) | |
| (define (set-add x xs) | |
| (if (member-symbol? x xs) | |
| xs | |
| (cons x xs))) | |
| (define (set-union xs ys) | |
| (fold-left | |
| (lambda (acc x) | |
| (set-add x acc)) | |
| ys | |
| xs)) | |
| (define (set-difference xs ys) | |
| (filter-list | |
| (lambda (x) | |
| (not (member-symbol? x ys))) | |
| xs)) | |
| (define (string-join xs separator) | |
| (cond | |
| ((null? xs) "") | |
| ((null? (cdr xs)) (car xs)) | |
| (else | |
| (string-append | |
| (car xs) | |
| separator | |
| (string-join (cdr xs) separator))))) | |
| (define *next-type-variable* 0) | |
| (define (reset-type-variables!) | |
| (set! *next-type-variable* 0)) | |
| (define (fresh-type-variable) | |
| (let ((n *next-type-variable*)) | |
| (set! *next-type-variable* | |
| (+ n 1)) | |
| (string->symbol | |
| (string-append "t" | |
| (number->string n))))) | |
| (define type-int 'int) | |
| (define type-bool 'bool) | |
| (define type-unit 'unit) | |
| (define (type-arrow from to) | |
| (list '-> from to)) | |
| (define (type-list element) | |
| (list 'list element)) | |
| (define (type-tuple elements) | |
| (cons 'tuple elements)) | |
| (define (type-arrow? type) | |
| (and (pair? type) | |
| (eq? (car type) '->) | |
| (= (length type) 3))) | |
| (define (type-list? type) | |
| (and (pair? type) | |
| (eq? (car type) 'list) | |
| (= (length type) 2))) | |
| (define (type-tuple? type) | |
| (and (pair? type) | |
| (eq? (car type) 'tuple))) | |
| (define (primitive-type? type) | |
| (and (symbol? type) | |
| (or (eq? type 'int) | |
| (eq? type 'bool) | |
| (eq? type 'unit)))) | |
| (define (type-variable? type) | |
| (and (symbol? type) | |
| (not (primitive-type? type)))) | |
| (define empty-substitution '()) | |
| (define (substitution-lookup variable substitution) | |
| (let ((binding (assq variable substitution))) | |
| (if binding | |
| (cdr binding) | |
| #f))) | |
| (define (apply-substitution type substitution) | |
| (cond | |
| ((type-variable? type) | |
| (let ((replacement | |
| (substitution-lookup | |
| type | | | substitution))) | | | (if replacement | | | (apply-substitution | | | replacement | | | substitution) | |
| type))) | |
| ((type-arrow? type) | |
| (type-arrow | |
| (apply-substitution | |
| (cadr type) | |
| substitution) | |
| (apply-substitution | |
| (caddr type) | |
| substitution))) | |
| ((type-list? type) | |
| (type-list | |
| (apply-substitution | |
| (cadr type) | |
| substitution))) | |
| ((type-tuple? type) | |
| (type-tuple | |
| (map | |
| (lambda (element) | |
| (apply-substitution | |
| element | |
| substitution)) | |
| (cdr type)))) | |
| (else | |
| type))) | |
| (define (compose-substitutions s1 s2) | |
| (append | | | (map | | | (lambda (binding) | | | (cons | |
| (car binding) | |
| (apply-substitution | |
| (cdr binding) | |
| s1))) | |
| s2) | |
| s1)) | |
| (define (free-type-variables type) | |
| (cond | |
| ((type-variable? type) | |
| (list type)) | |
| ((type-arrow? type) | |
| (set-union | |
| (free-type-variables | |
| (cadr type)) | |
| (free-type-variables | |
| (caddr type)))) | |
| ((type-list? type) | |
| (free-type-variables | |
| (cadr type))) | |
| ((type-tuple? type) | |
| (fold-left | |
| (lambda (acc element) | |
| (set-union | |
| acc | |
| (free-type-variables element))) | |
| '() | |
| (cdr type))) | |
| (else | |
| '()))) | |
| (define (make-scheme variables body) | |
| (list 'forall variables body)) | |
| (define (scheme-variables scheme) | |
| (cadr scheme)) | |
| (define (scheme-body scheme) | |
| (caddr scheme)) | |
| (define (free-type-variables-scheme scheme) | |
| (set-difference | |
| (free-type-variables | |
| (scheme-body scheme)) | |
| (scheme-variables scheme))) | |
| (define empty-environment '()) | |
| (define (environment-extend environment name scheme) | |
| (cons | |
| (cons name scheme) | |
| environment)) | |
| (define (environment-lookup environment name) | |
| (let ((binding | |
| (assq name environment))) | |
| (if binding | |
| (cdr binding) | |
| (type-error | |
| 'unbound-variable | |
| name)))) | |
| (define (free-type-variables-environment environment) | |
| (if (null? environment) | |
| '() | |
| (set-union | |
| (free-type-variables-scheme | |
| (cdar environment)) | |
| (free-type-variables-environment | |
| (cdr environment))))) | |
| (define (strip-quantified-variables substitution variables) | |
| (filter-list | |
| (lambda (binding) | |
| (not | |
| (member-symbol? | |
| (car binding) | |
| variables))) | |
| substitution)) | |
| (define (apply-substitution-scheme scheme substitution) | |
| (make-scheme | |
| (scheme-variables scheme) | |
| (apply-substitution | |
| (scheme-body scheme) | |
| (strip-quantified-variables | |
| substitution | |
| (scheme-variables scheme))))) | |
| (define (apply-substitution-environment environment substitution) | |
| (map | | | (lambda (binding) | | | (cons | |
| (car binding) | |
| (apply-substitution-scheme | |
| (cdr binding) | |
| substitution))) | |
| environment)) | |
| (define (generalise environment type) | |
| (make-scheme | |
| (set-difference | |
| (free-type-variables type) | |
| (free-type-variables-environment | |
| environment)) | |
| type)) | |
| (define (instantiate scheme) | |
| (let ((substitution | |
| (map | | | (lambda (variable) | | | (cons variable | |
| (fresh-type-variable))) | |
| (scheme-variables scheme)))) | |
| (apply-substitution | |
| (scheme-body scheme) | |
| substitution))) | |
| (define (occurs-in? variable type) | |
| (member-symbol? | |
| variable | |
| (free-type-variables type))) | |
| (define (bind variable type) | |
| (cond | |
| ((equal? variable type) | |
| empty-substitution) | |
| ((occurs-in? variable type) | |
| (type-error | |
| 'occurs-check | | | variable | | | type)) | | | (else | | | (list | |
| (cons variable type))))) | |
| (define (unify-sequence lefts rights) | |
| (cond | |
| ((null? lefts) | |
| (if (null? rights) | |
| empty-substitution | |
| (type-error | |
| 'arity-mismatch))) | |
| ((null? rights) | |
| (type-error | |
| 'arity-mismatch)) | |
| (else | | | (let* ((s1 | | | (unify | |
| (car lefts) | |
| (car rights))) | |
| (s2 | | | (unify-sequence | | | (map | |
| (lambda (type) | |
| (apply-substitution type s1)) | |
| (cdr lefts)) | |
| (map | |
| (lambda (type) | |
| (apply-substitution type s1)) | |
| (cdr rights))))) | |
| (compose-substitutions | |
| s2 | |
| s1))))) | |
| (define (unify left right) | |
| (cond | |
| ((type-variable? left) | |
| (bind left right)) | |
| ((type-variable? right) | |
| (bind right left)) | |
| ((and (primitive-type? left) | |
| (primitive-type? right) | |
| (eq? left right)) | |
| empty-substitution) | |
| ((and (type-arrow? left) | |
| (type-arrow? right)) | |
| (let* ((s1 | |
| (unify | |
| (cadr left) | |
| (cadr right))) | |
| (s2 | | | (unify | |
| (apply-substitution | |
| (caddr left) | |
| s1) | |
| (apply-substitution | |
| (caddr right) | |
| s1)))) | |
| (compose-substitutions | |
| s2 | |
| s1))) | |
| ((and (type-list? left) | |
| (type-list? right)) | |
| (unify | |
| (cadr left) | |
| (cadr right))) | |
| ((and (type-tuple? left) | |
| (type-tuple? right)) | |
| (if (= (length left) | |
| (length right)) | |
| (unify-sequence | |
| (cdr left) | |
| (cdr right)) | |
| (type-error | |
| 'tuple-arity-mismatch | |
| left | | | right))) | | | (else | | | (type-error | | | 'cannot-unify | | | left | |
| right)))) | |
| (define (mono type) | |
| (make-scheme '() type)) | |
| (define (binary-type left right result) | |
| (type-arrow | |
| left | | | (type-arrow | | | right | |
| result))) | |
| (define (unary-type argument result) | |
| (type-arrow | |
| argument | |
| result)) | |
| (define (initial-environment) | |
| (let ((environment empty-environment)) | |
| ;; integer arithmetic | |
| (set! environment | | | (environment-extend | | | environment | | | '+ | | | (mono | | | (binary-type | | | 'int | | | 'int | | | 'int)))) | | | (set! environment | | | (environment-extend | | | environment | | | '- | | | (mono | | | (binary-type | | | 'int | | | 'int | | | 'int)))) | | | (set! environment | | | (environment-extend | | | environment | | | '* | | | (mono | | | (binary-type | | | 'int | | | 'int | | | 'int)))) | | | (set! environment | | | (environment-extend | | | environment | | | '/ | | | (mono | | | (binary-type | | | 'int | | | 'int | |
| 'int)))) | |
| (for-each | |
| (lambda (operator) | |
| (set! environment | | | (environment-extend | | | environment | | | operator | | | (mono | | | (binary-type | | | 'int | | | 'int | |
| 'bool))))) | |
| '(< <= > >= =)) | |
| (set! environment | | | (environment-extend | | | environment | | | 'and | | | (mono | | | (binary-type | | | 'bool | | | 'bool | | | 'bool)))) | | | (set! environment | | | (environment-extend | | | environment | | | 'or | | | (mono | | | (binary-type | | | 'bool | | | 'bool | | | 'bool)))) | | | (set! environment | | | (environment-extend | | | environment | | | 'not | | | (mono | | | (unary-type | | | 'bool | | | 'bool)))) | | | (set! environment | | | (environment-extend | | | environment | | | 'nil | |
| (make-scheme | |
| '(a) | |
| (type-list 'a)))) | |
| (set! environment | | | (environment-extend | | | environment | | | 'cons | |
| (make-scheme | |
| '(a) | |
| (binary-type | |
| 'a | |
| (type-list 'a) | |
| (type-list 'a))))) | |
| (set! environment | | | (environment-extend | | | environment | | | 'head | |
| (make-scheme | |
| '(a) | |
| (unary-type | |
| (type-list 'a) | |
| 'a)))) | |
| (set! environment | | | (environment-extend | | | environment | | | 'tail | |
| (make-scheme | |
| '(a) | |
| (unary-type | |
| (type-list 'a) | |
| (type-list 'a))))) | |
| (set! environment | | | (environment-extend | | | environment | | | 'null? | |
| (make-scheme | |
| '(a) | |
| (unary-type | |
| (type-list 'a) | |
| 'bool)))) | |
| environment)) | |
| (define (lambda-expression? expression) | |
| (and (pair? expression) | |
| (eq? (car expression) 'lambda) | |
| (= (length expression) 3) | |
| (pair? (cadr expression)) | |
| (= (length (cadr expression)) 1))) | |
| (define (let-expression? expression) | |
| (and (pair? expression) | |
| (eq? (car expression) 'let) | |
| (= (length expression) 3))) | |
| (define (letrec-expression? expression) | |
| (and (pair? expression) | |
| (eq? (car expression) 'letrec) | |
| (= (length expression) 3))) | |
| (define (if-expression? expression) | |
| (and (pair? expression) | |
| (eq? (car expression) 'if) | |
| (= (length expression) 4))) | |
| (define (begin-expression? expression) | |
| (and (pair? expression) | |
| (eq? (car expression) 'begin) | |
| (>= (length expression) 2))) | |
| (define (tuple-expression? expression) | |
| (and (pair? expression) | |
| (eq? (car expression) 'tuple))) | |
| (define (operator? expression) | |
| (and (pair? expression) | |
| (member-symbol? | |
| (car expression) | |
| '(+ - * / < <= > >= = and or not)))) | |
| (define (curry-application expression) | |
| (fold-left | |
| (lambda (operator argument) | |
| (list operator argument)) | |
| (car expression) | |
| (cdr expression))) | |
| (define (infer environment expression) | |
| (cond | |
| ((integer? expression) | |
| (cons empty-substitution | |
| type-int)) | |
| ((boolean? expression) | |
| (cons empty-substitution | |
| type-bool)) | |
| ((symbol? expression) | |
| (cons empty-substitution | |
| (instantiate | | | (environment-lookup | | | environment | |
| expression)))) | |
| ((lambda-expression? expression) | |
| (let* ((name | |
| (car (cadr expression))) | |
| (body | |
| (caddr expression)) | |
| (argument-type | |
| (fresh-type-variable)) | |
| (body-environment | |
| (environment-extend | |
| environment | | | name | | | (mono argument-type))) | | | (result | | | (infer | | | body-environment | | | body)) | | | (substitution | |
| (car result)) | |
| (body-type | |
| (cdr result))) | |
| (cons | | | substitution | |
| (type-arrow | |
| (apply-substitution | |
| argument-type | | | substitution) | |
| body-type)))) | |
| ((and (pair? expression) | |
| (= (length expression) 2)) | |
| (let* ((function-result | |
| (infer | | | environment | | | (car expression))) | | | (s1 | |
| (car function-result)) | |
| (function-type | |
| (cdr function-result)) | |
| (environment-1 | |
| (apply-substitution-environment | |
| environment | |
| s1)) | |
| (argument-result | |
| (infer | | | environment-1 | | | (cadr expression))) | | | (s2 | |
| (car argument-result)) | |
| (argument-type | |
| (cdr argument-result)) | |
| (result-type | |
| (fresh-type-variable)) | |
| (s3 | | | (unify | | | (apply-substitution | | | function-type | | | s2) | | | (type-arrow | | | argument-type | | | result-type))) | | | (substitution | | | (compose-substitutions | | | s3 | | | (compose-substitutions | | | s2 | | | s1)))) | | | (cons | | | substitution | | | (apply-substitution | | | result-type | |
| s3)))) | |
| ((if-expression? expression) | |
| (let* ((condition-result | |
| (infer | | | environment | | | (cadr expression))) | | | (s1 | |
| (car condition-result)) | |
| (condition-type | |
| (cdr condition-result)) | |
| (s2 | | | (unify | | | (apply-substitution | | | condition-type | | | s1) | | | type-bool)) | | | (s12 | | | (compose-substitutions | | | s2 | |
| s1)) | |
| (environment-1 | |
| (apply-substitution-environment | |
| environment | |
| s12)) | |
| (then-result | |
| (infer | | | environment-1 | | | (caddr expression))) | | | (s3 | |
| (car then-result)) | |
| (then-type | |
| (cdr then-result)) | |
| (s123 | | | (compose-substitutions | | | s3 | |
| s12)) | |
| (environment-2 | |
| (apply-substitution-environment | |
| environment | |
| s123)) | |
| (else-result | |
| (infer | | | environment-2 | | | (cadddr expression))) | | | (s4 | |
| (car else-result)) | |
| (else-type | |
| (cdr else-result)) | |
| (s5 | | | (unify | | | (apply-substitution | | | then-type | | | s4) | | | else-type))) | | | (cons | | | (compose-substitutions | | | s5 | | | (compose-substitutions | | | s4 | | | (compose-substitutions | | | s3 | |
| s12))) | |
| (apply-substitution | |
| else-type | |
| s5)))) | |
| ((let-expression? expression) | |
| (let* ((bindings | |
| (cadr expression)) | |
| (binding | |
| (if (= (length bindings) 1) | |
| (car bindings) | |
| (error | | | "let expects one binding"))) | | | (name | | | (car binding)) | | | (value | | | (cadr binding)) | | | (body | |
| (caddr expression)) | |
| (value-result | |
| (infer | | | environment | | | value)) | | | (s1 | |
| (car value-result)) | |
| (value-type | |
| (cdr value-result)) | |
| (environment-1 | |
| (apply-substitution-environment | |
| environment | |
| s1)) | |
| (value-type-1 | |
| (apply-substitution | |
| value-type | | | s1)) | | | (scheme | | | (generalise | | | environment-1 | |
| value-type-1)) | |
| (environment-2 | |
| (environment-extend | |
| environment-1 | | | name | |
| scheme)) | |
| (body-result | |
| (infer | | | environment-2 | | | body))) | | | (cons | |
| (compose-substitutions | |
| (car body-result) | |
| s1) | |
| (cdr body-result)))) | |
| ((letrec-expression? expression) | |
| (let* ((bindings | |
| (cadr expression)) | |
| (binding | |
| (if (= (length bindings) 1) | |
| (car bindings) | |
| (error | | | "letrec expects one binding"))) | | | (name | | | (car binding)) | | | (value | | | (cadr binding)) | | | (body | | | (caddr expression)) | | | ;; the recursive name is visible while checking its own | | | ;; definition through a provisional monotype | |
| (provisional-type | |
| (fresh-type-variable)) | |
| (environment-1 | |
| (environment-extend | |
| environment | | | name | |
| (mono provisional-type))) | |
| (value-result | |
| (infer | | | environment-1 | | | value)) | | | (s1 | |
| (car value-result)) | |
| (value-type | |
| (cdr value-result)) | |
| (s2 | | | (unify | | | (apply-substitution | | | provisional-type | | | s1) | | | value-type)) | | | (s12 | | | (compose-substitutions | | | s2 | |
| s1)) | |
| (environment-2 | |
| (apply-substitution-environment | |
| environment | |
| s12)) | |
| (final-type | |
| (apply-substitution | |
| provisional-type | | | s12)) | | | (scheme | | | (generalise | | | environment-2 | |
| final-type)) | |
| (environment-3 | |
| (environment-extend | |
| environment-2 | | | name | |
| scheme)) | |
| (body-result | |
| (infer | | | environment-3 | | | body))) | | | (cons | |
| (compose-substitutions | |
| (car body-result) | |
| s12) | |
| (cdr body-result)))) | |
| ((begin-expression? expression) | |
| (infer-sequence | |
| environment | |
| (cdr expression))) | |
| ((tuple-expression? expression) | |
| (infer-tuple | |
| environment | |
| (cdr expression)) | |
| ((operator? expression) | |
| (infer | | | environment | |
| (curry-application expression))) | |
| ((and (pair? expression) | |
| (member-symbol? | |
| (car expression) | |
| '(cons head tail null?))) | |
| (infer | | | environment | |
| (curry-application expression))) | |
| ((and (pair? expression) | |
| (> (length expression) 2)) | |
| (infer | | | environment | | | (curry-application expression))) | | | (else | | | (type-error | | | 'unknown-expression | |
| expression)))) | |
| (define (infer-sequence environment expressions) | |
| (if (null? expressions) | |
| (cons empty-substitution | |
| type-unit) | |
| (let loop ((environment environment) | |
| (expressions expressions) | |
| (substitution empty-substitution) | |
| (last-type type-unit)) | |
| (if (null? expressions) | |
| (cons substitution | |
| last-type) | |
| (let* ((result | |
| (infer | | | environment | | | (car expressions))) | | | (s | | | (car result)) | | | (type | | | (cdr result)) | | | (combined | | | (compose-substitutions | | | s | |
| substitution)) | |
| (environment-1 | |
| (apply-substitution-environment | |
| environment | | | combined))) | | | (loop | | | environment-1 | | | (cdr expressions) | | | combined | |
| type)))))) | |
| (define (infer-tuple environment expressions) | |
| (let loop ((environment environment) | |
| (expressions expressions) | |
| (substitution empty-substitution) | |
| (types '())) | |
| (if (null? expressions) | |
| (cons | | | substitution | |
| (type-tuple | |
| (reverse types))) | |
| (let* ((result | |
| (infer | | | environment | | | (car expressions))) | | | (s | | | (car result)) | | | (type | | | (cdr result)) | | | (combined | | | (compose-substitutions | | | s | |
| substitution)) | |
| (environment-1 | |
| (apply-substitution-environment | |
| environment | | | combined))) | | | (loop | | | environment-1 | | | (cdr expressions) | | | combined | | | (cons | | | (apply-substitution | | | type | | | combined) | |
| types)))))) | |
| (define (type-variable-label n) | |
| (if (< n 26) | |
| (string | |
| (integer->char | |
| (+ (char->integer #\a) | |
| n))) | |
| (string-append | |
| (string | |
| (integer->char | |
| (+ (char->integer #\a) | |
| (modulo n 26)))) | |
| (number->string | |
| (quotient n 26))))) | |
| (define (rename-type-variables type) | |
| (let ((mapping '()) | |
| (counter 0)) | |
| (define (rename variable) | |
| (let ((binding | |
| (assq variable mapping))) | |
| (if binding | |
| (cdr binding) | |
| (let ((name | |
| (string->symbol | |
| (type-variable-label | |
| counter)))) | |
| (set! counter | | | (+ counter 1)) | | | (set! mapping | | | (cons | |
| (cons variable name) | |
| mapping)) | |
| name)))) | |
| (define (walk t) | |
| (cond | |
| ((type-variable? t) | |
| (rename t)) | |
| ((type-arrow? t) | |
| (type-arrow | |
| (walk (cadr t)) | |
| (walk (caddr t)))) | |
| ((type-list? t) | |
| (type-list | |
| (walk (cadr t)))) | |
| ((type-tuple? t) | |
| (type-tuple | |
| (map walk | | | (cdr t)))) | | | (else | |
| t))) | |
| (walk type))) | |
| (define (type->string type) | |
| (cond | | | ((eq? type 'int) | | | "int") | | | ((eq? type 'bool) | | | "bool") | | | ((eq? type 'unit) | | | "unit") | |
| ((type-variable? type) | |
| (symbol->string type)) | |
| ((type-arrow? type) | |
| (let ((from (cadr type)) | |
| (to (caddr type))) | |
| (string-append | |
| (if (type-arrow? from) | |
| (string-append | |
| "(" | |
| (type->string from) | |
| ")") | |
| (type->string from)) | |
| " -> " | |
| (type->string to)))) | |
| ((type-list? type) | |
| (string-append | |
| "[" | |
| (type->string | |
| (cadr type)) | |
| "]")) | |
| ((type-tuple? type) | |
| (string-append | |
| "(" | |
| (string-join | |
| (map type->string | |
| (cdr type)) | |
| " * ") | | | ")")) | | | (else | | | (type-error | | | 'unknown-type | |
| type)))) | |
| (define (infer-principal-type expression) | |
| (reset-type-variables!) | |
| (let* ((result | |
| (infer | |
| (initial-environment) | |
| expression)) | |
| (substitution | | | (car result)) | | | (type | |
| (cdr result))) | |
| (rename-type-variables | |
| (apply-substitution | |
| type | |
| substitution)))) | |
| (define (infer-type expression) | |
| (type->string | |
| (infer-principal-type | |
| expression))) | |
| (define (assert-type expression expected) | |
| (let ((actual | |
| (infer-type expression))) | |
| (if (string=? actual expected) | |
| #t | | | (error | | | "expected" | | | expected | | | "got" | |
| actual)))) | |
| (assert-type | |
| 42 | | | "int") | | | (assert-type | | | #t | | | "bool") | |
| (assert-type | |
| '(lambda (x) x) | |
| "(a -> a)") | |
| (assert-type | |
| '(lambda (x) | |
| (lambda (y) | |
| x)) | |
| "(a -> (b -> a))") | |
| (assert-type | |
| '(lambda (f) | |
| (lambda (x) | |
| (f x))) | |
| "((a -> b) -> (a -> b))") | |
| (assert-type | |
| '(lambda (f) | |
| (lambda (g) | |
| (lambda (x) | |
| (f (g x))))) | |
| "((b -> c) -> ((a -> b) -> (a -> c)))") | |
| (assert-type | |
| '(lambda (x) | |
| (+ x 1)) | |
| "(int -> int)") | |
| (assert-type | |
| '(lambda (x) | |
| (if x 1 0)) | |
| "(bool -> int)") | |
| (assert-type | |
| '(let ((id | |
| (lambda (x) | |
| x))) | |
| (tuple | |
| (id 1) | |
| (id #t))) | |
| "(int * bool)") | |
| (assert-type | |
| '(let ((xs | |
| (cons 1 nil))) | |
| (head xs)) | |
| "int") | |
| (assert-type | |
| '(lambda (xs) | |
| (tail xs)) | |
| "([a] -> [a])") | |
| (assert-type | |
| '(lambda (xs) | |
| (null? xs)) | |
| "([a] -> bool)") | |
| (assert-type | |
| '(letrec | |
| ((fact | |
| (lambda (n) | |
| (if | | | (= n 0) | | | 1 | | | (* n | | | (fact | | | (- n 1))))))) | | | fact) | |
| "(int -> int)") | |
| (assert-type | |
| '(letrec | |
| ((map | |
| (lambda (f) | |
| (lambda (xs) | |
| (if | | | (null? xs) | | | nil | | | (cons | |
| (f (head xs)) | |
| ((map f) | |
| (tail xs)))))))) | |
| map) | |
| "((a -> b) -> ([a] -> [b]))") | |
| (assert-type | |
| '(begin | | | 1 | | | 2 | | | 3) | | | "int") | |
| (assert-type | |
| '(tuple 1 #t 3) | |
| "(int * bool * int)") | |
| ;; expected failures | |
| ;; | |
| ;; (infer-type | |
| ;; '(+ #t 1)) | |
| ;; | |
| ;; cannot unify bool with int | |
| ;; | |
| ;; (infer-type | |
| ;; '(if #t 1 #f)) | |
| ;; | |
| ;; cannot unify int with bool | |
| ;; | |
| ;; (infer-type | |
| ;; '(lambda (x) | |
| ;; (x x))) | |
| ;; | |
| ;; occurs-check failure | |
| ;; | |
| ;; (infer-type | |
| ;; '(let ((f | |
| ;; (lambda (x) | |
| ;; (+ x 1)))) | |
| ;; (f #t))) | |
| ;; | |
| ;; cant unify bool with int | |
| (display | |
| (infer-type | |
| '(lambda (x) | |
| x))) | |
| (newline) | |
| (display | |
| (infer-type | |
| '(lambda (f) | |
| (lambda (g) | |
| (lambda (x) | |
| (f (g x)))))) | |
| (newline) | |
| (display | |
| (infer-type | |
| '(let ((id | |
| (lambda (x) | |
| x))) | |
| (tuple | |
| (id 42) | |
| (id #t))))) | |
| (newline) | |
| (display | | | (infer-type | | | '(letrec | |
| ((fact | |
| (lambda (n) | |
| (if | | | (= n 0) | | | 1 | | | (* n | | | (fact | |
| (- n 1))))))) | |
| fact)) | |
| (newline) |