型システム

型システムは、プログラムの構成要素がどのように合法的に組み合わせられるかを規定する。型チェックはルールを検証し、型推論は省略された型情報を補完する。それらがどのようなエラーを排除できるかは、具体的なルールとその信頼性次第であり、すべてのランタイムエラーやビジネスロジックエラーがないことを保証するものではない。

型安全性の形式的証明では、通常、良型なプログラムが特定の規則に従って実行できない状態に陥らないことが論じられる。nullポインタ、配列の範囲外アクセス、ゼロ除算などが静的に排除されるかどうかは、言語がこれらの操作をどのようにモデル化するかによる。

型ルール：局所的な判断を接続する

環境 $\Gamma$ において式 $e$ が型 $T$ を持つことを Γ ⊢ e : T と表す。単純な整数の加算ルールでは、左右両側が Int であり、結果も Int であることが要求される。if 文では、条件式が Bool であり、両方の分岐が言語定義された共通の結果型を満たす必要がある。

関数呼び出しでは、まず呼び出し可能性と引数の数をチェックし、その後、引数の型やその他の制約を項目ごとにチェックする。zip によるペアリングのみを使用すると、余分な引数や不足している引数が見逃される可能性がある。実際の言語では、デフォルト引数、可変長引数、オーバーロード、および変換も関与する可能性がある。

チェックは必ずしもボトムアップだけではない。双方向型チェックは、「式から型を合成する」と「期待される型のもとで式をチェックする」を組み合わせ、コンテキストを利用して曖昧さを減らし、エラーの位置を改善できる。

型の表現と同一性

内部表現では、通常、基本型、関数、型コンストラクタの適用、型変数、および宣言による同一性が区別される。再帰型は、ID または間接参照によって接続され、構造全体を無限に複製してはならない。

名義的型同一性は、単純な文字列名の比較ではなく宣言に由来する。2つのモジュールがどちらも Point を宣言していても、それらは異なる型である可能性がある。構造的ルールは、構成要素に基づいて特定の関係を判断する。型の等価性、代入互換性、部分型、および明示的な変換は異なる問題である。

言語はルールを混合することもできる。Go の名前付き型同一性と非構造化型ルールは異なり、インターフェース実装はメソッド集合を利用するため、「Go では見た目が同じ構造体はすべて同じ型である」と一般化することはできない。Go 型同一性ルール

統合：型式を等しくするための置換を求める

未知の型に変数 α、β を導入する。関数適用 f(3) に対して、type(f)=Int→α を生成できる。もしコンテキストが結果として Bool を要求するなら、α=Bool が追加される。

統合はコンストラクタを再帰的に比較する：List<α> と List<Int> から α=Int を導く。関数型は引数と結果を項目ごとに比較し、Int と Bool は失敗する。置換は一貫して伝播する必要があり、現在の型名だけを修正するだけでは不十分である。

Occurs check（出現検査）は、許されない無限型の構築を防ぐ。例えば α=α→β のような場合である。α が束縛される型に含まれている場合、通常の HM 型構文では拒否されるべきである。このステップを無視すると、ソルバーがループしたり、モデル外の型を受け入れたりする可能性がある。

最小限の統合器：既存の置換を適用し、新しい制約を構築する

? で始まる文字列を型変数、通常の文字列を基本型、タプルをコンストラクタ適用（例：("List", "?a")）として表す。関数型は二元コンストラクタ Fn として一様に表現される。これは有限の一次型項モデルであり、部分型、オーバーロード、再帰型、または完全な HM 汎化を扱わない。

def variable(t):
    return isinstance(t, str) and t.startswith("?")


def resolve(t, substitution):
    if variable(t) and t in substitution:
        return resolve(substitution[t], substitution)
    if isinstance(t, tuple):
        return (t[0], *(resolve(x, substitution) for x in t[1:]))
    return t


def occurs(v, t):
    return v == t or (isinstance(t, tuple) and any(occurs(v, x) for x in t[1:]))


def unify(a, b, substitution):
    a, b = resolve(a, substitution), resolve(b, substitution)
    if a == b:
        return
    if variable(a):
        if occurs(a, b):
            raise TypeError("infinite type")
        substitution[a] = b
        return
    if variable(b):
        unify(b, a, substitution)
        return
    if (isinstance(a, tuple) and isinstance(b, tuple)
            and a[0] == b[0] and len(a) == len(b)):
        for x, y in zip(a[1:], b[1:]):
            unify(x, y, substitution)
        return
    raise TypeError("type constructor mismatch")


