【Common Lisp】
SBCLの型宣言と「静的型検査」

by

関連記事

1. 型宣言と型注釈

Common Lispには型宣言があります。
たとえば、関数の引数に fixnum と宣言できます。

(defun f (x)
  (declare (type fixnum x))
  (1+ x))Code language: Lisp (lisp)

ただし、これはRustやHaskellの型注釈とは意味が根本的に違います。
Rustでは型の不整合はプログラム全体の静的解析でコンパイル時に検出されます。
SBCLの型宣言は、動的なCommon Lispの値の流れの上に置かれた「型についての主張」です1。

SBCLはその主張を最適化、型推論、安全設定での実行時検査という三つの目的に使います2。

1.1. 証明できる場合と証明できない場合

SBCLの文脈で「証明できる」とは、コンパイル時の型推論だけで、その値が宣言型に必ず入ると分かる場合のことです。
「証明できない」とは、値が外部入力・関数引数・汎用的な計算結果に依存していて、コンパイル時だけでは保証できない場合です。

証明できる例を見てみます。

(defun g ()
  (let ((x 10))
    (declare (type fixnum x))
    (1+ x)))Code language: Lisp (lisp)

x はその場で 10 に束縛されています。
10 が fixnum であることはコンパイル時に明らかなので、この宣言のための実行時型チェックは不要です3。

一方、これは証明できません。

(defun h (x)
  (declare (type fixnum x))
  (1+ x))Code language: Lisp (lisp)

x は外から渡されます。
コンパイラはこの関数が将来どんな値で呼ばれるかを知りません。
安全な設定では、関数の入口で「x が本当に fixnum か」を実行時に確認します。

(h "abc")  ; 実行時に型エラーになるCode language: Lisp (lisp)

read を使う場合も同様です。

(defun read-fixnum-and-add ()
  (let ((x (read)))
    (declare (type fixnum x))
    (1+ x)))Code language: Lisp (lisp)

read が何を返すかはコンパイル時に分からないので、x が fixnum であることは実行時まで確認できません4。

条件分岐から型情報を推論できる場合もあります。

(defun maybe-add (x)
  (if (fixnump x)
      (1+ x)
      0))Code language: Lisp (lisp)

then 側では fixnump によって型が絞られています。
SBCLはこのような分岐から型推論を進め、その側では x を fixnum として扱えます。

1.2. the も証明できなければチェックされる

the は「この式の値は指定の型である」という主張です5。

(defun k (x)
  (the fixnum x))Code language: Lisp (lisp)

x が引数ならコンパイル時に保証できないので、安全な設定では実行時チェックになります。
リテラルなら話が変わります。

(defun k2 ()
  (the fixnum 100))Code language: Lisp (lisp)

100 が fixnum であることは明らかなので、実行時チェックは不要です。

算術演算の結果にも気をつける必要があります。

(defun add1-fixnum (x)
  (declare (type fixnum x))
  (the fixnum (1+ x)))Code language: Lisp (lisp)

x が fixnum でも、(1+ x) が常に fixnum 範囲に収まるとは限りません。
x が最大の fixnum なら結果はオーバーフローします。
コンパイラが範囲を証明できなければ、(the fixnum (1+ x)) も実行時検査の対象になります6。

入力範囲を狭めると証明しやすくなります。

(defun add1-small (x)
  (declare (type (integer 0 100) x))
  (the (integer 1 101) (1+ x)))Code language: Lisp (lisp)

x が 0 から 100 なら、(1+ x) は必ず 1 から 101 です。
コンパイラがこれを追えるので、実行時チェックを省ける可能性が高くなります。

2. declare と declaim (ftype ...) の違い

defun 内の引数 declare は、主に関数本体と関数入口への型情報です。
これは「呼び出し側のコンパイル時に型チェックが走る」という意味ではありません。

(defun f (x)
  (declare (type fixnum x))
  (1+ x))

(defun g ()
  (f "abc"))  ; コンパイル時に警告が出るとは限らないCode language: Lisp (lisp)

f の declare は、f の内部で x を fixnum として扱う宣言です。
同じコンパイル単位内であれば、SBCLの型推論によって呼び出し側に情報が波及することがあります。
別ファイルや別コンパイル単位では安定しません。

呼び出し側にも型情報を確実に伝えたいときは、declaim (ftype ...) を使います7。

(declaim (ftype (function (fixnum) fixnum) f))
(defun f (x)
  (declare (type fixnum x))
  (1+ x))

(defun g ()
  (f "abc"))  ; コンパイル時に警告が出やすくなるCode language: Lisp (lisp)

declaim (ftype ...) は、関数 f の外部から見える関数型をコンパイラ環境に宣言します。
f を呼ぶ側をコンパイルするときに「f は fixnum を受け取る」と分かるので、型の不整合を検出しやすくなります。

