Lispにおける型推論

はじめに

自作のISLisp処理系について型推論の機能を追加しました。この間、試行錯誤したこと、考えたことを書き記しました。

動機

下記のコードは有名な竹内関数、たらいまわし関数です。現在のコンピューターは高速になり(tarai 12 6 0)程度はたいていの処理系で1秒以内に計算を終えます。しかし、さらに高速にしたい、SBCL（よく利用されるLispの処理系）の速度を超えたいと私は考えました。そのためには効率のよいコードを生成する必要があります。自作の処理系Easy-ISLisp（以下「EISL」）はCへ変換するタイプのコンパイラをもっています。Lispは動的型付け言語であり、あらゆる型をもつデータを処理しなければなりません。このためコンパイラが生成するコードも冗長にならざるを得ません。しかし、データの型がわかっていればもっと効率のよいコードへ変換することができるはずです。かといって静的型付け言語のように多くの型に関する記述を追加してしまうとLispらしくありません。そうした型情報なしに、あるいは最小限の型情報からより効率のよいコードへと変換できないだろうか？　これが発端となりLispにおける型推論について取り組みました。

(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))))

アルゴリズム

Prolog処理系がホーン節を証明する方法とほぼ同じ方法に拠っています。Hindley Milnerの型推論アルゴリズムが有名です。自分の方法がこれと同じなのかどうかはその詳細を読んだことがないためなんともわかりません。しかし、やさしく解説した文書を読むと基本的には同じことをやっているように思います。

Prologでは述語の列を最初から読み取って順次証明をしていきます。その過程で変数が持つべき値をunifyにより蓄積していきます。途中まで証明が成功していたとしても最後の述語で証明に失敗した場合にはそれまでunifyしたものを破棄して他の可能性がないかをバックトラックにより探します。これと同じことをやっています。

具体例で示します。次のあまり意味のない関数定義について考えてみます。

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

ISLispではlengthはベクタ、文字列、リストに対して用いることができます。

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

型推論器は関数定義の本体部を上から順に見に行きます。最初は(length x) です。型推論器は組込関数の引数の型を知っています。最初、lengthの引数をリストと仮定します。xはリストであると推定します。unifyという仕組みで行っています。型推論器は次の(string-append x "123")を見に行きます。先ほどxはリストであろうと仮定しました。ところが、string-appendは文字列を連結して返す組込関数ですからxは文字列でないといけません。lengthのところでリストであると仮定したのが間違いでした。そこでlengthに戻ってやり直します。unifyはxがリストであろうと仮定したことをご破算にします。今度はlengthはベクタではないかと仮定します。次のstring-appendはxが文字列であることを要請していますから、これもうまくありません。再度、lengthに戻ります。ようやく文字列の場合ではないかと仮定します。そしてstring-appendにいきますとxが文字列であることと矛盾しません。xは文字列であることが推論できました。

ISLispのクラス

ISLispは最初からILOSと呼ばれるオブジェクト指向を含んでいます。各データはそれぞれクラスを有します。これは階層構造になっておりobjectクラスを頂点にして様々なクラスに分類されます。数はnumberクラスの下にinteger、floatクラスがあります。また、EISLの独自拡張としてbignum、fixnum、longnumクラスを有します。これらもnumberクラスのサブセットであり、integerクラスのサブセットになっています。

<number> ---- <integer> ---- <bignum>
            |              |
　　　　　   - <float>      - <longnum>
　　　　　　　　　　　　　　　|
                           - <fixnum>

図　ISLispのクラス階層（ドラフトより引用）

unify

assignが破壊的代入なのに対して、unifyは非破壊的な統合です。unify(X,Y,type-env) とするとXとYとは同じクラスに属するものとして型環境type-envに登録されます。しかし上述のアルゴリズムの説明ではやり直しをしていました。unifyは非破壊的ですのでやり直すことが可能です。Prolog処理系で用いられています。

型推論でのunifyはPrologのunifyとは若干異なります。例えばｘがnumberクラスであろうと仮定して推論を進めていたところ、他の情報によりxがintegerクラスであることがわかったとします。unifyは型情報を書き換えるのではなく追加します。integerクラスはnumberクラスのサブセットであり矛盾していません。より詳しい型情報が得られたことになります。

unifyは型情報を局所変数type-envに保持しつつ推論を進めていきます。このtype-envは連想リストになっています。新しくクラスが見つかるとconsにより左側に追加していきます。

