型理論の基礎（ラムダ計算と型付け）

なぜラムダ計算から始めるのか

現代の型システムは、見た目こそ言語ごとに違っても、その正しさの根拠は1つの数学的モデルに行き着きます。それがラムダ計算（lambda calculus）です。1930年代にアロンゾ・チャーチが計算を定義するために導入したもので、チューリングマシンと同じ計算能力（チューリング完全）を持ちながら、構成要素は驚くほど少ない。型システムが「この値で何ができるか」をなぜ厳密に保証できるのかは、このモデルを通すと一気に見通せます。

型なしラムダ計算：3要素ですべてを表す

型なしラムダ計算の項（term）は、たった3種類の構文だけで作られます。

• 変数: x、y など
• 抽象（関数の定義）: λx. M（x を受け取り本体 M を返す関数）
• 適用（関数呼び出し）: M N（M に N を渡す）

計算規則も本質的に1つだけ。関数に引数を渡したとき、本体の中の仮引数を実引数で置き換える操作で、これをβ簡約（beta reduction）と呼びます。

(λx. x x) (λy. y)   →   (λy. y) (λy. y)   →   (λy. y)

(λx. x x) に (λy. y) を渡すと、本体 x x の x がすべて引数に置き換わる、というだけです。条件分岐も自然数も再帰も、すべてこの枠組みの中で表現できます（再帰の不動点も、ラムダ計算ではYコンビネータという項として書けます）。

型を導入する動機：止まらない計算がある

型なしには、いくら簡約しても終わらない項が存在します。代表が次の項です。

Ω = (λx. x x) (λx. x x)

Ω をβ簡約すると、まったく同じ Ω に戻ります。永遠にループするわけです。型なしラムダ計算がチューリング完全である以上、停止性を一般には判定できません。ここに型を導入する強い動機があります。「自分自身に自分を適用する」x x のような危うい操作を、型のレベルで初めから禁止できれば、計算の振る舞いを保証できます。

単純型付きラムダ計算：型は安全性の証明

単純型付きラムダ計算（STLC）は、項に型を付け、型が整合する項だけを「正しい」と認めます。型は次の2種類で構成されます。

• 基底型: Bool、Nat など
• 関数型: A -> B（A を受け取り B を返す関数の型）

型付けは型付け規則で定義され、たとえば適用 M N は「M が A -> B 型で N が A 型なら、M N は B 型」というように、引数の型が一致して初めて型が付きます。先ほどの x x は、x の型が A -> B と A の両方であることを同時に要求し、これは有限の型では満たせません。こうして Ω は型付け不能となり、システムから排除されます。

STLCの中心的な定理が型保存（preservation）と進行（progress）です。型保存は「型の付いた項を簡約しても型は変わらない」、進行は「型の付いた項は値であるか、さらに簡約できるかのどちらか（途中で詰まらない）」を意味します。両者を合わせると「正しく型付いたプログラムは実行時に型エラーで詰まらない」が証明されます。これが多くの言語が掲げる型安全性の数学的な核です。

Curry-Howard対応：型は命題、プログラムは証明

型理論が単なる検査ツールを超えて「論理学そのもの」とみなせる理由が、Curry-Howard対応（カリー・ハワード同型対応）です。型システムと論理体系のあいだに、次の精密な対応があります。

つまり「型 A -> B の関数を書く」ことは「A ならば B を証明する」ことと同じです。プログラムが型検査を通ることは、対応する命題の証明が完成したことに相当します。CoqやAgda、Leanといった証明支援系は、まさにこの対応を使って数学の定理をプログラムとして証明します。型を「制約」ではなく「証明すべき仕様」として捉え直すと、設計の解像度が上がります。

System F：型を引数化する

STLCでは「恒等関数」λx. x を Bool 用と Nat 用で別々に書く必要があります。これを1つにまとめるのがSystem F（多相ラムダ計算、ジラールとレイノルズが独立に発見）です。System Fは型抽象と型適用を導入し、型そのものを引数として渡せるようにします。

id = Λα. λx:α. x        -- 型 α を受け取り、α 型の値をそのまま返す
id [Nat] 5              -- 型 Nat を渡してから 5 を渡す

Λα（大文字ラムダ）が型を束縛する抽象で、id の型は「すべての型 α について α -> α」となります。これはジェネリクス（総称型）の数理的な正体そのものです。実用言語の <T> という記法は、System Fの全称量化された型 ∀α. α -> α を表面に出したものだと理解できます。

ラムダキューブ：型システムの地図

STLCからの拡張は、3つの軸で整理できます。これをラムダキューブ（バレンドレヒトの立方体）と呼びます。

3軸すべてを備えた頂点がCalculus of Constructionsで、証明支援系Coqの理論的土台です。とりわけ「型が項に依存する」依存型は強力で、たとえば「長さ n の配列」という型を書けるため、配列アクセスの範囲外参照を型レベルで排除できます。型と値の境界が消え、仕様と実装が同じ言語で書けるようになります。

まとめ：型注釈の裏にある理論

型注釈は単なる飾りではなく、その背後には「正しく型付いたプログラムは詰まらない」という証明が控えています。ラムダ計算が計算の最小モデルを与え、単純型がそこに安全性と停止性を持ち込み、Curry-Howard対応が型と論理を結び、System Fが多相という抽象を、依存型が仕様の表現を与える——この一本の線が、現代の型システムを貫いています。値を変更しないイミュータビリティや、副作用を持たない純粋関数が型理論と相性が良いのも、これらがラムダ計算という同じ源流から流れ出ているからです。型を「証明すべき仕様」として読み直せたとき、日々書く型注釈の意味は大きく変わるはずです。