Pop-Up Thingie
Sidebar
>>> Magnum BBS <<<
Home
Forum
Files
Dark
Log in
Username
Password
Sidebar
Forum
Usenet
COMP.LANG.SCHEME
Type inference fotr R4RS Scheme (2/2)
From
Nils M Holm
@21:1/5 to
All
on Sat Sep 26 10:23:22 2020
[continued from previous message]
(pair? (cdr x))
(args? (cadr x) #f)
(pair? (cddr x)))
(transform-define x))
((and (pair? x) ; (define name expr)
(eq? 'define (car x))
(pair? (cdr x))
(symbol? (cadr x))
(pair? (cddr x))
(null? (cdddr x)))
(make-define-con x))
((and (pair? x) ; define-syntax
(eq? 'define-syntax (car x))
(pair? (cdr x))
(symbol? (cadr x))
(pair? (cddr x)))
(make-syntax-con x))
((list? x) ; (fun arg ...)
(make-application-con x))
((or (boolean? x) ; atom
(char? x)
(integer? x)
(null? x)
(pair? x)
(real? x)
(string? x)
(vector? x))
(list (con (var x) (type-of x))))
(else
(error "make-constraints" x))))
(define (constraints x s0)
(let ((xa (alpha-conv x)))
(append (intrinsic-constraints)
s0
(make-constraints xa)
(list (con (var xa) (var x))))))
;; ----- constraint solver (unifier) ------
(define (lookup x s)
(if (var? x)
(let ((b (assoc x s)))
(if b
(if (eq? (cadr b) x)
x
(lookup (cadr b) s))
x))
x))
(define (extend l r s)
(cons (list l r) s))
(define (fail msg x y)
(list #F msg x y))
(define (mismatch x y)
(fail "type mismatch" x y))
(define (not-unifiable x y)
(fail "unification failed" x y))
(define (failed? x)
(and (pair? x)
(not (car x))))
(define (fix-arity a b)
(define (multiply x n)
(let loop ((r '())
(n n))
(if (positive? n)
(loop (cons x r) (- n 1))
r)))
(let* ((k (+ 2 (- (length b) (length a)))))
(let loop ((a a)
(r '()))
(if (eq? '... (cadr a))
(append (reverse r) (multiply (car a) k) (cddr a))
(loop (cdr a) (cons (car a) r))))))
(define type-var
(let ((c 0))
(lambda (new)
(if new (set! c (+ 1 c)))
(var (string->symbol (string-append "_." (number->string c)))))))
(define (instantiate fun)
(let ((var-map '()))
(define (inst fun)
(map (lambda (x)
(cond ((arrow? x)
(inst x))
((and (pair? x)
(eq? 'quote (car x))
(pair? (cdr x)))
(cond ((eq? '? (cadr x))
(type-var #t))
((assq (cadr x) var-map) => cdr)
(else
(let ((t (type-var #t)))
(set! var-map (cons (cons (cadr x) t) var-map))
t))))
((same? x)
(type-var #F))
(else
x)))
fun))
(inst fun)))
(define (flatten-unions x)
(cond ((null? x) x)
((and (pair? x)
(eq? 'U (car x)))
(let ((u (cons 'U (make-set
(remq 'T (remq 'U (flatten (cdr x))))))))
(if (null? (cddr u))
(apply type (u-members u))
u)))
((pair? x)
(cons (flatten-unions (car x))
(flatten-unions (cdr x))))
(else
x)))
(define (union-member? x a)
(and (memq (type-name x) (flatten-unions a)) #t))
(define (common-members? a b)
(not (null? (intersection (flatten-unions a) (flatten-unions b)))))
(define (unify lcon subst)
(if (null? lcon)
subst
(let ((lv (con-lhs (car lcon)))
(rv (con-rhs (car lcon))))
(let* ((l (lookup lv subst))
(r (lookup rv subst))
(l (if (union? l)
(map (lambda (x) (lookup x subst)) l)
l))
(r (if (union? r)
(map (lambda (x) (lookup x subst)) r)
r)))
(cond ((var? l)
(unify (cdr lcon) (extend l r subst)))
((var? r)
(unify (cdr lcon) (extend r l subst)))
((polymorphic? l)
(let try ((p (poly-sigs l)))
(if (null? p)
(mismatch lv rv)
(let ((nsubst (unify (list (con (car p) r)) subst)))
(if (failed? nsubst)
(try (cdr p))
nsubst)))))
((polymorphic? r)
(let try ((p (poly-sigs r)))
(if (null? p)
(mismatch lv rv)
(let ((nsubst (unify (list (con l (car p))) subst)))
(if (failed? nsubst)
(try (cdr p))
nsubst)))))
((and (arrow? l)
(arrow? r))
(let* ((l (if (memq '... l) (fix-arity l r) l))
(r (if (memq '... r) (fix-arity r l) r)))
(let ((l (instantiate l))
(r (instantiate r)))
(if (not (= (length l) (length r)))
(mismatch lv rv)
(unify (append (map con (cdr l) (cdr r))
(cdr lcon))
subst)))))
((and (union? l)
(union? r))
(if (common-members? (u-members l) (u-members r))
(unify (cdr lcon) subst)
(mismatch lv rv)))
((union? l)
(if (union-member? r l)
(unify (cdr lcon) subst)
(mismatch lv rv)))
((union? r)
(if (union-member? l r)
(unify (cdr lcon) subst)
(mismatch lv rv)))
((and (type? l)
(type? r))
(if (eq? (type-name l) (type-name r))
(unify (cdr lcon) subst)
(mismatch lv rv)))
(else
(not-unifiable `(,lv ,(rename-vars l))
`(,rv ,(rename-vars r)))))))))
;; ----- query interface ------
(define (resolve x s)
(call-with-current-continuation
(lambda (exit)
(define (res x)
(cond ((var? x)
(let ((b (lookup x s)))
(cond ((and (not (equal? x b))
(contains? x b))
(exit (fail "circular" x b)))
((and (var? b)
(eq? (cadr b) (cadr x)))
(var (cadr x)))
(else
(res b)))))
((pair? x)
(cons (res (car x)) (res (cdr x))))
(else
x)))
(instantiate (flatten-unions (res x))))))
(define (rename-vars x)
(define tvar
(let ((c (char->integer #\a)))
(lambda ()
(let ((n c))
(set! c (+ 1 c))
(list 'quote (string->symbol
(string (integer->char n))))))))
(define dict '())
(define (rename x)
(cond ((var? x)
(cond ((assoc x dict)
=> cdr)
(else
(let ((t (tvar)))
(set! dict (cons (cons x t) dict))
t))))
((type? x)
(type-name x))
((pair? x)
(cons (rename (car x))
(rename (cdr x))))
(else
x)))
(rename x))
(define (infer x s0)
(unify (constraints x s0) '()))
(define (query x s)
(resolve (lookup (var x) s) s))
(define (query/r x s)
(let ((res (query x s)))
(if (failed? res)
res
(rename-vars res))))
(define (type-signature x s0)
(let ((subst (infer x s0)))
(if (failed? subst)
subst
(query/r x subst))))
(define (sig x)
(type-signature x '()))
(define (definition-name x)
(and (pair? x)
(eq? 'define (car x))
(pair? (cdr x))
(or (and (symbol? (cadr x))
(cadr x))
(and (pair? (cadr x))
(caadr x)))))
(define (new-con x t)
(let ((v (definition-name x)))
(if v
(list (con (var v) t))
t)))
(define (type-check-program)
(let loop ((x (read))
(s '()))
(if (not (eof-object? x))
(let ((t (type-signature x s))
(n (definition-name x)))
(if n
(begin (display n)
(display " :: ")
(display t)
(newline)))
(loop (read)
(new-con x t))))))
; (display (sig '(define (length x)
; (if (null? x)
; 0
; (+ 1 (length (cdr x)))))) )
; (newline)
----->>> snip <<<-------------------------------------------------------------
--
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)
Who's Online
Recent Visitors
Michal Wronka
Wed Apr 24 14:13:57 2024
from
Wroclaw, Poland
via
SSH
Michal Wronka
Wed Apr 24 14:02:51 2024
from
Wroclaw, Poland
via
SSH
Michal Wronka
Thu Apr 25 14:02:21 2024
from
Wroclaw, Poland
via
SSH
Bob Worm
Thu Apr 25 11:52:12 2024
from
Wales, Uk
via
Telnet
System Info
Sysop:
Keyop
Location:
Huddersfield, West Yorkshire, UK
Users:
296
Nodes:
16 (
3
/
13
)
Uptime:
51:28:14
Calls:
6,650
Calls today:
2
Files:
12,200
Messages:
5,330,304