【Common Lisp】
the の基本の使い方と考え方
（型の絞り込み）

• the は値を変えず、式の型をコンパイラに伝える特殊形式です
• SBCLはその情報を最適化・コンパイル時警告・実行時型検査の三つに活用します
• 型推論は宣言や条件分岐を材料に絞り込まれ、the は途中で途切れた推論をつなぎます
• 関数入口では check-type で確実に検査し、内側では the と declare で最適化を引き出すのが実用的な使い方です

1. 式の型宣言 the

the は「式の結果」に型を付ける特殊形式です¹。

(the 型 式)Code language: Lisp (lisp)

theは、式の途中に挿入されますが、実行時には何もしません。

(setf z (the fixnum (+ x y)))Code language: Lisp (lisp)

基本的には (the fixnum (+ x y)) は (+ x y) をそのまま返すだけで、その意味は、「(+ x y) の結果は fixnum である」という「型宣言」です。

1.1. 型宣言は型変換ではない

the は変換ではありません。

C言語の「型キャスト」に似ていますが、まったく意味が違います。

int x = (int)3.14Code language: Arduino (arduino)

このC言語のコードでは、 x には 3 が代入されます。

それに対して、the は値を変えません。

(setf x (the fixnum 3.14))
;=> [Condition of type SIMPLE-TYPE-ERROR]Code language: Lisp (lisp)

(the fixnum 3.14) と書いても 3.14 が整数になるわけではありません。
この場合、「3.14はfixnumである」という型宣言は整合しないので、SBCLでコンパイルしたら型エラーになりました²。

Common Lispのtheは、型キャストとはむしろ逆です。
Cのキャストは型システムに強制的に適合させるように変換しますが、the はコンパイラに型情報を提供するだけで、処理系が宣言と矛盾を見つければ警告や検査が入ります。
Common Lispで型変換したいなら coerce や truncate などを使います

つまり、 the は、実行時には透明で、コンパイル時の型推論にだけ情報を持ち込む構文です。
コードの中に埋め込まれたコンパイラへのメッセージというのが、その存在意義です。

1.2. declareとthe

declare で変数に型を宣言できるのに、なぜ the という別の形式があるのか。

declare は変数に対する型宣言です。

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

x という変数が fixnum であることをコンパイラに伝えます。

一方、the は式の返す値に対する宣言です。