((x . <integer>)(y . <list>)(x . <number>) ...)

型情報の保存

このようにして変数の型を仮定を繰り返していき本体部の最後のS式を終えましたら、解析している関数の引数の型クラスを調べます。これは入力に関する情報です。出力に関する型情報も収集します。本体部の最後のS式が関数の値となるのですから、このクラスを調べればこれがその関数の出力する型クラスとなります。最初の例ですと本体部の最後のS式はstring-appendでした。これは文字列を返す組込関数ですから関数fooはstringクラスを返すことがわかります。

これらの情報は大域変数のtype-functionに保存されます。次の形式で保存されています。

((function-name output-class input-class1 input-class2 ...) ...)

上述の竹内関数の場合は次の結果を得ます。

> type-function
((TARAI <class integer> (<class integer> <class integer> <class integer>)))
> 

局所関数

Lispではlabelsあるいはfletにより局所関数を定義することができます。特に意味のある関数ではありませんが次のようなものです。

(defun foo (x)
  (labels ((boo (y)
                (+ y 1)))
    (boo (* x 2))))

この局所関数booについても型推論をしています。局所関数が複数ある場合にはそれぞれ型環境を別にして推論をしています。結果については大域定義された関数の最後に局所関数の情報を保存しています。

> type-function
((FOO <class integer> (<class integer>) ((BOO <class integer> (<class integer>)))))

推定

数の型については加減乗除計算のところで推定をしています。

(+ a ｂ) とあり、a,bのクラスがまだ不明なときにはa,bはnumberクラスであると推定します。
(+ a 0.2) とあり、aのクラスがまだ不明なときにはaはfloatクラスであると推定します。
(+ 1 2 3) のようにすべての引数がintegerクラスの場合には計算結果はintegerクラスと推論できます。
(+ a 1 2.0) のように引数のうちにひとつでもfloatクラスがあればaはfloatクラスと推定し、結果はfloatクラスと推論します。
(+ a 1) のように引数のうちにintegerクラスがある場合にはaはintegerクラスと推定し、結果はintegerクラスと推論します。

例えば最後の例の(+ a 1) でaはfloatである可能性もあるのですが、多くの場合aはintegerだろうと思います。プログラムの書き手はaがfloatになることを知っていれば(+ a 1.0) と記述するだろうという予想に基づいています。これでおおむねうまくいくようです。

マクロ

Lispと不可分な関係にあるのがマクロです。マクロを見つけた場合には型推論器はmacroexpand-1により展開します。そしてその展開結果を型推論するようにしています。関数の場合には読めばある程度直観的にその返す値のクラスを読み取ることができます。しかし、マクロですとうっかりミスをしてしまう可能性もあるように思います。

型推論の副産物

このように推論を進めていきますと明らかにおかしいというコードを検出することができます。例えば次のコードです。

(defun foo (x)
  (let ((v (create-vector 2)))
    (* x v)))

create-vector は指定個の要素数をもつベクタを生成する組込関数です。ですから変数vはvector クラスです。しかし乗算の*はnumberクラスであることが要請されています。したがってクラスが合致しません。EISLの型推論器は警告メッセージを出しますが、コンパイルは可能なので最後までコンパイルが進みます。実行するとエラーになります。

> (compile-file "foo.lsp")
type inference
FOO numerical argument type mismatch (* X V)
FOO type mismatch (LET ((V (CREATE-VECTOR 2))) (* X V))
initialize
pass1
pass2
compiling FOO 
finalize
invoke GCC
T
> 

また、とても単純なミスでありながら、よくやってしまうことに引数の個数を間違えていて気が付かない場合があります。実行時にしか検出できないとするとそれが滅多に実行されないコードである場合には長らくバグが検出されないという問題があります。型推論の過程でその単純なミスも検出できるようになりました。

問題点

cond節　if構文 での推論

動的型付け言語であるLispでは条件文は多様な型をもつ場合があります。例えば次の例です。

(defun foo (x)
  (cond ((floatp x) (format-float (standard-output) x))
        ((integerp x) (format-integer (standard-output) x 10))
        (t (format (standard-output) "~A" x))))

引数xの型に応じて出力関数を使い分けています。cond節の最初でformat-floatでxが使われていることからxはfloatクラスであると推論してしまうと、次のformat-integerでワーニングになってしまいます。そこでcond節の場合にはunifyはしてもその型情報は記憶しないこととしています。ifも同様です。

