Some weeks ago I promised to post some unfinished and unpolished
type inference code that I have written in/for R4RS Scheme some
time ago. Thanks to those who reminded me! Here it is.

----->>> snip <<<------------------------------------------------------------- ;;; Hindley-Milner type inference for R4RS Scheme
;;; By Nils M Holm, 2014
;;; In the public domain.

;;; Notes: - CONS, CAR, CDR work on LISTs only!
;;; Use PAIR, LEFT, RIGHT for PAIRs.
;;; - QUASIQUOTE accepts only LIST templates.
;;; - Macros are not really supported.
;;; - Cannot type check LETREC (and named LET)
;;; due to circularity.

;;; Example:
;;; (sig '(define (length x)
;;; (if (null? x)
;;; 0
;;; (+ 1 (length (cdr x)))))) ==> (-> list (u int real))
;;; ; function from list
;;; ; to int or real

;; ----- first some useful functions -----

(define (intersection a b)
(define (isect a b r)
(cond ((null? a) r)
((member (car a) b)
(isect (cdr a) b (cons (car a) r)))
(else
(isect (cdr a) b r))))
(isect a b '()))

(define (flatten x)
(letrec
((f (lambda (x r)
(cond ((null? x)
r)
((pair? x)
(f (car x)
(f (cdr x) r)))
(else
(cons x r))))))
(f x '())))

(define (remq x a)
(letrec
((rem
(lambda (a r)
(cond ((null? a)
(reverse r))
((eq? x (car a))
(rem (cdr a) r))
(else
(rem (cdr a) (cons (car a) r)))))))
(rem a '())))

(define (make-set a)
(letrec
((make-set2
(lambda (a r)
(cond ((null? a)
(reverse r))
((member (car a) r)
(make-set2 (cdr a) r))
(else
(make-set2 (cdr a)
(cons (car a) r)))))))
(make-set2 a '())))

(define (contains? x a)
(cond ((equal? x a))
((pair? a)
(or (contains? x (car a))
(contains? x (cdr a))))
(else
#F)))

(define (list-of? p a)
(cond ((null? a))
((not (pair? a))
#f)((p (car a))
(list-of? p (cdr a)))
(else
#F)))

(define (cond-clause? x)
(and (list? x)
(pair? x)))

(define (let-binding? x)
(and (pair? x)
(pair? (cdr x))
(null? (cddr x))))

(define (do-binding? x)
(and (pair? x)
(pair? (cdr x))
(or (null? (cddr x))
(and (pair? (cddr x))
(null? (cdddr x))))))

(define (case-clause? x)
(and (list? x)
(pair? x)
(pair? (cdr x))))

(define alpha-conv
(let ((c 0))
(lambda (form)
(letrec
((newvar
(lambda (n)
(set! c (+ 1 c))
(string->symbol
(string-append (symbol->string n)
"#"
(number->string c)))))
(subst
(lambda (x env)
(cond ((assq x env) => cdr)
(else x))))
(map-improper
(lambda (f a r)
(cond ((null? a)
(reverse r))
((not (pair? a))
(append (reverse r) (f a)))
(else
(map-improper f (cdr a) (cons (f (car a)) r))))))
(conv
(lambda (form env)
(cond ((symbol? form)
(subst form env))
((not (pair? form))
form)
((and (eq? 'quote (car form))
(pair? (cdr form))
(null? (cddr form)))
form)
((and (eq? 'lambda (car form))
(pair? (cdr form))
(pair? (cddr form)))
(let ((e (map-improper (lambda (x)
(cons x (newvar x)))
(flatten (cadr form))
'())))
`(lambda ,@(conv (cdr form)
(append e env)))))
((and (eq? (car form) 'let)
(pair? (cdr form))
(symbol? (cadr form))
(pair? (cddr form)))
(let* ((e (list (cons (cadr form)
(newvar (cadr form)))))
(x (conv `(let ,@(cddr form))
(append e env))))
`(let ,(cdar e) ,@(cdr x))))
((and (or (eq? (car form) 'let)
(eq? (car form) 'letrec)
(eq? (car form) 'let*)
(eq? (car form) 'do))
(pair? (cdr form))
(pair? (cadr form))
(pair? (caadr form))
(pair? (cddr form)))
(let ((e (map-improper (lambda (x)
(cons x (newvar x)))
(map (lambda (x)
(if (pair? x) (car x) #f))
(cadr form))
'())))
`(,(car form) ,@(conv (cdr form)
(append e env)))))
(else
(map-improper (lambda (x) (conv x env))
form
'()))))))
(conv form '())))))

;; ----- type definitions ------

(define (type . x) (cons 'T x))

(define type-name cadr)

(define (type? x)
(and (pair? x)
(eq? 'T (car x))))

(define t-bool (type 'bool))
(define t-char (type 'char))
(define t-inpp (type 'input-port))
(define t-int (type 'int))
(define t-list (type 'list))
(define t-mac (type 'macro))
(define t-outp (type 'output-port))
(define t-pair (type 'pair))
(define t-real (type 'real))
(define t-same (type 'same))
(define t-str (type 'string))
(define t-sym (type 'symbol))
(define t-vec (type 'vector))
(define t-void (type 'void))

(define (arrow x . v*)
(append (cons '-> v*) (list x)))

(define (arrow? x)
(and (pair? x)
(eq? '-> (car x))))

(define (same? x)
(and (type? x)
(eq? 'same (type-name x))))

(define (U . x) (cons 'U x))

(define u-members cdr)

(define (union? x)
(and (pair? x)
(eq? 'U (car x))))

(define (polymorphic? x)
(and (pair? x)
(eq? 'P (car x))))

(define poly-sigs cdr)

(define t-num (U t-int t-real))
(define t-?list (U t-list t-bool))
(define t-vfun (arrow ''b ''? '...))

;; ----- constraint generator ------

(define (var x)
(list 'var x))

(define (var? x)
(and (pair? x)
(eq? 'var (car x))))

(define (intrinsic-constraints)
(let*
((C '())
(C `(((var *) (-> ,t-num ... ,t-num )) ,@C))
(C `(((var +) (-> ,t-num ... ,t-num )) ,@C))
(C `(((var -) (-> ,t-num ,t-num ,t-num ... ,t-num )) ,@C))
(C `(((var /) (-> ,t-num ,t-num ,t-num ... ,t-real )) ,@C))
(C `(((var <) (-> ,t-num ,t-num ,t-num ... ,t-bool )) ,@C))
(C `(((var <=) (-> ,t-num ,t-num ,t-num ... ,t-bool )) ,@C))
(C `(((var =) (-> ,t-num ,t-num ,t-num ... ,t-bool )) ,@C))
(C `(((var >) (-> ,t-num ,t-num ,t-num ... ,t-bool )) ,@C))
(C `(((var >=) (-> ,t-num ,t-num ,t-num ... ,t-bool )) ,@C))
(C `(((var abs) (-> ,t-num ,t-num )) ,@C))
(C `(((var append) (-> ,t-list ... ,t-list )) ,@C))
(C `(((var apply) (-> ,t-vfun '? ... ,t-list 'b )) ,@C))
(C `(((var assoc) (-> 'a ,t-list ,t-?list)) ,@C))
(C `(((var assq) (-> 'a ,t-list ,t-?list)) ,@C))
(C `(((var assv) (-> 'a ,t-list ,t-?list)) ,@C))
(C `(((var boolean?) (-> 'a ,t-bool )) ,@C))
(C `(((var caaaar) (-> ,t-list 'a )) ,@C))
(C `(((var caaadr) (-> ,t-list 'a )) ,@C))
(C `(((var caaar) (-> ,t-list 'a )) ,@C))
(C `(((var caadar) (-> ,t-list 'a )) ,@C))
(C `(((var caaddr) (-> ,t-list 'a )) ,@C))
(C `(((var caadr) (-> ,t-list 'a )) ,@C))
(C `(((var caar) (-> ,t-list 'a )) ,@C))
(C `(((var cadaar) (-> ,t-list 'a )) ,@C))
(C `(((var cadadr) (-> ,t-list 'a )) ,@C))
(C `(((var cadar) (-> ,t-list 'a )) ,@C))
(C `(((var caddar) (-> ,t-list 'a )) ,@C))
(C `(((var cadddr) (-> ,t-list 'a )) ,@C))
(C `(((var caddr) (-> ,t-list 'a )) ,@C))
(C `(((var cadr) (-> ,t-list 'a )) ,@C))
(C `(((var call-with-current-continuation)
(-> (-> (-> 'a 'b) 'c) 'd )) ,@C))
(C `(((var call-with-input-file)
(-> ,t-str (-> ,t-inpp 'a) 'a )) ,@C))
(C `(((var call-with-output-file)
(-> ,t-str (-> ,t-outp 'a) 'a )) ,@C))
(C `(((var call/cc) (-> (-> (-> 'a 'b) 'c) 'd )) ,@C))
(C `(((var car) (-> ,t-list 'a )) ,@C))
(C `(((var cdaaar) (-> ,t-list 'a )) ,@C))
(C `(((var cdaadr) (-> ,t-list 'a )) ,@C))
(C `(((var cdaar) (-> ,t-list 'a )) ,@C))
(C `(((var cdadar) (-> ,t-list 'a )) ,@C))
(C `(((var cdaddr) (-> ,t-list 'a )) ,@C))
(C `(((var cdadr) (-> ,t-list 'a )) ,@C))
(C `(((var cdar) (-> ,t-list 'a )) ,@C))
(C `(((var cddaar) (-> ,t-list 'a )) ,@C))
(C `(((var cddadr) (-> ,t-list 'a )) ,@C))
(C `(((var cddar) (-> ,t-list 'a )) ,@C))
(C `(((var cdddar) (-> ,t-list 'a )) ,@C))
(C `(((var cddddr) (-> ,t-list 'a )) ,@C))
(C `(((var cdddr) (-> ,t-list 'a )) ,@C))
(C `(((var cddr) (-> ,t-list 'a )) ,@C))
(C `(((var cdr) (-> ,t-list ,t-list )) ,@C))
(C `(((var char->integer)
(-> ,t-char ,t-int )) ,@C))
(C `(((var char-alphabetic?)
(-> ,t-char ,t-bool )) ,@C))
(C `(((var char-ci<=?)
(-> ,t-char ... ,t-bool )) ,@C))
(C `(((var char-ci<?)
(-> ,t-char ... ,t-bool )) ,@C))
(C `(((var char-ci=?)
(-> ,t-char ... ,t-bool )) ,@C))
(C `(((var char-ci>=?)
(-> ,t-char ... ,t-bool )) ,@C))
(C `(((var char-ci>?)
(-> ,t-char ... ,t-bool )) ,@C))
(C `(((var char-downcase)
(-> ,t-char ,t-char )) ,@C))
(C `(((var char-lower-case?)
(-> ,t-char ,t-bool )) ,@C))
(C `(((var char-numeric?)
(-> ,t-char ,t-bool )) ,@C))
(C `(((var char-upcase)
(-> ,t-char ,t-char )) ,@C))
(C `(((var char-upper-case?)
(-> ,t-char ,t-bool )) ,@C))
(C `(((var char-whitespace?)
(-> ,t-char ,t-bool )) ,@C))
(C `(((var char<=?) (-> ,t-char ,t-char ,t-char ... ,t-bool )) ,@C))
(C `(((var char<?) (-> ,t-char ,t-char ,t-char ... ,t-bool )) ,@C))
(C `(((var char=?) (-> ,t-char ,t-char ,t-char ... ,t-bool )) ,@C))
(C `(((var char>=?) (-> ,t-char ,t-char ,t-char ... ,t-bool )) ,@C))
(C `(((var char>?) (-> ,t-char ,t-char ,t-char ... ,t-bool )) ,@C))
(C `(((var char?) (-> 'a ,t-bool )) ,@C))
(C `(((var close-input-port)
(-> ,t-inpp ,t-void )) ,@C))
(C `(((var close-output-port)
(-> ,t-outp ,t-void )) ,@C))
(C `(((var cons) (-> 'a ,t-list ,t-list )) ,@C))
(C `(((var current-input-port)
(-> ,t-inpp )) ,@C))
(C `(((var current-output-port)
(-> ,t-outp )) ,@C))
(C `(((var delay) (-> 'a (-> 'a) )) ,@C))
(C `(((var display)
(P (-> 'a ,t-void )
(-> 'a ,t-outp ,t-void ))),@C))
(C `(((var eof-object?)
(-> 'a ,t-bool )) ,@C))
(C `(((var eq?) (-> 'a 'b ,t-bool )) ,@C))
(C `(((var eqv?) (-> 'a 'b ,t-bool )) ,@C))
(C `(((var equal?) (-> 'a 'b ,t-bool )) ,@C))
(C `(((var even?) (-> ,t-int ,t-bool )) ,@C))
(C `(((var exact->inexact)
(-> ,t-num ,t-real )) ,@C))
(C `(((var exact?) (-> ,t-num ,t-bool )) ,@C))
(C `(((var expt) (-> ,t-num ,t-num ,t-num )) ,@C))
(C `(((var floor) (-> ,t-num ,t-num )) ,@C))
(C `(((var for-each) (-> ,t-vfun ,t-list ,t-list ... ,t-void )) ,@C))
(C `(((var force) (-> (-> 'a) 'a )) ,@C))
(C `(((var gcd) (-> ,t-int ... ,t-int )) ,@C))
(C `(((var inexact->exact)
(-> ,t-num ,t-int )) ,@C))
(C `(((var inexact?) (-> ,t-num ,t-bool )) ,@C))
(C `(((var input-port?)
(-> 'a ,t-bool )) ,@C))
(C `(((var integer->char)
(-> ,t-int ,t-char )) ,@C))
(C `(((var integer?) (-> 'a ,t-bool )) ,@C))
(C `(((var lcm) (-> ,t-int ... ,t-int )) ,@C))
(C `(((var left) (-> ,t-pair 'a )) ,@C))
(C `(((var length) (-> ,t-list ,t-int )) ,@C))
(C `(((var list) (-> '? ... ,t-list )) ,@C))
(C `(((var list->string)
(-> ,t-list ,t-str )) ,@C))
(C `(((var list->vector)
(-> ,t-list ,t-vec )) ,@C))
(C `(((var list-ref) (-> ,t-list ,t-int 'a )) ,@C))
(C `(((var list-tail)
(-> ,t-list ,t-int ,t-list )) ,@C))
(C `(((var list?) (-> 'a ,t-bool )) ,@C))
(C `(((var load) (-> ,t-str ,t-void )) ,@C))
(C `(((var make-string)
(-> ,t-char ... ,t-str )) ,@C))
(C `(((var make-vector)
(-> '? ... ,t-vec )) ,@C))
(C `(((var map) (-> ,t-vfun ,t-list ,t-list ... ,t-list )) ,@C))
(C `(((var max) (-> ,t-num ,t-num ... ,t-num )) ,@C))
(C `(((var member) (-> 'a ,t-list ,t-?list)) ,@C))
(C `(((var memq) (-> 'a ,t-list ,t-?list)) ,@C))
(C `(((var memv) (-> 'a ,t-list ,t-?list)) ,@C))
(C `(((var min) (-> ,t-num ,t-num ... ,t-num )) ,@C))
(C `(((var modulo) (-> ,t-int ,t-int ,t-int )) ,@C))
(C `(((var negative?)
(-> ,t-num ,t-bool )) ,@C))
(C `(((var newline)
(P (-> ,t-void )
(-> ,t-outp ,t-void ))),@C))
(C `(((var not) (-> 'a ,t-bool )) ,@C))
(C `(((var null?) (-> 'a ,t-bool )) ,@C))
(C `(((var number->string)
(P (-> ,t-num ,t-str )
(-> ,t-num ,t-int ,t-str ))),@C))
(C `(((var number?) (-> 'a ,t-bool )) ,@C))
(C `(((var odd?) (-> ,t-int ,t-bool )) ,@C))
(C `(((var open-input-file)
(-> ,t-str ,t-inpp )) ,@C))
(C `(((var open-output-file)
(-> ,t-str ,t-outp )) ,@C))
(C `(((var output-port?)
(-> 'a ,t-bool )) ,@C))
(C `(((var pair) (-> 'a 'b ,t-pair )) ,@C))
(C `(((var pair?) (-> 'a ,t-bool )) ,@C))
(C `(((var peek-char)
(P (-> ,t-char )
(-> ,t-inpp ,t-char ))),@C))
(C `(((var positive?)
(-> ,t-num ,t-bool )) ,@C))
(C `(((var procedure?)
(-> ,t-num ,t-bool )) ,@C))
(C `(((var quotient) (-> ,t-int ,t-int ,t-int )) ,@C))
(C `(((var read) (P (-> 'a )
(-> ,t-inpp 'a ))),@C))
(C `(((var read-char)
(P (-> ,t-char )
(-> ,t-inpp ,t-char ))),@C))
(C `(((var real?) (-> 'a ,t-bool )) ,@C))
(C `(((var remainder)
(-> ,t-int ,t-int ,t-int )) ,@C))
(C `(((var reverse) (-> ,t-list ,t-list )) ,@C))
(C `(((var right) (-> ,t-pair 'a )) ,@C))
(C `(((var set!) (-> 'a 'b ,t-void )) ,@C))
(C `(((var set-car!) (-> ,t-list 'a ,t-void )) ,@C))
(C `(((var set-cdr!) (-> ,t-list 'a ,t-void )) ,@C))
(C `(((var string) (-> ,t-char ... ,t-str )) ,@C))
(C `(((var string->list)
(-> ,t-str ,t-list )) ,@C))
(C `(((var string->number)
(P (-> ,t-str ,t-num )
(-> ,t-str ,t-int ,t-num ))),@C))
(C `(((var string->symbol)
(-> ,t-str ,t-sym )) ,@C))
(C `(((var string-append)
(-> ,t-str ... ,t-str )) ,@C))
(C `(((var string-ci<=?)
(-> ,t-str ,t-str ,t-bool )) ,@C))
(C `(((var string-ci<?)
(-> ,t-str ,t-str ,t-bool )) ,@C))
(C `(((var string-ci=?)
(-> ,t-str ,t-str ,t-bool )) ,@C))
(C `(((var string-ci>=?)
(-> ,t-str ,t-str ,t-bool )) ,@C))
(C `(((var string-ci>?)
(-> ,t-str ,t-str ,t-bool )) ,@C))
(C `(((var string-copy)
(-> ,t-str ,t-str )) ,@C))
(C `(((var string-fill!)
(-> ,t-str ,t-char ,t-str )) ,@C))
(C `(((var string-length)
(-> ,t-str ,t-int )) ,@C))
(C `(((var string-ref)
(-> ,t-str ,t-int ,t-char )) ,@C))
(C `(((var string-set!)
(-> ,t-str ,t-int ,t-char ,t-char )) ,@C))
(C `(((var string<=?)
(-> ,t-str ,t-str ,t-bool )) ,@C))
(C `(((var string<?) (-> ,t-str ,t-str ,t-bool )) ,@C))
(C `(((var string=?) (-> ,t-str ,t-str ,t-bool )) ,@C))
(C `(((var string>=?)
(-> ,t-str ,t-str ,t-bool )) ,@C))
(C `(((var string>?) (-> ,t-str ,t-str ,t-bool )) ,@C))
(C `(((var string?) (-> 'a ,t-bool )) ,@C))
(C `(((var substring)
(-> ,t-str ,t-int ,t-int ,t-str )) ,@C))
(C `(((var symbol->string)
(-> ,t-sym ,t-str )) ,@C))
(C `(((var symbol?) (-> 'a ,t-bool )) ,@C))
(C `(((var vector) (-> '? ... ,t-vec )) ,@C))
(C `(((var vector->list)
(-> ,t-vec ,t-list )) ,@C))
(C `(((var vector-fill!)
(-> ,t-vec ,t-int 'a ,t-void )) ,@C))
(C `(((var vector-length)
(-> ,t-vec ,t-int )) ,@C))
(C `(((var vector-ref)
(-> ,t-vec ,t-int 'a )) ,@C))
(C `(((var vector-set!)
(-> ,t-vec ,t-int 'a ,t-char )) ,@C))
(C `(((var vector?) (-> 'a ,t-bool )) ,@C))
(C `(((var with-input-from-file)
(-> ,t-str (-> 'a) 'a )) ,@C))
(C `(((var with-output-to-file)
(-> ,t-str (-> 'a) 'a )) ,@C))
(C `(((var write) (P (-> 'a ,t-void )
(-> 'a t-outp ,t-void ))),@C))
(C `(((var write-char)
(P (-> ,t-char ,t-void )
(-> ,t-char ,t-outp ,t-void ))),@C))
(C `(((var zero?) (-> 'a ,t-bool )) ,@C))
(C C))
C))

(define (con l r) (list l r))
(define con-lhs car)
(define con-rhs cadr)

(define (args? x atomic)
(if (symbol? x)
atomic
(or (null? x)
(let loop ((x x))
(cond ((null? x))
((symbol? x))
((and (pair? x)
(symbol? (car x)))
(loop (cdr x)))
(else #f))))))

(define (last-arg x)
(cond ((null? x)
t-void)
((null? (cdr x))
(car x))
(else
(last-arg (cdr x)))))

(define (type-of x)
(cond ((boolean? x) t-bool)
((char? x) t-char)
((integer? x) t-int)
((null? x) t-list)
((list? x) t-list)
((pair? x) t-pair)
((real? x) t-real)
((string? x) t-str)
((vector? x) t-vec)
((symbol? x) t-sym)
(else (error "type-of" x))))

(define (improper-args a)
(let loop ((a a)
(r '()))
(if (symbol? a)
(reverse (cons '... (cons (type-var #t) r)))
(loop (cdr a) (cons (var (car a)) r)))))

(define (make-lambda-con x)
(append (make-constraints (cons 'begin (cddr x)))
(list (con (var x)
(apply arrow
(var (last-arg x))
(if (list? (cadr x))
(map var (cadr x))
(improper-args (cadr x))))))))

(define (make-bind-con x)
(let* ((vars (map car (cadr x)))
(args (map cadr (cadr x)))
(dx `((lambda ,vars ,@(cddr x)) ,@args)))
(append (make-constraints dx)
(list (con (var x) (var dx))))))

(define (make-named-let-con x)
(let* ((vars (map car (caddr x)))
(args (map cadr (caddr x)))
(dx `((lambda ,vars ,@(cdddr x)) ,@args)))
(append (make-constraints dx)
(list (con (var (cadr x))
(apply arrow
(var (last-arg x))
(map var vars)))
(con (var x) (var dx))))))

(define (make-begin-con x)
(append (apply append (map make-constraints (cdr x)))
(list (con (var x) (var (last-arg x))))))

(define (make-and/or-con x)
(append (apply append (map make-constraints (cdr x)))
(list (con (var x) (apply U (map var (cdr x)))))))

(define (make-if-con x)
(append (apply append (map make-constraints (cdr x)))
(list (con (var x)
(U (var (caddr x))
(var (cadddr x)))))))

(define (make-cond-con x)
(if (null? (cdr x))
(list (con (var x) t-void))
(append (apply append (map (lambda (x)
(make-constraints
(cons 'begin x)))
(cdr x)))
(list (con (var x)
(apply U (map (lambda (x)
(var (last-arg x)))
(cdr x))))))))

(define (make-case-con x)
(if (null? (cddr x))
(list (con (var x) t-void))
(append (make-constraints (cadr x))
(apply append (map (lambda (x)
(make-constraints
(cons 'begin (cdr x))))
(cddr x)))
(list (con (var x)
(apply U (map (lambda (x)
(var (last-arg x)))
(cddr x))))))))

(define (make-do-con x)
(let ((vars (map car (cadr x)))
(args (map cadr (cadr x)))
(ops (map (lambda (x)
(if (null? (cddr x))
(car x)
(caddr x)))
(cadr x)))
(test (caddr x))
(body (cdddr x)))
(append (map (lambda (v a)
(con (var v) (var a)))
vars
args)
(apply append (map make-constraints args))
(apply append (map make-constraints ops))
(make-constraints (cons 'begin body))
(make-constraints (cons 'begin test))
(list (con (var x) (var (last-arg (caddr x))))))))

(define (make-qq-con x)
(append (let unquoted ((x x))
(cond ((and (pair? x)
(or (eq? 'unquote (car x))
(eq? 'unquote-splicing (car x))))
(make-constraints (cadr x)))
((pair? x)
(append (unquoted (car x))
(unquoted (cdr x))))
(else
'())))
(list (con (var x) t-list))))

(define (transform-define x)
(let ((dx `(,(car x) ,(caadr x) (lambda ,(cdadr x) ,@(cddr x)))))
(append (make-constraints dx)
(list (con (var x) (var dx))))))

(define (make-define-con x)
(append (make-constraints (caddr x))
(list (con (var x)
(var (caddr x)))
(con (var (cadr x))
(var (caddr x))))))

(define (make-syntax-con x)
(append (list (con (var x)
t-mac)
(con (var (cadr x))
t-mac))))

(define (make-application-con x)
(append (apply append (map make-constraints x))
(list (con (var (car x))
(apply arrow
(var x)
(map var (cdr x)))))))

(define (make-constraints x)
(cond ((symbol? x) ; symbol
'())
((null? x) ; nil
'())
((and (pair? x) ; (quote obj)
(eq? 'quote (car x))
(pair? (cdr x))
(null? (cddr x)))
(list (con (var x)
(type-of (cadr x)))))
((and (pair? x) ; (lambda args expr ...)
(eq? 'lambda (car x))
(pair? (cdr x))
(args? (cadr x) #t)
(pair? (cddr x)))
(make-lambda-con x))
((and (pair? x) ; (let bindings expr ...)
(or (eq? 'let (car x)) ; (let* bindings expr ...)
(eq? 'let* (car x)) ; (letrec bindings expr ...)
(eq? 'letrec (car x)))
(list-of? let-binding? (cadr x))
(pair? (cddr x)))
(make-bind-con x))
((and (pair? x) ; (let name binds expr ...)
(eq? 'let (car x))
(symbol? (cadr x))
(list-of? let-binding? (caddr x))
(pair? (cdddr x)))
(make-named-let-con x))
((and (pair? x) ; (begin ...)
(eq? 'begin (car x)))
(make-begin-con x))
((and (pair? x) ; (and ...)
(or (eq? 'and (car x)) ; (or ...)
(eq? 'or (car x))))
(make-and/or-con x))
((and (pair? x) ; (if pred conseq alt)
(eq? 'if (car x))
(pair? (cdr x))
(pair? (cddr x))
(pair? (cdddr x))
(null? (cddddr x)))
(make-if-con x))
((and (pair? x) ; (cond clause ...)
(eq? 'cond (car x))
(list-of? cond-clause? (cdr x)))
(make-cond-con x))
((and (pair? x) ; (case clause ...)
(eq? 'case (car x))
(pair? (cdr x))
(list-of? case-clause? (cddr x)))
(make-case-con x))
((and (pair? x) ; (do binds test expr ...)
(eq? 'do (car x))
(list-of? do-binding? (cadr x))
(cond-clause? (cadr x))
(pair? (cddr x)))
(make-do-con x))
((and (pair? x)
(eq? 'quasiquote (car x))
(pair? (cdr x))
(list? (cadr x))
(null? (cddr x)))
(make-qq-con x))
((and (pair? x) ; (define (f a ...) x ...)
(eq? 'define (car x))

[continued in next message]

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Nils M Holm <nmh@ananda.local> wrote:

Some weeks ago I promised to post some unfinished and unpolished
type inference code that I have written in/for R4RS Scheme some
time ago. Thanks to those who reminded me! Here it is.

Here is another example (higher-order MAPCAR function);

(sig '(define (m f a)
(if (null? a)
'()
(cons (f (car a))
(m f (cdr a)))))) ==> (-> (-> 'b 'a) list list)

--
Nils M Holm < n m h @ t 3 x . o r g > www.t3x.org

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)