(let* ((x (list 'a 'b 'c))
       (y 5))
  (setf (the fixnum (car x)) y)
  x) =>  (5 B C)Code language: Lisp (lisp)

(car x) という式の型が fixnum であることをコンパイラに伝え、コンスセルの要素が fixnum であることが宣言できます³。
変数を経由せず、式にそのまま型を付けられます。

1.3. 型に関する用語の整理

the の話をしていると、似た言葉がいくつも出てくるので、ここで整理しておきます。

用語	英語	意味
型宣言	type declaration	処理系に「この値はこの型である」という前提を渡すこと。declare と the がこれにあたる。型検査を保証しない
型指定	type specifier	fixnum、(integer 0 100)、(simple-array fixnum (*)) のような、型を記述する構文そのもの
型推論	type inference	コンパイラが式や変数の型をコードから推測すること。宣言・分岐・リテラルなどが材料になる
型検査	type checking	値が宣言された型に合うかを確認すること。静的なコンパイル時と動的な実行時の両方がある
型検証	type assertion	実行時に型が正しいことを確認し、違えばエラーにすること。check-type や assert がこれにあたる
型最適化	type-based optimization	型情報をもとに、より特化したコードを生成すること。型宣言の主目的

Common Lispの型宣言は型検査を保証しません。
「この型である」という前提を処理系に渡すだけで、処理系がそれをどう使うかは実装と最適化設定に委ねられています⁴。
ただし、SBCLは、デフォルトではこの型宣言を型最適化だけでなく、型検査にも活用しています。

2. the をSBCLが使う三つの方法

the の型宣言を書くと、SBCLはその情報を三つの目的に使います。

2.1. 最適化

型が確定した式については、SBCLはより特化したコードを生成できます。

たとえば、+ は引数の型が不明なまま呼ばれると、汎用的なコードにコンパイルされます。
整数かもしれない、浮動小数点かもしれない、あるいは全く別のオブジェクトかもしれない、という可能性を全部考慮する必要があるからです。

;; 型情報なし：汎用的な加算
(+ (aref v i) 1)

;; the で型を明示：fixnum 向けの加算に絞れる
(+ (the fixnum (aref v i)) 1)Code language: Lisp (lisp)

一方、型が絞れると、複数の可能性に備えた冗長な処理を省け、効率的なコードにコンパイルできます⁵。

2.2. コンパイル時の整合性確認

さらに、宣言された型の矛盾がコンパイル時に明らかな場合、SBCLは警告やエラーを出せます。

(the fixnum "hello")Code language: Lisp (lisp)

"hello" は文字列で、宣言された型 fixnum ではないことが証明できるので、SBCLはこれをコンパイル時に指摘できます。

ただし、次のような場合はコンパイル時にはわかりません。

(defun f (x)
  (the fixnum (foo x)))Code language: Lisp (lisp)

foo が何を返すかは実行時まで不明なので、コンパイル時には判断できません⁶。

2.3. 実行時の動的型検査

コンパイル時に証明できない型宣言に対して、デフォルトのSBCLは実行時に型検査を追加します。

(defun f (x)
  (the fixnum x))

(f "abc")  ; 実行時に TYPE-ERROR になるCode language: Lisp (lisp)

これはSBCLの安全設定である safety によって変わります。
デフォルトでは証明できない宣言は、アサーションコードを追加して実行時に判定することができます。
ただし、SBCLでもsafety 0 にすると宣言を信じて検査を省き、型が間違っていた場合はエラーではなく未定義動作になります⁷。

3. 型の可能性はコードとともに絞られる

SBCLがコードをコンパイルするとき、変数や式の型は最初 T、つまり何でもありの状態として始まります。
コードが進むにつれて情報が加わり、型の可能性が絞られていきます。

宣言もコードもなければ x はどんな値でもありえます。

(defun f (x)
  (+ x 1))  ; x は T、つまり何でもCode language: Lisp (lisp)

ここに declare を加えると、x は fixnum の範囲に絞られます。

(defun f (x)
  (declare (type fixnum x))
  (+ x 1))  ; x は fixnumCode language: Lisp (lisp)

SBCLの型推論は「広い可能性から始めて、制約を加えるたびに狭める」という方向で動きます⁸。

3.1. 絞り込みの情報源

型の可能性を狭める情報は、複数の場所から来ます。

まず、リテラルは値そのものから型が確定します。
10 は fixnum、"hello" は string です。

また、declare と ftype は、変数や関数に対して明示的に型を与えます。

条件分岐も型情報を生み出します。

(if (typep x 'fixnum)
    (+ x 1)   ; この側では x は fixnum に絞られる
    0)Code language: Lisp (lisp)

then 側では typep の結果から x が fixnum であることが確定するので、SBCLはこの情報を使って分岐内の推論を進めることができます。

the も同じです。
式の結果に型を付けることで、それ以降の推論に使える情報が増えます。

3.2. 式の途中で推論が途切れる場所

declare は変数には届きますが、式の結果には届きません。

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

x は fixnum と伝わっています。
しかし (some-fn x) が何を返すかは、関数の型情報がなければSBCLにはわかりません。
ここで型推論が途切れます。

ここで、some-fn の戻り値が fixnum に収まると分かっているなら、the でそれを明示することで推論を続けられます。
コンパイラはさまざまな可能性を考慮するけど、プログラマは問題の制約条件を知っているからです。

(+ (the fixnum (some-fn x)) 1)Code language: Lisp (lisp)

他にも推論が途切れやすい場所があります。
aref は配列の要素型が宣言されていれば推論できますが、汎用配列の場合は T のままになります。

(aref v i)              ; v の要素型が不明なら T
(the fixnum (aref v i)) ; 明示することで fixnum に絞れるCode language: Lisp (lisp)

また、ループの累積変数も保守的に扱われます。

(loop with total = 0
      for x across arr
      do (incf total (the fixnum x))
      finally (return (the fixnum total)))Code language: Lisp (lisp)

setf で書き換える変数は型が曖昧になりやすく、要所に the を加えると推論がそこで途切れずに続きます⁹。

4. check-type と the の挟み撃ち構造

デフォルトのSBCLを前提にすると、型の安全性は「外側の明示的な検査」と「内側の型宣言による副次的な確認」の二層で保たれています。

書き方	主目的	副次的に起こること
check-type	型検査、安全確認	検査後の型情報が最適化に使われる
assert	条件検査、安全確認	条件が型情報を含むなら、後続の型推論に使われる
typep + 分岐	実行時判定、処理分岐	分岐内で型が絞り込まれ、最適化に使われる
declare	型情報の提供、最適化	安全な SBCL では実行時検査にも使われる
the	式の型情報の提供、最適化	安全な SBCL では実行時検査にも使われる

check-type や assert、typep による分岐は、型検査そのものが目的のコードです。

(defun process (x)
  (check-type x fixnum)   ; ここで確実に検査する
  ...)Code language: Lisp (lisp)

値が期待する型でなければ止まります¹⁰。

一方、declare と the は最適化のために型前提を渡すもので、型検査が主目的ではありません。
ただし、デフォルトのSBCLでは、証明できない型宣言に実行時検査を追加するので、副次的に型の整合性確認としても機能します。

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

つまり、check-type は「ここで必ず確認したい」という意思表示です。
外部入力や関数の入口など、前提が崩れる可能性がある場所に置きます。
一方、the と declare は「この型であるという前提をコンパイラに渡す」もので、SBCLはそれを最適化に使い、証明できなければ実行時検査も追加します。

実用上は、関数の入口では check-type で確実に検査し、内側の計算では declare と the で型前提を渡して最適化を引き出す形になります。

観点	the / declare
出発点	型情報を処理系に渡す
主目的	型推論・最適化を助ける
安全な SBCL での効果	証明できない制約は実行時検査されうる
静的に矛盾する場合	コンパイル時に警告・エラーになりうる
効率優先の場合	検査を省き、宣言を前提として使いやすい
本質的なイメージ	型の可能性を制約で絞る

ただし、safety 0 にすると declare と the の実行時検査は消え、残るのは最適化の前提だけです。
型宣言が間違っていたとき、check-type がなければ気づく手段がなくなります。
safety 0 に踏み切る前に check-type で入口を固めておく理由はここにあります。

1. the はCommon Lispの特殊演算子のひとつです。特殊演算子の集合は言語仕様で固定されており、ユーザーが新たに定義することはできません。if、let、progn などと同じカテゴリに属します。 – CLHS: Special Forms
2. Common Lisp HyperSpecでは、the で宣言した型と実際の値が合わない場合の結果は「未定義（the consequences are undefined）」と明記されています。つまり標準仕様は「必ずエラーにする」とは定めておらず、処理系の判断に委ねています。 – CLHS: Special Operator THE
3. HyperSpecでは、the を setf と組み合わせる用途も言及されています。(setf (the fixnum (car x)) y) のように書くと、型宣言が代入先に転送されます。 – CLHS: Special Operator THE
4. Common Lisp標準（ANSI CL）では、型宣言の効果は実装依存とされています。SBCLのように型宣言を実行時アサーションとして扱う処理系がある一方、宣言を最適化ヒントとしてのみ使い、検査を行わない処理系もあります。 – Compile Time Type Checking in Common Lisp
5. fixnum の範囲は処理系依存で、Common Lisp標準は最低限 (signed-byte 16) のスーパータイプであることを要求します。64bit環境のSBCLでは -2^62 から 2^62-1（4611686018427387903）です。most-positive-fixnum で確認できます。 – The Common Lisp Cookbook – Numbers
6. SBCLの型推論はCMU Common Lisp（CMU CL）の流れを受け継いでおり、他のLisp処理系より積極的に型情報を活用します。SBCLマニュアルでは「SBCLはほとんどの型宣言を盲信せず、アサーションとして扱う」と説明されています。 – SBCL User Manual – Handling of Types
7. SBCLの型検査方針は三段階です。Full Type Checks（デフォルト、(or (>= safety 2) (>= safety speed 1))）、Weak Type Checks（型を粗い上位型に単純化して検査）、No Type Checks（(= safety 0)、全宣言を無検査で信じる）。safety 0 ではヒープ破壊が起きうると明記されています。 – SBCL User Manual – Declarations as Assertions
8. Common Lispの型階層では T がすべての型のスーパータイプです。あらゆる値は T 型に属します。逆に NIL 型はいかなる値も含まない空の型で、型の交差が空であることを表すのに使われます。 – CLHS: Type Specifiers
9. 型宣言が実際に最適化に効いているかは (disassemble #'関数名) で確認できます。SBCLは型が曖昧で最適化できない箇所に note: unable to optimize という警告を出します。この警告を手がかりに the や declare を加えていくのが、型宣言チューニングの実践的な進め方です。 – SBCL User Manual
10. check-type はエラーを通知するだけでなく、store-value リスタートを提供します。デバッガから正しい値を入力し直して処理を続けることができます。assert と似ていますが、変数への再代入に特化した設計です。 – CLHS: Macro CHECK-TYPE