大域変数

defglobalにより大域変数を定義することができます。(defglobal a 1)とすればaは１と定義されます。この場合、aは数ですから(sin a)は正しく実行されます。しかしaの値はsetqによりいかようにでも変更されます。推論をしている関数ではない他の関数で(setq a '(1 2))とリストにされていると(sin a)という計算はエラーとなります。しかし、これを型推論で検出するのは困難です。そこで型推論では大域変数については推論をしていません。

funcall

明らかに書き間違いと思われる次のコードについてです。

(defun foo (x)
  (funcall x x x))

これについて型推論をすると警告は出ずコンパイルは可能です。しかし実行時にエラーになります。
funcallの第一引数はfunctionクラスである必要があります。そのためxはfunctionクラスであると推論されます。functionクラスを引数として受け取る関数がないわけではないので型推論器は次の結果をだします。

> type-function
((FOO <class object> (<class function>)))
> 

人間が見れば書き間違えだろうと容易に推測できることも形式的な型推論だけでは検出することは困難と思われます。

再帰の場合のcond節　if構文

cond節やif構文では帰結部のクラスを見て、それらが全部一致しているときにそのクラスを返すべきです。しかし竹内関数のように再帰する場合にはそうもいきません。

(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))))

再帰の部分に(- y 1)があることからyはintegerクラスであることが推論できます。従ってif_then_else のthenの部分はintegerクラスであることが推論できます。しかし、else部分が問題です。else部はtarai関数の出力のクラスでありそれは未定です。これではクラスは判明しません。そこでやむを得ずthen部のクラスをもってif構文の返すクラスとしています。cond節でも最初の帰結部が基底であろうと考えてこれをcond節の返すクラスとしています。厳密さを欠いています。検討を要する部分です。

真偽値

Lispでは伝統的にTを真、NILを偽とすることとなっています。ISLispでも同様です。Tはsymbolクラス、nilはnullクラスとされています。ですから (integer x) の出力の型は一意には定まりません。やむなく出力についてはobjectクラスとしています。
　

ヒントを与える

さて、このようにして曲りなりにも関数の各変数と関数の返す値のクラスを求めることができるようになりました。型推論をしたかった動機はより効率のよいコードを生成することでした。

竹内関数は引数のx,y,zはそれぞれintegerクラス、出力もintegerクラスであると推論しました。しかし、これでは効率化が図れません。Lispの場合、一般的に整数はbignumが使えることが通常です。integerという情報だけからはそれが計算の結果bignumになる可能性も考えなければなりません。

竹内関数は極めて多くの再帰計算をするためコンピューターで実用時間内に計算できるのは引数がfixnumクラスの場合に限られます。(tarai 20 10 0) 程度が精いっぱいです。bignumやlongnumが使われる可能性はありません。しかし、処理系にはそのことはわかりません。そこで最小限の型のヒントを与えることにしました。

(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))))

2行目にtheという構文が挿入されています。ISLispではドラフトp63で定義されています。

(the <integer> 10)

のように使われます。これをコンパイラで活用することにしました。上記の例ではx,y,zの各変数はfixnumクラス、小整数であることを示しています。これによりtarai関数の出力はfixnum、引数もfixnumであることを推論できるようになります。

Lispでは整数はbignumになる場合もあることからセル上にその値を確保するのが通常です。しかし、それですとセルを消費しGC（ガベージコレクション）の負担が増加します。小整数であることがわかっているのであればセルは使わずにC言語のint型変数とすることができます。これであればメモリの節約になりGCも起動する必要がなくなります。コンパイルすると次の実行性能を得ることができました。

> (load "tarai.o")
T
> (time (tarai 12 6 0))
Elapsed Time(second)=0.019989
<undef>
> 

これをスクリプト型のGaucheで実行すると次の結果を得ます。

gosh> (time (tarai 12 6 0))
;(time (tarai 12 6 0))
; real   0.345
; user   0.343
; sys    0.000
12
gosh> 

約17倍の実行性能を有していることがわかります。

コンパイラ型のSBCLで型指定をして計算すると次の結果を得ます。

(declaim (ftype (function (fixnum fixnum fixnum) fixnum) tarai))
(defun tarai(x y z)
  (declare (optimize (speed 3) (debug 0) (safety 0))
    (type fixnum x)(type fixnum y)(type fixnum z))
  (if (<= x y)
      y
      (tarai (tarai (- x 1) y z)
             (tarai (- y 1) z x)
             (tarai (- z 1) x y))))

