12 分で読了 #compilers #semantic-analysis
このページの目次

型システム

型チェックは、コンパイラによるプログラムの静的検証——実行前に型エラーが発生しないことを証明するものです。単純な等式チェックから Hindley-Milner 推論、サブタイプと共変性・反変性、そしてジェネリクスの単一化と型消去という2つのアプローチまで。

概要

シンボルテーブルとスコープは「この名前はどの定義を指すのか」を解決します。型システムは次のレベルを解決します：⁠これらの名前の型が合法的に組み合わせられるか⁠——x + y において x と y は足し合えるか？f(a) の引数の型は一致しているか？型チェック(type checking)は判定を行うプロセスであり、型推論(type inference)は省略された型注釈を自動的に補完するものです。本稿では、「単純な型チェック→HM推論→サブタイプ→ジェネリクス」という難易度の勾配に沿って、型のエンジニアリング的な実装を明確に解説します。

型チェック: 各部分木の検証

型チェックは AST 上でボトムアップ（下位から上位へ）に行われます。

typecheck(expr):
    match expr:
        Number(n) → Int
        Binary(op, left, right) →
            t_left = typecheck(left)
            t_right = typecheck(right)
            if op is '+' and t_left == Int and t_right == Int:
                return Int
            else:
                report_type_error("cannot add {t_left} and {t_right}")
        Variable(name) →
            lookup(name).type                 ← シンボルテーブルから型を取得
        Call(func, args) →
            t_func = typecheck(func)
            if t_func is not Function:
                error
            for (arg, param_type) in zip(args, t_func.params):
                t_arg = typecheck(arg)
                if t_arg != param_type:
                    error
            return t_func.return_type

骨格は極めて単純です：AST を再帰的に走査し、各ノードがその子ノードの型がノードの型ルールに適合しているか検証します。真の複雑さは、⁠型の表現⁠（関数、ジェネリクス、代数的データ型などの内部構造の保存方法）、⁠型の等価性⁠（2つの型が「同じ」とは何か——構造的等価性 vs 名義的等価性）、そしてジェネリクスのインスタンス化⁠（T=Int における List<T> の動作）にあります。

型の表現

型システム内部では、AST に似たデータ構造を用いて型を表現します。

enum Type {
    Int,
    Float,
    Bool,
    String,
    Function(Vec<Type>, Box<Type>),    // params → return_type
    Struct(String, Vec<(String, Type)>),  // name + fields
    Enum(String, Vec<(String, Vec<Type>)>),  // name + variants
    TyVar(u32),                        // 型変数。一意のIDで識別（O(1) 比較）
    Apply(Box<Type>, Vec<Type>),       // ジェネリクスインスタンス化: List<Int>
}

再帰的な表現——Function の引数と戻り値はどちらも Type であり、Apply(List, [Box<Type>]) はネスト可能です（例：Map<String, List<Int>>）。

型の等価性: 構造的 vs 名義的

2つの型がいつ「同じ」とみなされるか？

  • 構造的等価性(structural equivalence): 「見た目が同じなら同じ」。struct { x: Int, y: Float } と struct { x: Int, y: Float } は、異なるモジュールで定義されていても同一の型とみなされます。Go や TypeScript がこれを採用しています。代償として、偶然同型であっても意味が全く異なる型（例：Point{x,y} と Vector{x,y}）が同一の型として扱われてしまいます。
  • 名義的等価性(nominal equivalence): 「名前が同じでなければ同じではない」。Point{x:Int, y:Float} と Vector{x:Int, y:Float} は異なる型です。Rust、Java、C++ がこれを採用しています。型チェック時には、フィールドを一つずつ比較するのではなく、2つの型の「構造的な名前」のペアを比較します。名義的等価性はより安全（意味の混同を防ぐ）ですが、ジェネリクス推論をサポートするために、型制約を表現するための追加メカニズム（Rust のトレイト境界、Java の extends など）が必要です。