SBCLのマニュアルには、ftype 宣言を defun より後に置いた場合、その関数自身は型チェックを行わず、呼び出し側が宣言型を盲信するという実装上の制限が記されています8。
declaim (ftype ...) は defun より前に書くのが安全です。

2.1. safety 設定が変わると何が起きるか

SBCLの型宣言の挙動は、optimize の safety 設定に依存します。

(declare (optimize (safety 0) (speed 3)))Code language: Lisp (lisp)

(safety 0) では、型宣言を盲信して実行時チェックを省きます。
型が間違っていると、ヒープ破壊などの未定義動作につながり得ます9。
デフォルトの安全設定では、証明できない宣言は実行時 assertion として残ります。

パフォーマンスを優先して安全設定を下げるときは、型の正確さに自信がある部分だけに限定するのが賢明です。

3. まとめ

コードの形証明しやすいか理由
リテラル値しやすい値がコンパイル時に明らか
狭い整数範囲の計算しやすい範囲推論で追える
fixnump 等で分岐した内側しやすい条件分岐で型が絞られる
関数引数への型宣言しにくい呼び出し時の値は不明
read や外部入力できない実行時まで値が不明
他の関数の戻り値場合による関数の型情報やインライン展開次第
the による結果型宣言場合による式の結果範囲を証明できるか次第

declare は静的型システムではなく、SBCLが最適化・型推論・実行時型確認の三つに使う宣言です。
Rustのように「型エラーはコンパイル時にすべて潰す」とはなりません。
ただのコメントでもありません。
宣言の粒度と安全設定を意識して使えば、コンパイル時警告と実行時チェックの両方を引き出せます。

  1. SBCLマニュアルは「宣言は一般的にアサーション（assertion）として扱われる」と明記しています。このセクションは “Declarations as Assertions” として独立して解説されています。 – SBCL User Manual – Declarations as Assertions
  2. SBCLのtype checkingポリシーは safety の値によって三段階に分かれます。(or (>= safety 2) (>= safety speed 1)) のときは全宣言を精確に実行時検査します。safety が低い中間段階では型を上位型に簡略化した弱い検査になります。(= safety 0) では検査を省略し、引数カウントや配列境界チェックも無効になります。 – SBCL User Manual – Handling of Types
  3. fixnum はCLHSで「most-negative-fixnum 以上 most-positive-fixnum 以下の整数」と定義されており、正確な範囲は実装依存です。CLHSは (signed-byte 16) の上位型であることを保証します。64bit SBCL では most-positive-fixnum は 4611686018427387903（2の62乗から1を引いた値）です。 – CLHS: Type FIXNUM
  4. read はリーダーマクロや *read-eval* の設定に応じてあらゆる Lisp オブジェクトを返し得ます。型を限定したいときは parse-integer や check-type など、特定の型に絞った入力関数や検査を組み合わせるのが一般的です。 – Common Lisp Cookbook – Type System
  5. CLHSでは the を「値型を宣言するスペシャルフォーム」と定義しています。コンパイラはその情報を最適化に使ってよく、型が合わない場合の動作は実装依存です。SBCLはデフォルトで実行時チェックを行います。 – CLHS: Special Operator THE
  6. CLHSのTYPE宣言の解説には、引数が fixnum であっても (+ x y) の結果が fixnum に収まる保証はないと明記されています。中間値がオーバーフローする場合があるため、範囲を絞った the を細かく入れるか、演算を分けて書くことを推奨しています。 – CLHS: Declaration TYPE
  7. declaim はトップレベルで使うグローバル宣言マクロです。proclaim と似ていますが、declaim はコンパイル時にも副作用を及ぼします。ただし、CLHSはファイルコンパイル後にその副作用が持続するかどうかを未規定としています。SBCLでは declaim の効果はそのファイルのコンパイル中に有効ですが、ファイルをまたいで確実に伝えるには明示的に前方に配置する必要があります。 – Common Lisp Cookbook – Performance Tuning
  8. SBCLのmanページには「PROCLAIM または DECLAIM で関数の戻り型を指定すると、コンパイラはチェックなしにその宣言を信じる」と書かれており、これはバグとして認識されています。戻り型が間違っていても、コンパイル時に検出されずに誤った結果を返す可能性があります。 – SBCL man page – Known Bugs
  9. safety が低い設定では、引数カウントチェックや配列境界チェックも同時に無効になります。SBCLマニュアルは「type errorsはヒープを破壊するおそれがある」と明記しており、既存のプログラムを移植したり最適化する際にはまずフルチェック（高safety）でテストしてから安全設定を下げることを推奨しています。 – SBCL User Manual – Getting Existing Programs to Run