diff options
| -rw-r--r-- | infer2.scm | 402 |
1 files changed, 402 insertions, 0 deletions
diff --git a/infer2.scm b/infer2.scm new file mode 100644 index 0000000..e2ff375 --- /dev/null +++ b/infer2.scm @@ -0,0 +1,402 @@ +(use-modules (ice-9 format) + (ice-9 match) + (srfi srfi-1) + (srfi srfi-9) + (srfi srfi-9 gnu)) + +(define-syntax-rule (define-matcher (name rules ...) body ...) + (define name + (match-lambda* + ((rules ...) body ...) + (_ 'unmatched)))) + +(define-syntax-rule (compose-matchers matcher ...) + (lambda args + (let loop ((matchers (list matcher ...))) + (match matchers + (() (error "unmatched" args)) + ((m . rest) + (let ((result (apply m args))) + (if (eq? result 'unmatched) + (loop rest) + result))))))) + + +;;; +;;; Typed expression annotation +;;; + +(define-record-type <primitive-type> + (make-primitive-type name) + primitive-type? + (name primitive-type-name)) + +(define (display-primitive-type type port) + (format port "#<primitive ~a>" (primitive-type-name type))) +(set-record-type-printer! <primitive-type> display-primitive-type) + +(define int-type (make-primitive-type 'int)) +(define float-type (make-primitive-type 'float)) +(define bool-type (make-primitive-type 'bool)) + +(define-record-type <type-variable> + (make-type-variable name) + type-variable? + (name type-variable-name)) + +(define (display-type-variable type port) + (format port "#<tvar ~a>" (type-variable-name type))) +(set-record-type-printer! <type-variable> display-type-variable) + +(define unique-counter (make-parameter 0)) + +(define (unique-number) + (let ((n (unique-counter))) + (unique-counter (+ n 1)) + n)) + +(define* (unique-identifier #:optional (prefix 'T)) + (string->symbol + (format #f "~a~a" prefix (unique-number)))) + +(define (fresh-type-variable) + (make-type-variable (unique-identifier))) + +(define-record-type <procedure-type> + (make-procedure-type arg-types return-type) + procedure-type? + (arg-types procedure-type-arg-types) + (return-type procedure-type-return-type)) + +(define (display-procedure-type type port) + (format port "#<proc-type ~a → ~a>" + (procedure-type-arg-types type) + (procedure-type-return-type type))) +(set-record-type-printer! <procedure-type> display-procedure-type) + +(define (type? obj) + (or (primitive-type? obj) + (type-variable? obj) + (procedure-type? obj))) + +(define (top-level-env) + '()) + +(define (lookup var env) + (or (assq-ref env var) + (error "unbound variable" var))) + +(define (make-texp type exp) + `(t ,type ,exp)) + +(define (texp? obj) + (match obj + (('t _ _) #t) + (_ #f))) + +(define (texp-type texp) + (match texp + (('t type _) type))) + +(define (texp-exp texp) + (match texp + (('t _ exp) exp))) + +(define (display-typed-expression texp port) + (format port "#<texp ~a ~a>" (texp-type texp) (texp-exp texp))) +(set-record-type-printer! <typed-expression> display-typed-expression) + +(define-matcher (annotate:bool (? boolean? b) env) + (make-texp bool-type b)) + +(define-matcher (annotate:int (and (? number?) (? exact-integer? n)) env) + (make-texp int-type n)) + +(define-matcher (annotate:float (and (? number?) (? inexact? n)) env) + (make-texp float-type n)) + +(define-matcher (annotate:var (? symbol? var) env) + (make-texp (lookup var env) var)) + +(define-matcher (annotate:if ('if predicate consequent alternate) env) + (make-texp (fresh-type-variable) + `(if ,(annotate-exp predicate env) + ,(annotate-exp consequent env) + ,(annotate-exp alternate env)))) + +(define-matcher (annotate:lambda ('lambda ((? symbol? args) ...) body) env) + (define arg-types (map (lambda (_name) (fresh-type-variable)) args)) + (define env* (append (map cons args arg-types) env)) + (define return-type (fresh-type-variable)) + (make-texp (make-procedure-type arg-types return-type) + `(lambda ,args ,(annotate-exp body env*)))) + +(define-matcher (annotate:call (operator args ...) env) + (make-texp (fresh-type-variable) + (cons (annotate-exp operator env) + (map (lambda (arg) (annotate-exp arg env)) args)))) + +(define annotate-exp + (compose-matchers annotate:bool + annotate:int + annotate:float + annotate:var + annotate:if + annotate:lambda + annotate:call)) + +(define (annotate-exp* exp) + (parameterize ((unique-counter 0)) + (annotate-exp exp (top-level-env)))) + + +;;; +;;; Constraints +;;; + +(define-record-type <constraint> + (constrain lhs rhs) + constraint? + (lhs constraint-lhs) + (rhs constraint-rhs)) + +(define (display-constraint constraint port) + (format port "#<constraint ~a = ~a>" + (constraint-lhs constraint) + (constraint-rhs constraint))) +(set-record-type-printer! <constraint> display-constraint) + +(define-matcher (constrain:other (? type? _) _) '()) + +(define-matcher (constrain:if (? type? type) + ('if (? texp? predicate) + (? texp? consequent) + (? texp? alternate))) + (append (list (constrain bool-type (texp-type predicate)) + (constrain type (texp-type consequent)) + (constrain type (texp-type alternate))) + (program-constraints predicate) + (program-constraints consequent) + (program-constraints alternate))) + +(define-matcher (constrain:lambda (? procedure-type? type) + ('lambda ((? symbol? args) ...) + (? texp? body))) + (cons (constrain (procedure-type-return-type type) + (texp-type body)) + (program-constraints body))) + +(define-matcher (constrain:call (? type? type) + ((? texp? operator) (? texp? operands) ...)) + (cons (constrain (texp-type operator) + (make-procedure-type (map texp-type operands) + type)) + (append (program-constraints operator) + (append-map program-constraints operands)))) + +(define %program-constraints + (compose-matchers constrain:if + constrain:lambda + constrain:call + constrain:other)) + +(define (program-constraints texp) + (%program-constraints (texp-type texp) (texp-exp texp))) + + +;;; +;;; Unification +;;; + +(define-matcher (occurs:default _ _) + #f) + +(define-matcher (occurs:variable (? type-variable? a) (? type-variable? b)) + (eq? a b)) + +(define-matcher (occurs:procedure (? type-variable? v) (? procedure-type? p)) + (or (any (lambda (arg-type) + (occurs-in? v arg-type)) + (procedure-type-arg-types p)) + (occurs-in? v (procedure-type-return-type p)))) + +(define occurs-in? + (compose-matchers occurs:variable + occurs:procedure + occurs:default)) + +(define (substitute-term term dict) + (match dict + (() term) + (((from . to) . rest) + (if (eq? term from) + to + (substitute-term term rest))))) + +(define (substitute-dict var term dict) + (map (match-lambda + ((a . b) + (cons (if (eq? a var) term a) + (if (eq? b var) term b)))) + dict)) + +(define (substitute var term dict) + (let ((term* (substitute-term term dict))) + (and (not (occurs-in? var term*)) + (alist-cons var term* (substitute-dict var term* dict))))) + +(define (maybe-substitute var-first terms) + (lambda (dict succeed fail) + (match var-first + ((var . rest-vars) + (match terms + ((term . rest-terms) + (cond + ;; Tautology: matching 2 vars that are the same. + ((and (type-variable? term) (eq? var term)) + (succeed dict fail rest-vars rest-terms)) + ;; Variable has been bound to some other value, recursively + ;; follow it and unify. + ((assq-ref dict var) => + (lambda (type) + ((unify:dispatch (cons type rest-vars) terms) + dict succeed fail))) + ;; Substitute variable for value. + (else + (let ((dict* (substitute var term dict))) + (if dict* + (succeed dict* fail rest-vars rest-terms) + (fail))))))))))) + +(define (constant? obj) + (and (not (type-variable? obj)) + (not (procedure-type? obj)) + (not (list? obj)))) + +(define-matcher (unify:fail a b) + (define (fail-unifier dict succeed fail) + (fail)) + fail-unifier) + +(define-matcher (unify:constants ((? constant? a) . rest-a) ((? constant? b) . rest-b)) + (define (constant-unifier dict succeed fail) + (if (eqv? a b) + (begin + (succeed dict fail rest-a rest-b)) + (fail))) + constant-unifier) + +(define-matcher (unify:lists (a . rest-a) (b . rest-b)) + (define (list-unifier dict succeed fail) + ((unify:dispatch a b) + dict + (lambda (dict* fail* _null-a _null-b) + (succeed dict* fail* rest-a rest-b)) + fail)) + list-unifier) + +(define-matcher (unify:variable-left (and ((? type-variable? _) . _) a) b) + (maybe-substitute a b)) + +(define-matcher (unify:variable-right a (and ((? type-variable? _) . _) b)) + (maybe-substitute b a)) + +(define-matcher (unify:procedures ((? procedure-type? a) . rest-a) + ((? procedure-type? b) . rest-b)) + (define (procedure-unifier dict succeed fail) + ((unify:dispatch (cons (procedure-type-return-type a) + (procedure-type-arg-types a)) + (cons (procedure-type-return-type b) + (procedure-type-arg-types b))) + dict + (lambda (dict* fail* _null-a _null-b) + (succeed dict* fail* rest-a rest-b)) + fail)) + procedure-unifier) + +(define %unify:dispatch + (compose-matchers unify:constants + unify:variable-left + unify:variable-right + unify:procedures + unify:lists + unify:fail)) + +(define (unify:dispatch a b) + (define (dispatcher dict succeed fail) + (if (and (null? a) (null? b)) + (succeed dict fail a b) + ((%unify:dispatch a b) + dict + (lambda (dict* fail* rest-a rest-b) + ((unify:dispatch rest-a rest-b) + dict* succeed fail*)) + fail))) + dispatcher) + +(define (%unify a b dict succeed) + ((unify:dispatch (list a) (list b)) + dict + (lambda (dict fail rest-a rest-b) + (or (and (null? rest-a) (null? rest-b) (succeed dict)) + (fail))) + (lambda () + #f))) + +(define (unify a b) + (%unify a b '() identity)) + +(define (unify-constraints constraints) + (unify (map constraint-lhs constraints) + (map constraint-rhs constraints))) + + +;;; +;;; Type Resolution +;;; + +(define (primitive? x) + (or (number? x) + (boolean? x) + (symbol? x))) + +(define-matcher (resolve:primitive (? primitive? x) dict) + x) + +(define-matcher (resolve:primitive-type (? primitive-type? type) dict) + type) + +(define-matcher (resolve:type-variable (? type-variable? var) dict) + (let ((type (assq-ref dict var))) + (if (or (not type) (type-variable? type)) + (error "cannot determine type" var) + type))) + +(define-matcher (resolve:procedure-type (? procedure-type? type) dict) + (make-procedure-type (resolve-types (procedure-type-arg-types type) dict) + (resolve-types (procedure-type-return-type type) dict))) + +(define-matcher (resolve:list (exps ...) dict) + (map (lambda (texp) (resolve-types texp dict)) exps)) + +(define resolve-types + (compose-matchers resolve:primitive + resolve:primitive-type + resolve:type-variable + resolve:procedure-type + resolve:list)) + +(define (infer-types exp) + (let* ((texp (annotate-exp* exp)) + (constraints (program-constraints texp)) + (substitutions (unify-constraints constraints))) + (unless substitutions + (error "type mismatch" texp)) + (resolve-types texp substitutions))) + +(infer-types #t) +(infer-types 6) +(infer-types 6.5) +(infer-types '(if #t 1 2)) +(infer-types '((lambda (x) x) 1)) +(infer-types '((lambda (f) (if (f #t) (f 1) (f 2))) (lambda (x) x))) |