Hindley-Milner 型推論: 型を書かなくてもチェックできる

HM は ML 系言語（OCaml、Haskell）の型推論の基礎であり、その核心は unification（合一） にあります：2つの型式が与えられたとき、それらを等しくする型変数の置換の組が存在するかどうかを確認します。

推論プロセス (擬似コード):
  AST の各ノードに対して型変数（t1, t2, ...など）を生成
  ノードに対して型ルールを適用し、制約を生成:
    Number(n)     → t == Int
    x + y         → t_x == Int, t_y == Int, t_result == Int
    if cond a b   → t_cond == Bool, t_a == t_b, t_result == t_a
  制約集合の解決 — unification:
    各等式 t_i == t_j について:
      t_i が未束縛の型変数であれば、t_i → t_j を束縛
      t_j が未束縛の型変数であれば、t_j → t_i を束縛
      両側が具体的な型（Int と Float など）であれば、等しさをチェック——不一致なら型エラー

Unification は決定論的です——等式に出会ったらルールに従って置換し、バックトラックして再試行する必要はありません。

HM の制限：⁠多相性は let によってのみ導入される⁠（let-polymorphism——let id = fn x => x における id は多相的であり、let 束縛箇所で汎化されます。関数引数の多相性は型推論によって自動的に決定されます）。これは HM の let-polymorphism ルールによるものです：let 束縛箇所でのみ Generalization（汎化）が行われ、lambda 束縛の変数は汎化されません。これにより、推論の決定可能性が保証されます——Hindley-Milner は HM-valid なプログラムに対して、有限ステップ内で主型(principal type)を必ず導出でき、無限ループに陥ることはありません。

サブタイプ: 置換可能性の原則

Dog <: Animal（Dog は Animal のサブタイプ）のとき、Animal を要求する場所には Dog を渡すことができます。サブタイプは型チェックに「型は白か黒かの比較ではない」という概念を追加します。

  • 共変(covariant): Dog <: Animal ならば List<Dog> <: List<Animal>。これは読み取り専用の構造に対して安全です——Java の List<? extends Animal> など。
  • 反変(contravariant): Fn(Animal) <: Fn(Dog)。関数の引数は反変です——Animal を食べられる関数は、Dog も食べられます（Dog <: Animal であり、Animal の集合は Dog を包含するため）。逆に、Fn(Dog) は Fn(Animal) を置き換えることはできません⁠——Dog しか食べられない関数は Cat を食べられませんが、Fn(Animal) が要求される場所には Cat が渡される可能性があるためです。
  • 不変(invariant): Array<Dog> と Array<Animal> は無関係です。⁠読み書き可能な構造（配列は読み書き可能）に対しては不変でなければなりません——さもないと、arr: Array<Animal> に Cat を入れた後、既存の Array<Dog> 参照がすべての要素を Dog だとみなし、型安全性が破綻します。

Rust は実際のサブタイプの使用において非常に抑制的です：⁠ライフタイムのみがサブタイプ関係⁠（'static <: 'a）であり、他の型はすべて名義的等価性を持ち、構造的なサブタイプは存在しません。

ジェネリクス: 多相性の異なる実装

ジェネリクス（List<T>）は、コンパイル後にどのようにコードを生成するか？

単一化(monomorphization)

Rust、C++、Swift がこれを採用しています：実際の型引数ごとに独立した機械語を生成します。

fn identity<T>(x: T) → T           // ジェネリクス定義 (IR 内で保持)
identity::<i32>(42)                 // identity_i32 の関数体を生成
identity::<String>("hello")         // identity_String の関数体を生成

利点：ランタイムオーバーヘッドゼロ（直接呼び出し、間接呼び出しなし）、各 T ごとに独立して最適化可能（コンパイラは T=i32 を見た場合、インライン展開や定数畳み込みが可能）。欠点：コードの肥大化——各 T ごとに1つ。ただし Rust では、十分なデジュープリケーション（同じ Option<i32> は1回だけ生成）があるため、実用上の制限は大きくありません。

