雑に型推論するものを書いたぞ。

方程式を導出してそれを解くということをしただけ。

サポートする構文、組み込み関数

構文
ifとfunとlambda(1つ以上の引数関数の糖衣構文として)

(if bool a a)
(fun x body)
(lambda (x1 x2 ... ) body)

組み込み関数
succ + zero? の3つだけ。

例

関数適用
(zero? (+ 1 2))
;boolean

整数をいれて、2加えて返す関数
(fun a (succ (succ a))) 
;integer -> integer

多相型
(fun a a)
;T4 -> T4

ifの型推論
(lambda (a b)(if a 1 b))       
;boolean -> integer -> integer

合成関数
(lambda (a b)(fun x (a (b x))))
;(T10 -> T11) -> (T9 -> T10) -> T9 -> T11

雑なソースコード

;-----------------------------------------------------
;
;             data
;
;-----------------------------------------------------


(define builtin-functions
  '((succ . (function . (integer . integer)))
    (+ . (function . (integer . (function . (integer . integer)))))
    (zero? . (function . (integer . boolean)))))
  




;-----------------------------------------------------
;
;             curry
;
;-----------------------------------------------------


(define (lmd-to-curry-fun code)
  (let ((param (cadr code))
        (body (caddr code)))
    (let loop ((p param))
        (if (null? p)
          body
          `(fun ,(car p) ,(loop (cdr p)))))))

(define (curry-apply code)
  (let loop ((args (reverse (cdr code))))
    (if (null? (cdr args))
      `(,(car code) ,(car args))
      `(,(loop (cdr args)) ,(car args)))))



(define (test-convert code)
  (if (pair? code)
    (case (car code) 

      ((lambda) 
         (let ((body (test-convert (caddr code))))
           (lmd-to-curry-fun `(lambda ,(cadr code) ,body))))

      ((fun) 
       (let ((body (test-convert (caddr code))))
         `(fun ,(cadr code) ,body)))

      ((if)
       (let ((test (test-convert (cadr code)))
             (true (test-convert (caddr code)))
             (false (test-convert (cadddr code))))
         `(if ,test ,true ,false)))

      (else 
        (let ((args (map test-convert (cdr code)))
              (f (test-convert (car code))))
                (curry-apply (cons f args)))))
    code))




;-----------------------------------------------------
;
;             type inference
;
;-----------------------------------------------------


(define extract #f)
(let ((type-vars 0))
  (define (publish-type-vars)
    (set! type-vars (+ type-vars 1))
    (cons 'type-var type-vars))
  (define (catch-type env sym)
    (cond ((assv sym env) => cdr)
    (else (display "ERROR::unbound variable ")(display sym)(display "   env=")(display env)(newline))))
  (set! extract
    (lambda (env code)
      (cond 
        ((integer? code) '(() . integer))
        ((boolean? code) '(() . boolean))
        ((symbol? code) (cons '() (catch-type env code)))
        ((eqv? (car code) 'if)
          (let* ((et1 (extract env (cadr code)))
                 (et2 (extract env (caddr code)))
                 (et3 (extract env (cadddr code))))
            (let ((e4 (append 
                          (car et1) 
                          (car et2) 
                          (car et3)
                        (list (cons (cdr et1) 'boolean)
                              (cons (cdr et2) (cdr et3))))))
              (cons e4 (cdr et2)))))
        ((eqv? (car code) 'fun)
         (let ((t (publish-type-vars)))
           (let ((et0 (extract (cons (cons (cadr code) t) env) (caddr code))))
             (cons (car et0) (cons 'function (cons t (cdr et0)))))))
        (else
          (let* ((et1 (extract env (car code)))
                 (et2 (extract env (cadr code))))
            (let ((t (publish-type-vars)))
              (let ((e3 (append
                          (car et1) 
                          (car et2)
                          (list (cons (cdr et1) (cons 'function (cons  (cdr et2) t)))))))
                (cons e3 t)))))
        ))))







(define (expand obj env)
  (cond 
    ((type-var? obj) 
       => (lambda (id) 
            (let loop ((p env)) 
              (cond 
                ((null? p) obj)
                ((eqv? id (caar p))(cdar p))
                (else (loop (cdr p)))))))
    (else obj)))
    

(define (expand-rec obj env)
    (cond 
      ((symbol? obj) obj)
      ((type-var? obj)
       (let ((expanded-obj (expand obj env)))
         (if (and (type-var? expanded-obj) (eqv? (type-var? expanded-obj)(type-var? obj)))
           expanded-obj
           (expand-rec expanded-obj env))))
      ((eqv? (car obj) 'function)
       `(function . (,(expand-rec (cadr obj) env) . ,(expand-rec (cddr obj) env))))
      (else obj)))
                


(define (unify e equations)
  (cond 
    ((null? equations) e)
    ((null? (car equations)) (unify e (cdr equations)))
    (else
      (let ((left (expand (caar equations) e))
            (right (expand (cdar equations) e)))
        (cond
          ((equal? left right) (unify e (cdr equations)))
          ((and (not (type-var? right)) (type-var? left) )
            => (lambda (id) (unify (cons (cons id right) e) (cdr equations))))
          ((and (not (type-var? left)) (type-var? right))
            => (lambda (id) (unify (cons (cons id left) e) (cdr equations))))
          ((and (pair? left)(pair? right) (eqv? (car left) 'function) (eqv? (car right) 'function))
           (unify e `(,(cons (cadr left)(cadr right)) ,(cons (cddr left)(cddr right)) . ,(cdr equations))))
          (else  (display "TYPE ERROR")(newline)))))))

          
        
(define (type-var? o)
  (and (pair? o)(eqv? (car o) 'type-var)(cdr o)))



(define (type->string obj)
  (cond 
    ((symbol? obj) (symbol->string obj))
    ((eqv? (car obj) 'type-var) (string-append "T" (number->string  (cdr obj))))
    ((eqv? (car obj) 'function) 
     (let ((arg 
             (if (and (pair? (cadr obj)) (not (type-var? (cadr obj))))
               (string-append "(" (type->string (cadr obj)) ")")
               (type->string (cadr obj))))
           (body (type->string (cddr obj)))) 
       (string-append arg  " -> "  body )))))
     


;-----------------------------------------------------
;
;             REPL
;
;-----------------------------------------------------

(define (eqshow eqs)
  (let loop ((l eqs))
    (cond 
      ((null? l) '())
      ((null? (car l)) (loop (cdr l)))
      (else (display ":::::  ")(display (caar l))(display " = ")(display (cdar l))(newline)(loop (cdr l))))))


(let type-check-loop ()
  (let* ((input (test-convert (read)))
         (analyzed-input (extract builtin-functions input))
         (kai (unify '() (car analyzed-input)))
         (ret (expand-rec (cdr analyzed-input) kai)))
    (display (type->string ret))(newline)
    (type-check-loop)))