はじめに

型推論の仕組みがPrologとほぼ同様であることから理解のための試作をしました。理解が深まってきましたので本格的にISLisp用の型推論器の制作にとりかかりました。型推論はなかなか難しく、考えるべきことも多いことから制作は長丁場になることが予想されます。考えたことの覚書として投稿することにしました。

データ構造

推論した型データは大域変数type-functionに次のように連想リストとして蓄えられます。

((関数名 出力の型　(引数1の型　引数２の型　・・・引数ｎの型)) ...)

バックトラック

ISLispの組込み関数には異なる型の引数を受け取ることができるものがあります。例えばlengthはリスト、ベクタ、文字列をとることができます。

> (length '(1 2 3))
3
> (length #(1 2 3))
3
> (length "123")
3

ところで、このlengthを使った次の関数について考えてみます。意味のある関数ではありません。

(defun test1 (x)
  (length x)
  (string-append x "123"))

推論器はlengthでxが引数として使われていることから、xはリスト、ベクタ、文字列の可能性があることがわかります。リストであると仮定して推論を進めるとstring-appendにおいてxは文字列であることから、推論をやり直さないといけません。ここでバックトラックをしています。

unify

バックトラックを可能にするには、それまでに突き止めた型環境を以前の状態に復元させて、改めて推論を再開しないといけません。このためunifyが生成する型環境は非破壊的です。当初xがobjectクラスをもつという環境があり、その後、xはリストのクラスを持つことが判明した場合には、objectの情報はそのまま残して、listクラスにunifyしたことを型環境に追加します。listであったことが間違いでありバックトラックする場合に備えています。通常のPrologではすでに環境にあるのであればそれと一致しなければunifyは失敗します。しかし型推論の場合にはそのクラスが記憶されているもののサブクラスである場合にはunifyは成功します。

エラー処理

例えば次のケースでは型クラスの不整合が起きています。

(defun test4 (x)
  (sin (string= x "1")))

上記の例は単純でありエラーであることが確定できます。しかし複雑なものになると直ちには判別できず、バックトラックによりすべてを調べ上げたうえでないとエラーを確定できない場合があります。そこで、型推論器はこのような場合にもエラーを起動せず、不整合だったことを大域変数のerror-messageに記憶するにとどめます。unifyは失敗です。完全失敗に至った状態でこのエラーメッセージを表示し、どこに問題があったのかを知らせる方法をとっています。

基本機能　覚書

推論の中枢部分はinference inference-all が担当しています。これはピーター・ノーヴィッグ先生の「実用Common Lisp」のPrologインタプリタの構造と同じです。defunにより定義されるLisp関数は暗黙のprognにより複数のS式を持ちます。inference-allはこの複数のS式を受け取り推論をスタートします。1個のS式の推論をinferenceに託し、残りを再帰的にinference-allで消化していきます。途中prognやletにより新たに暗黙のprognによるS式が発生する場合にはinference-allを再帰的に起動しています。全部のS式の推論が終わり空リストになった時点で推論は終了です。

if構文は、現状では単純に成功した場合のクラスをそのクラスとみなしています。正確には成功と失敗の両方をみてクラスを決定する必要があります。cond節も同様です。

subrの引数の型クラス、戻り値の型クラスはマクロassertにより属性リストとして保持しています。lengthのように複数の場合があるときはassertは複数行になります。retructマクロはそのデータを全部削除します。読み込み時に全部をretructしています。

symbol-classは与えられたシンボル引数のclassを返すもので、独自拡張です。functionに対してのsymbol-functionのようなものです。

例　竹内関数

test1.lsp
(defun tarai (x y z)
  (if (<= x y)
      y
      (tarai (tarai (- x 1) y z)
             (tarai (- y 1) z x)
             (tarai (- z 1) x y))))

> (inference-file "test1.lsp")
inferencing TARAI
T
> type-function
((TARAI <class integer> (<class integer> <class integer> <class integer>)))
>

例　型情報を付加した竹内関数

(defun tarai (x y z)
  (the <fixnum> x)(the <fixnum> y)(the <fixnum> z)
  (if (<= x y)
      y
      (tarai (tarai (- x 1) y z)
             (tarai (- y 1) z x)
             (tarai (- z 1) x y))))


> (inference-file "test1.lsp")
inferencing TARAI
T
> type-function
((TARAI <class fixnum> (<class fixnum> <class fixnum> <class fixnum>)))
>

例　型情報を付加したフィボナッチ数

(defun fib (n)
  (the <fixnum> n)
  (if (< n 2)
      1
      (fib (- n 1))))

> (inference-file "test1.lsp")
inferencing FIB
T
> type-function
((FIB <class fixnum> (<class fixnum>)))
>

例　浮動小数点数のフィボナッチ数

(defun fib (n)
  (the <float> n)
  (if (< n 2.0)
      1.0
      (fib (- n 1.0))))


> (inference-file "test1.lsp")
inferencing FIB
T
> type-function
((FIB <class float> (<class float>)))
>

推定

加減乗演算については、ある程度推定せざるを得ません。(+ x 0.2) であればxはfloatであろうと推定しています。しかし実際にはintegerである可能性も否定できません。
〇すべての引数の型がまだ定まっていない、あるいはobjectクラスの場合はnumberクラスであると推定します。
〇すべての引数がfixnumクラスであればfixnumです。
〇ひとつでもfloatクラスがあればすべての引数はfloatであると推定し、戻り値もfloatであると推論します。
〇ひとつでもintegerクラスがあればすべての引数をintegerクラスと推定し、戻り値もintegerであると推論します。

拡張

ISLisp規格ではintegerのサブクラスはないのですが、以下のものを拡張しました。そのスーパークラスは整数のintegerクラスです。

<fixnum>  小整数クラス　-999999999 ~ 999999999

<longnum> ロング整数クラス

<bignum>　BIGNUMクラス

コード

現状のコードです。まだ、不完全です。ファイルに関数定義を書いておいて、(inference-file "foo.lsp")のようにして起動します。現状、まだまだすべての構文に対応していません。完全動作することを確認した後にISLispのFASTコンパイラに組み込み、その情報をもとにより効率のよいコードを生成したいと考えています。

;;-----------type inferrence-------------
(defun optimize-p (x)
  (let* ((fn (elt x 1))
         (dt (assoc fn type-function)))
    (cond ((null dt) nil)
          ((and (eq (elt x 0) 'defun)
                (member (elt dt 1) (list (class <fixnum>)(class <float>)))
                (subsetp (elt dt 2) (list (class <fixnum>)(class <float>))))
           t)
          (t nil))))

(defun return-type (x)
  (elt (assoc x type-function) 1))

(defun argument-type (x)
  (elt (assoc x type-function) 2))

;; (x y z) -> (int x, double y, int z) when (<fixnum> <float> <fixnum>)
;; output to stream of string
(defun type-gen-arg2 (stream ls type)
  (format stream "(")
  (if (null ls)
      (format stream ")")
      (for ((ls1 ls (cdr ls1))
            (n 0 (+ n 1)))
           ((null (cdr ls1))
            (cond ((eq (elt type n) (class <fixnum>))
                   (format stream "int ")
                   (format-object stream (conv-name (car ls1)) nil)
                   (format stream ")"))
                  ((eq (elt type n) (class <float>))
                   (format stream "double ")
                   (format-object stream (conv-name (car ls1)) nil)
                   (format stream ")"))))
           (cond ((eq (elt type n) (class <fixnum>))
                  (format stream "int ")
                  (format-object stream (conv-name (car ls1)) nil)
                  (format stream ","))
                 ((eq (elt type n) (class <float>))
                  (format stream "double ")
                  (format-object stream (conv-name (car ls1)) nil)
                  (format stream ","))))))

;;for tail call
;; when ls=(<fixnum> <float> <fixnum>) -> int temp1; double temp2; int temp3;
(defun type-gen-arg3 (n ls)
  (unless (= n 0)
    (for ((m 1 (+ m 1)))
         ((> m n) 
          (format code2 "~%"))
         (cond ((eq (car ls) (class <fixnum>))
                (format code2 "int "))
               ((eq (car ls) (class <float>))
                (format code2 "double ")))
         (format code2 "temp")
         (format code2 (convert m <string>))
         (format code2 ";"))))



;;(foo arg1 arg2) -> 
;;  return(F_makeint(foo(Fgetint(arg1),Fgetint(arg2))));
(defun type-gen-call (name n)
  (let ((name1 (conv-name name))
        (return (return-type name))
        (argument (argument-type name)))
    (cond ((= n 0)
           (cond ((eq return (class <fixnum>))
                  (format code1 "return(Fmakeint(")
                  (format code1 (convert name1 <string>))
                  (format code1 "() ));~%"))
                 ((eq return (class <float>))
                  (format code1 "return(Fmakedoubleflt(")
                  (format code1 (convert name1 <string>))
                  (format code1 "() ));~%"))))
        (t 
          (cond ((eq return (class <fixnum>))
                 (format code1 "return(Fmakeint(")
                 (format code1 (convert name1 <string>))
                 (format code1 "("))
                ((eq return (class <float>))
                 (format code1 "return(Fmakedoubleflt(")
                 (format code1 (convert name1 <string>))
                 (format code1 "(")))
          (for ((m 1 (+ m 1)))
               ((= m n)
                (cond ((eq (elt argument (- m 1)) (class <fixnum>))
                       (format code1 "Fgetint(arg")
                       (format code1 (convert m <string>))
                       (format code1 "))));~%"))
                      ((eq (elt argument (- m 1)) (class <float>))
                       (format code1 "Fgetflt(arg")
                       (format code1 (convert m <string>))
                       (format code1 "))));~%"))))
               (cond ((eq (elt argument (- m 1)) (class <fixnum>))  
                      (format code1 "Fgetint(arg")
                      (format code1 (convert m <string>))
                      (format code1 "),"))
                     ((eq (elt argument (- m 1)) (class <float>))
                      (format code1 "Fgetflt(arg")
                      (format code1 (convert m <string>))
                      (format code1 "),"))))))))


(defun subsetp (x y)
  (cond ((null x) t)
        ((member (car x) y)
         (subsetp (cdr x) y))
        (t nil)))


(defmacro assert (sym :rest class)
  `(let ((old (property ',sym 'inference)))
     (if (null old)
         (set-property (list (mapcar #'eval ',class))
                       ',sym 'inference)
         (set-property (append old (list (mapcar #'eval ',class)))
                       ',sym 'inference ))))

(defmacro retruct (sym)
  `(remove-property ',sym 'inference))

(defglobal file-name-and-ext nil)
(defglobal instream nil)
(defglobal type-function nil)
(defglobal loca-type-function nil) ;;for lavels flet syntax
(defglobal error-message nil)


(defun warning (str x)
  (setq error-message (list str x)))

(defun inference-defun (x)
  (let* ((name (elt x 1))
         (arg (elt x 2))
         (body (cdr (cdr (cdr x))))
         (init-type-input (create-list (length arg) (class <object>)))
         (init-env (create-init-env arg)))
    (format (standard-output) "inferencing ~A~%" name)
    (setq type-function (cons (list name
                                    (class <object>)
                                    init-type-input)
                              type-function))
    (let ((type-env (inference-all body init-env name)))
      (cond ((eq type-env 'no)
             (format (standard-output) "~A~%" error-message))
            (t (set-type-function-input name (find-argument-class arg type-env)))))))


;;transform from data in ls to class data. 
(defun find-argument-class (ls type-env)
  (for ((arg ls (cdr arg))
        (result nil))
       ((null arg) (reverse result))
       (setq result (cons (find-class (car arg) type-env)
                          result))))

;;create list that length is length of ls. all element is <object>
(defun create-init-env (ls)
  (for ((arg ls (cdr arg))
        (result nil))
       ((null arg) (reverse result))
       (setq result (cons (cons (car arg) (class <object>))
                          result))))

;; inference a s-expression
;; if x is true return type-env else return 'no
(defun inference (x type-env)
  (cond ((and (symbolp x)(eq x t)) type-env)
        ((and (symbolp x)(eq x nil)) type-env)
        ((symbolp x)
         (let ((y (refer x type-env)))
           (if y
               type-env
               (unify x (class <object>) type-env))))
        ((atom x) type-env)
        ((and (consp x)(eq (car x) 'the))
         (unify (class* (elt x 1)) (elt x 2) type-env))
        ((and (consp x)(eq (car x) 'not)) ;; ignore not function
         type-env)
        ((and (consp x)(eq (car x) 'setq))
         (unify (elt x 1) (elt x 2) type-env))
        ((and (consp x)(eq (car x) 'catch))
         (inference (elt x 2) type-env))
        ((and (consp x)(eq (car x) 'throw))
         (inference (elt x 2) type-env))
        ((and (consp x)(eq (car x) 'quote)) type-env)
        ((and (consp x)(eq (car x) 'cond))
         (inference-cond x type-env))
        ((and (consp x)(eq (car x) 'if))
         (inference-if x type-env))
        ((and (consp x)(eq (car x) 'let))
         (inference-let x type-env))
        ((and (consp x)(eq (car x) 'let*))
         (inference-let x type-env))
        ((and (consp x)(eq (car x) 'while))
         (inference-while x type-env))
        ((and (consp x)(member (car x) '(+ - * = > < >= <= /=)))
         (inference-numeric x type-env))
        ((and (consp x)(subrp (car x)))
         (let ((type-subr (property (car x) 'inference)))
           (block exit-inference
             (for ((type type-subr (cdr type)))
                  ((null type) (warning "subr type mismatch" x) 'no)
                  (let ((new-env (inference-arg (cdr x) (cdr (car type)) type-env)))
                    (if (not (eq new-env 'no))
                        (return-from exit-inference new-env)))))))
        ((consp x)
         (let ((type (find-function-type (car x))))
           (if type
               (inference-arg (cdr x) 
                              (elt type 1)
                              type-env))))
        (t (warning "inference type mismatch" x)'no)))


;; inference s-expressions
;; if all success return type-env else return 'no
(defun inference-all (x type-env fn)
  (let ((result (inference-all1 x type-env fn)))
    (if (not (eq result 'no))
        (set-type-function-output fn (find-class (last x) result)))
    result))

(defun inference-all1 (x type-env fn)
  (cond ((null x) type-env)
        ((and (consp (car x))(member (car (car x)) '(+ - * = > < >= <= /=)))
         (let ((new-env (inference (car x) type-env)))
           (cond (new-env
                   (inference-all1 (cdr x) new-env fn))
                 (t (warning "numeric type mismatch" x) 'no))))
        ((and (consp (car x))(subrp (car (car x))))
         (let ((type-subr (property (car (car x)) 'inference)))
           (block exit-all
             (for ((type type-subr (cdr type)))
                  ((null type) (warning "subr type mismatch" x) 'no)
                  (let ((new-env (inference-arg (cdr (car x)) (cdr (car type)) type-env)))
                    (if (not (eq new-env 'no))
                        (let ((result (inference-all1 (cdr x) new-env fn)))
                          (if (not (eq result 'no))(return-from exit-all result)))))))))
        (t 
         (let ((new-env (inference (car x) type-env)))
           (cond ((eq new-env 'no)
                  (warning "type mismatch" x) 'no)
                 (t (inference-all1 (cdr x) new-env fn)))))))

;;cond syntax
(defun inference-cond (x type-env)
  (inference-cond1 (cdr x) type-env))

(defun inference-cond1 (x type-env)
  (cond ((null x) type-env)
        (t (let ((new-env (inference-cond2 (car x) type-env)))
             (if (not (eq new-env 'no))
                 (inference-cond1 (cdr x) new-env)
                 (warning "cond mismatch" x)))))) 

(defun inference-cond2 (x type-env)
  (if (null x)
      type-env
      (inference-cond2 (cdr x) (inference (car x) type-env))))

;;if syntax
(defun inference-if (x type-env)
  (if (= (length x) 4)
      (inference-if1 x type-env)
      (inference-if2 x type-env)))

;;(if test true else)
(defun inference-if1 (x type-env)
  (let ((test (inference (elt x 1) type-env)))
    (if (not (eq test 'no))
        (let ((else (inference (elt x 3) test)))
          (if (not (eq else 'no))
              (let ((true (inference (elt x 2) else)))
                (if (not (eq true 'no))
                    true
                    (progn (warning "if mismatch" x) 'no))))))))

;;(if test true)
(defun inference-if2 (x type-env)
  (let ((test (inference (elt x 1) type-env)))
    (if (not (eq test 'no))
        (let ((true (inference (elt x 2) test)))
          (if (not (eq true 'no))
              true
              (progn (warning "if mismatch" x) 'no))))))
;; +-* ...
(defun inference-numeric (x type-env)
  (cond ((every (lambda (x) 
                  (let ((type (find-class x type-env)))
                    (or (null type)
                        (eq type (class <object>)))))
                (cdr x))
                (estimate (cdr x) (class <number>) type-env))
        ((every (lambda (x) (eq (class <fixnum>)
                                (find-class x type-env)))
                (cdr x))
         type-env)
        ((any (lambda (x) (eq (class <float>)
                              (find-class x type-env)))
              (cdr x))
         (estimate (cdr x) (class <float>) type-env))
        ((any (lambda (x) (eq (class <integer>)
                              (find-class x type-env)))
              (cdr x))
         (estimate (cdr x) (class <integer>) type-env))
        ((any (lambda (x) (eq (class <fixnum>)
                              (find-class x type-env)))
              (cdr x))
         (estimate (cdr x) (class <integer>) type-env))
        (t (warning "numerical argument type mismatch" x)
           'no)))

;;let syntax
(defun inference-let (x type-env)
  (let ((vars (elt x 1))
        (body (cdr (cdr x))))
    (block exit-let
      (for ((vars1 vars (cdr vars1)))
           ((null vars1))
           (setq type-env (unify (elt (car vars1) 0)
                                 (elt (car vars1) 1) type-env))
           (if (eq type-env 'no)
               (return-from exit-let 'no)))
      (inference-all1 body type-env nil))))

(defun inference-while (x type-env)
  (inference-while1 (cdr x) type-env))

(defun inference-while1 (x type-env)
  (cond ((null x) type-env)
        (t (inference-while1 (cdr x) (inference (car x) type-env)))))


;;find type-data of user defined function.
;;return list as (output-class (input-class ...) type-env)
(defun find-function-type (x)
  (let ((y (assoc x type-function)))
    (if (null y)
        nil
        (cdr y))))

;;if argument is atom unify the atom and type of argument.
;;else if argument is cons, inference the cons. 
;;and unify the cons and type of argument. 

(defun inference-arg (x y type-env)
  (block exit-arg
    (for ((arg x (cdr arg))
          (type y (cdr type)))
         ((null arg) type-env)
         (cond ((atom (car arg)) 
                (let ((new-env (unify (car arg)(car type) type-env)))
                  (if (eq new-env 'no)
                      (return-from exit-arg 'no)
                      (setq type-env new-env))))
               (t (let ((new-env (inference (car arg) type-env)))
                    (cond ((eq new-env 'no)
                           (return-from exit-arg 'no))
                          (t (let ((output-class (find-class (car arg) type-env)))
                               (if (not (or (eq output-class (car type))
                                            (subclassp output-class (car type))))
                                   (return-from exit-arg 'no)))))
                    (setq type-env new-env)))))))



;;type inference s-expression(s) in file x.
;;x is string of filename.
(defun inference-file (x)
  (setq file-name-and-ext x)
  (setq type-function nil)
  (setq instream (open-input-file x))
  (let ((sexp nil))
    (while (setq sexp (read instream nil nil))
           (if (and (consp sexp)(eq (car sexp) 'defun))
               (inference-defun sexp)))
    (close instream)
    (setq instream nil))
  t)

;;if x is registed in type-function data,
;;return t (if the output-class is <object>) 
;;return nil (if the output-class is not <object>)
(defun function-type-object-p (x)
  (let ((y (assoc (elt x 1) type-function)))
    (if (not y)
        nil
        (eq (elt y 0)(class <object>)))))

;;find class of s-exp
(defun find-class (x type-env)
  (cond ((null x) (class <null>))
        ((and (symbolp x) (eq x 't)) (class <symbol>))
        ((symbolp x) (refer x type-env))
        ((atom x) (class-of x))
        ((and (consp x) (member (car x) '(+ - * = > < >= <= /=)))
         (find-class-numeric x type-env))
        ((and (consp x) (subrp (car x)))
         (let ((type-subr (property (car x) 'inference)))
           (car (car type-subr))))
        ((and (consp x) (type-function-p (car x)))
         (elt (find-function-type (car x)) 0))
        ((and (consp x) (eq (car x) 'cond))
         (find-class (last (elt x 1)) type-env))
        ((and (consp x) (eq (car x) 'if))
         (find-class (elt x 2) type-env))                          
        ((and (consp x) (eq (car x) 'quote))
         (class-of (elt x 1)))
        ((and (consp x) (eq (car x) 'the)) nil)
        ((and (consp x) (eq (car x) 'setq))
         (find-class (elt x 1) type-env))
        ((and (consp x) (eq (car x) 'catch))
         (find-class (elt x 1) type-env))
        ((and (consp x) (eq (car x) 'throw))
         (find-class (elt x 2) type-env))
        ((and (consp x) (eq (car x) 'let))
         (find-class (last (cdr (cdr x))) type-env))
        ((and (consp x) (eq (car x) 'let*))
         (find-class (last (cdr (cdr x))) type-env))
        ((and (consp x) (eq (car x) 'while))
         (class <null>))
        ((and (consp x) (eq (car x) 'lambda))
         (class <function>))
        ((consp x)
         (class <object>))))

(defun find-class-numeric (x type-env)
  (cond ((every (lambda (x) 
                  (let ((type (find-class x type-env)))
                    (or (null type)
                        (eq type (class <object>)))))
                (cdr x))
                (class <number>))
        ((every (lambda (x) (eq (class <fixnum>)
                                (find-class x type-env)))
                (cdr x))
         (class <fixnum>))
        ((any (lambda (x) (eq (class <float>)
                              (find-class x type-env)))
              (cdr x))
         (class <float>))
        ((any (lambda (x) (eq (class <integer>)
                              (find-class x type-env)))
              (cdr x))
         (class <integer>))
        ((any (lambda (x) (eq (class <fixnum>)
                              (find-class x type-env)))
              (cdr x))
         (class <integer>))
        (t (class <number>))))


;;reference symbol x in type-env       
(defun refer (x type-env)
  (let ((y (assoc x type-env)))
    (cond ((null y) (class <object>))
          (t (cdr y)))))

;;assign type destructive in type-function
;;set output class
(defun set-type-function-output (fn y)
  (let ((z (assoc fn type-function)))
    (setf (elt z 1) y)))
;;set input class
(defun set-type-function-input (fn y)
  (let ((z (assoc fn type-function)))
    (setf (elt z 2) y)))


;;if x is registed in type-function return not nil
;;elt return nil
(defun type-function-p (x)
  (assoc x type-function))

;;if eq(x,y) subclassp(x,y) or subclassp(y,x),then unify is success
;;if success return type-env else return 'no.
(defun unify (x y type-env) 
  (cond ((and (not (variablep x)) (not (variablep y)))
         (let ((x1 (if (not (classp x))
                       (find-class x type-env)
                       x))
               (y1 (if (not (classp y))
                       (find-class y type-env)
                       y)))
           (if (or (eq x1 y1)
                   (subclassp* x1 y1)
                   (subclassp* y1 x1))
               type-env
               'no)))
        ((and (variablep x) (not (variablep y)))
         (let ((x1 (refer x type-env))
               (y1 (if (not (classp y))
                       (find-class y type-env)
                       y)))
           (cond ((null x1) 
                  (setq type-env 
                        (cons (cons x y1) type-env))
                  type-env)
                 ((eq x1 y1) type-env)
                 ((subclassp* x1 y1) type-env)
                 ((subclassp* y1 x1)
                  (cons (cons x y1) type-env)) 
                 (t 'no))))
        ((and (not (variablep x)) (variablep y))
         (let ((x1 (if (not (classp x))
                       (find-class x type-env)
                       x))
               (y1 (refer y type-env)))
           (cond ((null y1) 
                  (setq type-env
                        (cons (cons y x1) type-env))
                  type-env)
                 ((eq x1 y1) type-env)
                 ((subclassp* x1 y1)
                  (cons (cons y x1) type-env))
                 ((subclassp* y1 x1) type-env)
                 (t 'no))))
        (t (setq type-env
                 (cons (cons x y) type-env))
           type-env)))

;;symbol is variable in unify.
;;but nil and t are not variable.
(defun variablep (x)
  (and (symbolp x) (not (null x)) (not (eq x t))))

(defun subclassp* (x y)
  (cond ((or (eq x nil)(eq x t)(eq y nil)(eq y t)) nil)
        (t (subclassp x y))))

;;unify all data in ls with class.
(defun estimate (ls class type-env)
  (for ((ls1 ls (cdr ls1)))
       ((null ls1) type-env)
       (cond ((not (symbolp (car ls1))) t)
             (t (setq type-env (unify (car ls1) class type-env))))))

(defun class* (x)
  (symbol-class x))

;;subr type data
(retruct parse-number)
(retruct sin)
(retruct cos)
(retruct tan)
(retruct atan)
(retruct atan2)
(retruct sinh)
(retruct cosh)
(retruct tanh)
(retruct floor)
(retruct ceiling) 
(retruct truncate)
(retruct round)
(retruct mod)
(retruct div)
(retruct gcd)
(retruct lcm)
(retruct isqrt)
(retruct char=)
(retruct char/=)
(retruct char<)
(retruct char>)
(retruct char<=)
(retruct char>=)
(retruct quotient)
(retruct reciprocal)
(retruct max)
(retruct min)
(retruct abs)
(retruct exp)
(retruct log) 
(retruct expt)
(retruct sqrt)
(retruct cons)
(retruct car) 
(retruct cdr) 
(retruct create-list)
(retruct list)
(retruct reverse) 
(retruct nreverse)
(retruct assoc)
(retruct member)
(retruct mapcar)
(retruct mapc)
(retruct mapcan)
(retruct maplist) 
(retruct mapcl)
(retruct mapcon)
(retruct create-array)
(retruct array-dimension)
(retruct create-vector)
(retruct vector)
(retruct create-string)
(retruct string=) 
(retruct string/=)
(retruct string<) 
(retruct string>) 
(retruct string>=)
(retruct string<=)
(retruct funcall) 
(retruct char-index)
(retruct string-index)
(retruct length)
(retruct elt)
(retruct null)
(retruct eq)
(retruct cons)
(retruct format)
(retruct format-integer)
(retruct format-float)
(retruct standard-input)
(retruct standard-output)
(retruct system)
(retruct open-input-file)
(retruct open-output-file)
(retruct eval)
(retruct atom)
(retruct consp)
(retruct symbolp)
(retruct listp)
(retruct consp)
(retruct numberp)
(retruct integerp)
(retruct floatp)
(retruct fixnump)
(retruct bignump)
(retruct longnump)
(retruct stringp)
(retruct characterp)
(retruct general-vector-p)
(retruct general-array*-p)
(retruct property)
(retruct set-property)
(retruct read)
(retruct eval)
(retruct append)
(retruct list-to-c1)

;;       fn          output           input
(assert parse-number (class <number>) (class <string>))
(assert sin (class <float>) (class <number>))
(assert cos (class <float>) (class <number>))
(assert tan (class <float>) (class <number>))
(assert atan (class <float>) (class <number>))
(assert atan2 (class <float>) (class <number>) (class <number>))
(assert sinh (class <float>) (class <number>))
(assert cosh (class <float>) (class <number>))
(assert tanh (class <float>) (class <number>))
(assert floor (class <integer>) (class <number>))
(assert ceiling (class <integer>) (class <number>))
(assert truncate (class <integer>) (class <number>))
(assert round (class <integer>) (class <number>))
(assert mod (class <integer>) (class <integer>) (class <integer>))
(assert div (class <integer>) (class <number>) (class <number>))
(assert gcd (class <integer>) (class <integer>) (class <integer>))
(assert lcm (class <integer>) (class <integer>) (class <integer>))
(assert isqrt (class <number>) (class <integer>))
(assert char= (class <object>) (class <character>) (class <character>))
(assert char/= (class <object>) (class <character>) (class <character>))
(assert char< (class <object>) (class <character>) (class <character>))
(assert char> (class <object>) (class <character>) (class <character>))
(assert char<= (class <object>) (class <character>) (class <character>))
(assert char>= (class <object>) (class <character>) (class <character>))
(assert quotient (class <number>) (class <number>) (class <number>))
(assert reciprocal (class <number>) (class <number>))
(assert max (class <number>) '+ (class <number>))
(assert min (class <number>) '+ (class <number>))
(assert abs (class <number>) (class <number>))
(assert exp (class <number>) (class <number>))
(assert log (class <number>) (class <number>))
(assert expt (class <number>) (class <number>))
(assert sqrt (class <number>) (class <number>))
(assert cons (class <list>) (class <object>) (class <object>))
(assert car (class <object>) (class <list>))
(assert cdr (class <object>) (class <list>))
(assert create-list (class <list>) (class <integer>) '- )
(assert list (class <list>) 
  (class <object>)(class <object>)(class <object>)(class <object>))
(assert reverse (class <list>) (class <list>))
(assert nreverse (class <list>) (class <list>))
(assert assoc (class <list>) (class <object>) (class <list>))
(assert member (class <object>) (class <object>) (class <list>))
(assert mapcar (class <list>) (class <function>)
   (class <list>)(class <list>)(class <list>)(class <list>)(class <list>))
(assert mapc (class <list>) (class <function>) '+ (class <list>))
(assert mapcan (class <list>) (class <function>) '+ (class <list>))
(assert maplist (class <list>) (class <function>) '+ (class <list>))
(assert mapcl (class <list>) (class <function>) '+ (class <list>))
(assert mapcon (class <list>) (class <function>) '+ (class <list>))
(assert create-array (class <basic-array>) (class <list>) '+  (class <object>))
(assert array-dimensions (class <list>) (class <basic-array>))
(assert create-vector (class <integer>) '+ (class <object>))
(assert vector (class <general-vector>) '+ (class <object>))
(assert create-string (class <string>) (class <integer>) '+ (class <object>))
(assert string= (class <object>) (class <string>) (class <string>))
(assert string/= (class <object>) (class <string>) (class <string>))
(assert string< (class <object>) (class <string>) (class <string>))
(assert string> (class <object>) (class <string>) (class <string>))
(assert string>= (class <object>) (class <string>) (class <string>))
(assert string<= (class <object>) (class <string>) (class <string>))
(assert funcall (class <object>) (class <function>) (class <object>))
(assert char-index (class <object>) (class <character>) '-  (class <integer>))
(assert string-index (class <object>) (class <string>) (class <string>) '- (class <integer>))
(assert length (class <integer>) (class <list>))
(assert length (class <integer>) (class <general-vector>))
(assert length (class <integer>) (class <string>))
(assert elt (class <object>) (class <list>) (class <integer>))
(assert elt (class <object>) (class <general-vector>) (class <integer>))
(assert elt (class <object>) (class <string>) (class <integer>))
(assert null (class <symbol>) (class <object>))
(assert eq (class <symbol>) (class <object>) (class <object>))
(assert cons (class <object>) (class <object>))
(assert format (class <null>) 
  (class <stream>) (class <string>) (class <object>) (class <object>))
(assert format-integer (class <null>)
  (class <stream>) (class <integer>) (class <integer>))
(assert format-float (class <null>)
  (class <stream>) (class <float>))
(assert standard-input (class <stream>))
(assert standard-output (class <stream>))
(assert system (class <string>))
(assert open-input-file (class <string>))
(assert open-output-file (class <string>))
(assert eval (class <object>) (class <object>))
(assert atom (class <object>) (class <object>))
(assert consp (class <object>) (class <object>))
(assert symbolp (class <object>) (class <object>))
(assert listp (class <object>) (class <object>))
(assert consp (class <object>) (class <object>))
(assert numberp (class <object>) (class <object>))
(assert integerp (class <object>) (class <object>))
(assert floatp (class <object>) (class <object>))
(assert fixnump (class <object>) (class <object>))
(assert longnump (class <object>) (class <object>))
(assert bignump (class <object>) (class <object>))
(assert stringp (class <object>) (class <object>))
(assert characterp (class <object>) (class <object>))
(assert general-vector-p (class <object>) (class <object>))
(assert general-array*-p (class <object>) (class <object>))
(assert property (class <object>) (class <symbol>) (class <symbol>))
(assert set-property (class <object>)
  (class <object>) (class <symbol>) (class <symbol>))
(assert read (class <object>)
  (class <object>)(class <object>))
(assert eval (class <object>) (class <object>))
(assert append (class <list>) (class <object>) (class <object>))
(assert list-to-c1 (class <stream>)(class <object>))

参考資料

YouTubeにて公開されていた下記の講演がとてもわかりやすかったです。PHPに型推論を実装するというテーマです。
https://www.youtube.com/watch?v=rWX3Y0HaJPE

千葉滋先生の本もとても平易に説明されていてわかりやすいです。
「2週間でできる！スクリプト言語の作り方」
http://gihyo.jp/book/2012/978-4-7741-4974-5