型消去(type erasure)

Java、Scala、Kotlin がこれを採用しています：ジェネリクスはコンパイル時のみ存在し、ランタイムではすべての List<T> が List<Object> となります。

List<String> xs = ...;
String s = xs.get(0);     ← コンパイラが暗黙の cast を挿入: (String) xs.get(0)

利点：コードは1つだけで、肥大化しない。欠点：プリミティブ型をジェネリクスに直接使用できない（List<int> は不正、List<Integer> のようにボックス化する必要がある）、ランタイムに cast とボックス化のオーバーヘッドが発生する。

Trait/Typeclass: 制約多相性

ジェネリクスの引数には制約が必要です：T が「足し算できる」「比較できる」「印刷できる」ものであることを指定します。Rust の trait、Haskell の typeclass はこの制約の表現方法です。コンパイラの処理：

  • Rust: fn sum<T: Add>(xs: &[T]) → T に対して、単一化により各 T ごとに sum の1つを生成し、引数の Add::add 呼び出しは静的ディスパッチ——コンパイル時に T::add のどの実装にジャンプするかが決定されます。仮想テーブルの検索は行われません。
  • しかし、トレイトオブジェクト dyn Add が現れると、コンパイラは vtable（仮想テーブル）を使用します——関数ポインタを格納した構造体であり、ランタイムに検索されます。

Trait solver は Rust コンパイラの中で最も複雑なコンポーネントの一つです。その役割：T: Add<Output = T> と Vec<T> が与えられたとき、すべての制約が充足可能であることを検証する——これは本質的に Prolog 風の論理プログラミングです（Chalk ライブラリは、Rust のトレイトルールを Prolog ルールに変換して求解します）。

トレードオフと失敗パターン

  • 型推論失敗時のエラーメッセージが分かりにくい⁠: HM の unification は失敗した場合、「2つの型が一致しない」ということしか分かりません。「なぜか」は分かりません——「expected Foo, found Bar」と表示しても、「ここで呼び出している関数は Foo を期待しているが、渡された x は Bar である。なぜなら3行前で Bar を代入したからだ」とは説明しません。→ 現代のコンパイラ（Rustc など）は、推論中に「制約の由来」を記録し、推論失敗後に制約チェーンを遡ってメッセージを診断します。
  • 推論の非決定性⁠: HM の外側の特徴（GADT、型ファミリー、rank-N 多相性など）を追加すると、型推論が決定不能になる可能性があります——コンパイラが永遠に推論を続けることがあります。→ 制限を加える（Haskell は GADT と型ファミリーに対して型注釈を要求、Rust は推論を関数内に制限し、関数間で推論を行わない）。
  • 単一化によるコンパイル時間の増大⁠: C++ テンプレートと Rust ジェネリクスの両方で、コンパイル時間の爆発を引き起こす可能性があります → 必要に応じて単一化（理論的に可能なすべてのインスタンスを生成しない）、デジュープリケーション（同じ組み合わせは1回だけ生成）。

参考文献

  • Pierce: "Types and Programming Languages"(TAPL) — 型理論の標準的な教科書。単純型→サブタイプ→多相性→HM をカバー
  • Dragon Book: Chapter 6, Type Checking — コンパイラにおける型チェックの実装
  • Rust Chalk: https://github.com/rust-lang/chalk — Rust trait solver の論理プログラミングによる実装

Keywords: type checking, type inference, Hindley-Milner, unification, type variable, principal type, subtyping, covariance, contravariance, invariance, monomorphization, type erasure, generic, trait, typeclass, vtable, static dispatch, dynamic dispatch, trait solver, nominal equivalence, structural equivalence, let-polymorphism

関連ページ

© 2026 liz's doc