もしTypeScriptの型システムが不完全だとしたら？
日本の開発者の皆さん、こんにちは！海外の個人開発メディア編集長 shiroです。
普段私たちが頼りにしているTypeScriptやRustなどの型システム。厳格なおかげでバグが減ると信じられていますが、もしその「型システム」自体に、どうやっても解決できない数学的な限界があるとしたら？
今回、Hacker Newsで話題になったのは、この根源的な問いにLean 4という形式証明言語で答えを出したという衝撃的なニュースです。
型システム、構造 vs. 名前の終わらない戦い
開発者なら一度は耳にしたことがあるかもしれませんが、「構造的型付け（Structural Typing）」と「名前的型付け（Nominal Typing）」の論争は、長い間続いてきました。
- 構造的型付け (TypeScript, Goなど)：中身（プロパティやメソッド）が一致していれば、型が同じと見なす考え方。柔軟性が高い。
- 名前的型付け (Java, Rustなど)：型を宣言した名前（class名やtrait名）が一致しないと、別物と見なす考え方。厳格で安全性が高い。
どちらが優れているか、というのは言語設計者にとって永遠のテーマでした。
【本題】固定軸型システムは必ず失敗する
今回、この論争に決着をつけようと試みた論文の核心は、次の通りです。
「構造、継承、階層」など、何らかの固定された軸（Fixed Axes）に基づいて設計された型システムは、必ずその要件を完全に捉えきれないドメイン（領域）が存在する。
これは、特定の言語（Python, TS, Java, Rust）の実装ミスではなく、数学的な不可能性（Impossibility Result）として証明されました。
具体的にどういうこと？
開発者が型システムを設計する際、便宜上「構造」や「継承関係」という軸を使って整理します。しかし、現実世界には、その軸では分類できない、新しい種類の関係性を持つデータ領域が必ず現れるということです。
- 例えば、あるドメインでは「構造」が重要なのに、別のドメインでは「いつ、誰によって定義されたか（名前）」が重要になる場合、固定された一つの軸では両方を完全に満たす型付けはできません。
- この証明は、実際の言語仕様から抽出された公理に基づいており、机上の空論ではない点が重要です。
私たちの設計への影響
この結果が、私たち個人の開発や副業にどう影響するのでしょうか？
それは、「型システムは万能ではない」という謙虚さを持つことです。
- 型に頼りすぎない設計：型チェックが通ったからといって安心せず、実行時チェックやバリデーションを疎かにしない姿勢が求められます。
- ドメインに合わせた柔軟性：一つの言語（例えばTS）の中でも、構造的型付けと名前的型付けのエッセンスを使い分ける（例: Brand Typeを導入する）など、ドメインの要求に応じて柔軟な設計が必要です。
型システムは強力なツールですが、完全無欠ではありません。この数学的な限界を知ることで、より強靭で現実的なソフトウェア設計を目指しましょう！
コメント