12 分で読了
このページの目次

型システム

型チェックは、プログラムの静的検証——実行前に型エラーが発生しないことを証明する——です。単純な等式チェックから 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 名義的等価性)、そしてジェネリクスのインスタンス化⁠(List<T> において T=Int のときの挙動)にあります。

型の表現

型システム内部では、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++ がこれを使用します。型チェック時、比較されるのは一対の型の「構造的な名前」であり、フィールドを一つずつ比較するわけではありません。名義的等価性はより安全 (意味の混同を防ぐ) ですが、ジェネリクス推論をサポートするために、追加のメカニズム (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 束縛箇所のみに適用され、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 のどの実装にジャンプするかが決定されます。虚表 (vtable) の検索はありません。
  • しかし、trait オブジェクト dyn Add が現れる場合、コンパイラは vtable (関数ポインタを格納した構造体) を使用し、実行時に検索を行います。

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

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

  • 型推論失敗時のエラーメッセージがひどい⁠: HM の unification は失敗した場合、「2つの型が一致しない」ということしか分かりません。「なぜか」は分かりません——「Foo が必要だが Bar が見つかった」と表示しても、「ここで呼び出している関数は Foo を期待しているが、渡された x は Bar である、なぜなら3行前で Bar を代入したから」とは説明しません。→ 現代のコンパイラ (Rustc など) は推論中に「制約の起源」を記録し、推論失敗後に制約チェーンを遡ってメッセージを診断します。
  • 推論が決定不能⁠: HM の外側 (GADT、type family、rank-N 多相性など) に特性を追加すると、型推論が決定不能になる可能性があります——コンパイラが永遠に推論を続けることがあります。→ 制限を加える (Haskell は GADT と type family に型注釈を要求、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