lisp
型推論
ISLisp

ISLispにおける型推論コンパイラ

はじめに

自作のISLisp処理系のEasy-ISLisp(EISL)のコンパイラにつき、型推論器を組み込んでテストをしています。ver0.85より実験的に導入しました。

動作例

現在のところコンパイラ起動の際に第2引数にtypeというシンボルを与えた場合に型推論を行うようにしています。

例1

この例、関数fooではlengthに数が与えられてしまいますから、実行時にエラーになります。これを型推論でチェックしてワーニングメッセージを出しています。コンパイルは可能なのでコードは生成されます。

(defun foo (x)
  (length (+ x 1)))

> (compile-file "tarai.lsp" 'type)
initialize
pass1
inferencing FOO
("subr type mismatch" ((LENGTH (+ X 1))))
pass2
compiling FOO 
finalize
invoke GCC
T
> 

例2

竹内関数のコードです。型推論を用いたとしても引数と返り値が整数であることは推論できますが、それが限界です。竹内関数は膨大な再帰計算を要するため、実用時間内に計算できるのは引数が小整数のときに限られます。従って小整数に限定したコードを生成させ、BIGNUMになる場合は考えない、とコンパイラに教えてあげれば効率の良いコードを生成できます。the構文はインタプリタにおいては効果はありませんが、コンパイラではこの付加データをもとに型推論を行います。

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

> (compile-file "tarai.lsp" 'type)
initialize
pass1
inferencing TARAI
pass2
compiling TARAI 
finalize
invoke GCC
T
> 

例3

アッカーマン関数も、膨大な再帰計算を要し、巨大数を生成します。しかし、パソコンで実用時間内に計算できるのはack(4,1)程度が限界であろうと思います。この場合には計算は小整数の範囲内で収まります。これもthe構文を利用して型情報を追加することで可能となります。

(defun ack (m n)
  (the <fixnum> m)(the <fixnum> n)
  (cond ((= m 0)(+ n 1))
        ((= n 0)(ack (- m 1) 1))
        (t (ack (- m 1) (ack m (- n 1))))))


例4

フィボナッチ数は整数ですが、浮動小数点数により計算させる例です。型推論により定数1.0などから引数と返り値が浮動小数点数であることが導かれます。コンパイラは浮動小数点数に特化したコードを生成します。この場合には型についての付加情報は必要ありません。

(defun fib* (n)
  (cond ((= n 1.0) 1.0)
        ((= n 2.0) 1.0)
        (t (+ (fib* (- n 1.0)) (fib* (- n 2.0))))))


ベンチマーク

Common Lispの代表的処理系であるSBCLとの対比をしました。SBCLには型宣言をつけて高速化させています。

例1 竹内関数

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


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

例2 アッカーマン関数

SBCL
(declaim (ftype (function (fixnum fixnum) fixnum) ack))
(defun ack (m n)
  (declare (optimize (speed 3) (debug 0) (safety 0))
    (type fixnum m)(type fixnum n))
  (cond ((= m 0)(+ n 1))
        ((= n 0)(ack (- m 1) 1))
        (t (ack (- m 1) (ack m (- n 1))))))


* (time (ack 4 1))

Evaluation took:
  4.558 seconds of real time
  4.531250 seconds of total run time (4.531250 user, 0.000000 system)
  99.41% CPU
  14,552,407,668 processor cycles
  0 bytes consed

65533
* 

EISL
> (load "tarai.o")
T
> (ack 4 1)
65533
> (time (ack 4 1))
Elapsed Time(second)=2.382881
<undef>
> 

例4 浮動小数点数によるフィボナッチ

(declaim (ftype (function (float) float) fib*))
(defun fib* (n)
  (declare (optimize (speed 3) (debug 0) (safety 0)) (type float n))
  (if (< n 2.0)
    n
    (+ (fib* (- n 2.0)) (fib* (- n 1.0)))))

* (time (fib* 40.0))

Evaluation took:
  6.479 seconds of real time
  6.468750 seconds of total run time (6.406250 user, 0.062500 system)
  [ Run times consist of 0.156 seconds GC time, and 6.313 seconds non-GC time. ]
  99.85% CPU
  20,682,846,107 processor cycles
  3,973,926,912 bytes consed

1.0233415e8
* 

> (fib* 40.0)
102334155.0
> (time (fib* 40.0))
Elapsed Time(second)=0.479320
<undef>
> 

制限

開発途上にあり、labels、fletといった構文には対応できていません。

今後の展望

型推論器はまだまだ不安定なところがあります。多くのコードで試し、より完成度を上げたところで平成30年6月をもって正式版にしたいと考えています。安定したならば、型推論ありのコンパイルをデフォルトにしたいと考えています。

型推論器の詳細、コードは下記に投稿してあります。
https://qiita.com/sym_num/items/ba3608abebf5c12385c5