subst = {}
unify(("Fn", "?a", "?b"), ("Fn", "Int", ("List", "?c")), subst)
unify("?c", "Bool", subst)
assert resolve(("Fn", "?a", "?b"), subst) == ("Fn", "Int", ("List", "Bool"))
for a, b in [("Int", "Bool"), ("?a", ("Fn", "?a", "?b")),
             (("Pair", "Int"), ("Pair", "Int", "Bool"))]:
    try:
        unify(a, b, {})
    except TypeError:
        pass
    else:
        raise AssertionError("incompatible types accepted")
# 間接的な自己参照も拒否する：?a = ?b の後、?b = List<?a>。
indirect = {}
unify("?a", "?b", indirect)
try:
    unify("?b", ("List", "?a"), indirect)
except TypeError:
    pass
else:
    raise AssertionError("indirect occurs check missed")

最初の制約は ?a=Int、?b=List<?c> を得、その後 ?c=Bool を得る。関数型を読み出す際には、置換を再帰的に適用して Int→List<Bool> を得る必要がある。現在のノードだけを変更すると、更新されていない ?c が残ってしまう。間接的な自己参照のテストは、occurs check が既存の置換が展開された後に行われる必要があることを示している。

ここで失敗が発生した場合、現在のソルビングを直ちに終了する。オーバーロードの候補試行に使用する場合、以前の再帰ステップで substitution が変更されている可能性があるため、失敗後はその分岐を破棄するかロールバックし、半成功の置換を持って次の候補を試してはならない。型項の入力構築はフロントエンドによって合法であることが保証され、実際の処理系では別途深さや作業量の制限を設定する必要がある。

置換はどこまで伝播されてこそ、型が本当に解けたと言えるか？

同じ変数が複数の位置に現れる場合、各位置は同じ置換として解釈されなければならない。以下では互換性のある制約を選択することも、コンストラクタの衝突や間接的な自己参照を構築することもできる。エラーが発生した場合、全体のソルビング結果は無効になる。保持される処理記録は、失敗がどこで発生したかを説明するためのものであり、すでに修正された半分の置換を次の候補に持ち込むことを許可するものではない。

Hindley–Milner：汎化とインスタンス化の両方が不可欠

単純化された純粋な HM 言語では、let id = fun x -> x は α→α と推論され、let において外部環境に自由に出てこない型変数が型スキーマ ∀α. α→α に汎化される。

id を使用するたびに、新しい型変数付きの型にインスタンス化される。したがって、id 1 と id true はそれぞれ Int→Int と Bool→Bool を使用でき、2回の呼び出しが同じ束縛待ち変数を共有することはない。

ラムダパラメータは基本的な HM ではこのような let 汎化を行わない。fun f -> (f 1, f true) において f を2つの型で呼び出せる多型関数として扱いたい場合、これは単純なルールを超えている。関数パラメータの任意の高階多型が自動的に HM によって推論されるとは言えない。

可変参照などのエフェクトを持つ言語では、汎化を制限する必要がある。例えば ML 系言語の value restriction は、共有可変ユニットを誤って複数の型として扱うのを防ぐ。実際の言語は純粋な HM を超え、型クラス、部分型、または局所注釈を追加することがあり、推論アルゴリズムと保証も変化する。

汎化によって外部環境の未知変数も任意の型にしてはならない

環境にすでに x:?a があり、let keep = fun u -> x の型が ?b→?a であると仮定する。?b は汎化できるが、?a は環境に由来するため、x の実際の型に従って制約される。したがって、スキーマは ∀β. β→?a であり、∀αβ. β→α ではない。後者のスキーマは、呼び出し側が返り値の型を任意に選択できるかのように誤って許可し、同じ x が同時に Int と Bool になり得ることを意味してしまう。

汎化集合は通常 free(type) − free(environment) と表記される。インスタンス化はスキーマで量化された変数だけを新鮮なものに更新し、環境の未知変数への関連付けは保持される。前述の統合器は等価制約のみを解決しており、このステップを実装していないため、そのまま完全な Algorithm W と呼ぶことはできない。

共有可変ユニットは問題をより顕著にする。もしある記憶領域が誤って汎化され、アクセスするたびに任意の要素型にインスタンス化されると、最初に Int として書き込み、その後関数型として同じ内容を読み出すことが可能になる。OCaml は弱型変数と value restriction などのルールを用いてこの状況を制約し、具体的な緩和ルールでは共変性も利用される。OCaml の多型と可変状態

2回の使用において、どの未知変数がそれぞれ新鮮化されるか？