* (time (tarai 12 6 0))

Evaluation took:
  0.028 seconds of real time
  0.031250 seconds of total run time (0.031250 user, 0.000000 system)
  110.71% CPU
  79,247,451 processor cycles
  0 bytes consed

12

効率化したSBCLよりもEISLの方が1.4倍ほど高速になっていることがわかりました。

最適化

現在のところ型推論により得られた型情報により効率的なコードに変換できるものは限定的です。引数と出力が小整数あるいは浮動小数点数であり、局所関数がある場合にはそれも同様に小整数と浮動小数点数で構成されている場合に限定しています。竹内関数やフィボナッチ数、アッカーマン関数のようなマイクロベンチマークで効率を上げる程度にとどまっています。

今後の課題として、もっと型情報を有効に活用し通常のLispコードでも効率的なコードを生成したいと考えています。

組込関数の型情報

マクロassert, assertz を用いて属性リストとして組込関数の型情報を保持しています。
次の形式です。

(assert name output-class input-class1 input-class2 ...)

assertとassertzの違いはデータを破壊的にセットするか、既にあるデータに追加するかの違いです。assertは以前のデータを破壊してセットします。assertzは以前からあるデータに追加します。例えばeltは文字列、リスト、ベクタを扱うことができます。この場合には次のようにして記述しています。

(assert elt (class <object>) (class <list>) (class <integer>))
(assertz elt (class <object>) (class <general-vector>) (class <integer>))
(assertz elt (class <object>) (class <string>) (class <integer>))

不定個の引数をとる組込関数もあります。例えばlistです。この場合には次のように記述します。

(assert list (class <list>) (class <object>) 'repeat)

終わりに　Lispにおける型推論の意義

LispはもともとAIの研究用に作られました。1958年当時、Fortranなどバッチ処理が普通であった時代に敢えて対話型の処理系として登場しました。これはAIの研究がまだ知見を得られていない未知のものを研究することへの考慮だろうと思います。試行錯誤をしつつプログラムを書き進めていくというスタイルが必要であったからだろうと思います。

Lispはこういう背景があるため、気楽にREPLで対話をしながらコードを書き進めていくことができます。ぼんやりとしたアイディアだけがあり、まだ細部の詳細が決まっていなかったとしても、なんとなく書いているうちに形になってくるのがLispの良さです。

しかし、一方でプログラムの正確性ということでは問題があります。気楽に書き進めた結果、バグが混入していることが多々あります。Lispには対話型のデバッガがあるのでデバッグも気楽ではありますが、完全にとりきれないバグも残ってしまいがちです。スクリプト型の処理系のなかには未だにデバッガさえないものもあるのには閉口してしまいますが。

型推論はこうした正確さを担保するのに有効です。もともと動的型付け言語のLispですから型推論をしても間違いをすべて検出することはできません。依然として実行時エラーの出る可能性は残ります。しかし、自分でやってみた感触としては大部分のエラーを事前に除去できるように感じています。

数十行、数百行程度のLispコードであれば、実行時にエラーを検出、修正することは可能だろうと思います。優秀なデバッガも装備されています。しかし、これが数千行、数万行のLispコードとなると実行時エラーを検出できない場合も出てくるだろうと思います。Lispの動的型付け言語としての気楽さと、大規模プログラミングでの正確性、信頼性の確保に型推論は有効であり、Lispにおいても重要視されるべきだろうと思います。

バージョンアップ

EISL　ver0.90よりコンパイラに型推論が追加されます。これまではcompile-fileで第二引数に'typeを与えた場合にのみ、型推論を実行していました。型推論器のデバッグを進め、コンパイラのセルフコンパイルまで型推論アリでもできるようになりましたので、常時、コンパイル時には型推論をするようにしてあります。

EISL処理系はここで公開されています。
http://eisl.kan-be.com/library/easyislisp.html

ISLispについて

こんなやさしい入門書も出してますので、よかったらどうぞ。
https://www.amazon.co.jp/dp/B074HWYR5N

参考資料

人でもわかる型推論　
https://qiita.com/uint256_t/items/7d8c8feeffc03b388825

「2週間でできる！　スクリプト言語の作り方」　千葉　滋　著　技術評論社