汎化式における減算には具体的な意味がある。環境から継承された未知変数は、各呼び出し側に任意に選択させることはできない。id にはそのような返り値の依存関係がない。keep は外部の x を返すため、2回の呼び出しの引数型が異なっていても、返り値型は依然として関連付けられている。下図は、2つの呼び出しインスタンスを用いて、「量化変数の新鮮化」と「環境変数の保持」を同時に示している。

$$Q=\mathrm{FTV}(\tau )\setminus \mathrm{FTV}(\Gamma ),\sigma =\forall Q.\tau$$

部分型と共変性：どの置換が安全か

Dog<:Animal の場合、Animal の能力だけを必要とする場所には Dog を受け取ることができる。関数の場合、任意の Animal を処理できる関数は、Dog だけを渡す呼び出し元に使用できる。入力位置では反変性が、出力位置では通常共変性が現れる。

読み書き可能なコンテナが Box<Dog> を直接 Box<Animal> として許可すると、ユーザーは Cat を書き込み、元の Dog のビューからそれを読み出す可能性があるため、通常は不変であるか、またはランタイムチェックや制限付きインターフェースなどの他の設計が必要である。

読み取り専用インターフェースが共変であるための前提は、そのインターフェースを通じて互換性のない値を書き込む能力が本当にないことである。共変性は、型パラメータが各位置でどのように使用されるかによって決定され、List や Array という名前が見えただけで一律に結論を下すことはできない。

Rust の部分型は主にライフタイムと高階ライフタイム型を中心に展開され、型コンストラクタはそれぞれ独自の共変性を持つ。それを「他のすべてのものは名前だけを比較する」と単純化することはできない。Trait 実装と型強制は、通常の継承部分型とは等しくない。Rust の部分型と共変性

関数の置換において、なぜ入力方向が逆になるのか？

関数型を呼び出し側の間の集合的契約と見なすと、2つの方向を直接読み取ることができる。呼び出し側が実際に渡す可能性のある集合は、候補が処理できる集合に含まれている必要がある。候補が返す可能性のある集合は、呼び出し側が許可する集合に含まれている必要がある。以下では、呼び出し入力を Dog に固定し、候補の入力、候補の出力、および呼び出し側の出力要件をそれぞれ変更できる。金色の値は、カバーされていない入力や範囲外の出力を具体的に示す。

$$(A_c\to R_c)<:(A_e\to R_e)\text{if}{A}_e<:A_c\wedge R_c<:R_e$$

ジェネリクスのセマンティクスとマシンコード戦略の分離

言語とコンパイラは戦略を組み合わせることができる。Swift や他の言語のすべてのジェネリクスがモノモーフィゼーションしかないとは断言できず、Java のすべての型情報が List<Object> というリテラルになるわけでもない。消去ルール、境界、およびメタデータの保持には具体的な仕様がある。

特殊化は特定の間接呼び出しを減らすものの、ジェネリックプログラム全体が「ランタイムオーバーヘッドゼロ」になるわけではない。割り当て、実際のアルゴリズム、およびコードキャッシュは存在し続ける。コンパイラは同等のインスタンスをマージすることもある。

Trait / Typeclass：制約能力の解決

制約 T が某操作をサポートすることは、必要な実装や関連型などの条件をチェックすることを意味する。解決は再帰的に新しい義務を生成し、一貫性、曖昧さ、および終了戦略に関与する。静的ジェネリック呼び出しと動的インターフェースオブジェクトは、異なるディスパッチ方式を持つ。

任意の trait を直接有効な dyn Trait と書くことはできない。オブジェクト互換性、関連型、およびメソッドシグネチャには要件がある。理解する際は、まず「T に能力があることをチェックする」と「ランタイムで実装をどのように見つけるか」を区別する。

エラーメッセージも型システム実装の一部である

制約の出所を保持する：どの実引数、どの返却位置、どの宣言が期待される型を生成したか。エラーリカバリには、マーク付きの未知型またはエラー型を使用して連鎖的なエラー報告を減らすことができるが、成功したコード生成時には証明された正しさとして扱ってはならない。

実際の推論では、リソース制限と明確な注釈入口が必要であり、複雑なインスタンスによる極端に長いコンパイルを避ける必要がある。言語機能の追加後に決定可能かどうかは、組み合わせたルールに基づいて分析する必要があり、機能名だけで判断してはならない。

参考

• Go Specification：Type Identity。
• Rust：Subtyping and Variance。
• シンボルテーブルとスコープ、コンパイル時メタプログラミング。

Keywords: 型チェック, 推論, 統合, 出現検査, Hindley-Milner, 汎化, 部分型, 共変性, モノモーフィゼーション