型システム

型システム

執筆済 コンピュータ言語型

プログラムの各部分に型を割り当て、整合性を検査する体系。

Pierce の定義では、型システムとは プログラムの各部分をその値の種類で分類することで、 特定の種類の実行時エラーが起きないことを証明する 軽量な形式手法。

何を保証するのか#

型が付く⟹ある種の誤りは起きない

保証されるのは「型に関する誤り」だけ。 配列の範囲外、0 除算、無限ループは 通常の型システムでは防げない。

健全性 (soundness) = 型が付いたプログラムは 「詰まらない」（progress + preservation）。

軸#

軸 対比
静的 / 動的 コンパイル時に検査するか、実行時か
強 / 弱 暗黙の型変換をどれだけ許すか
明示 / 推論 型を書くか、推論させるか
公称 / 構造 名前で同一性を決めるか、形で決めるか

TypeScript は静的・構造的、 Java は静的・公称、 Python は動的（型注釈は実行時に検査されない）。

型推論#

Hindley-Milner 型推論は、 型注釈なしで最も一般的な型（主要型）を求める。

let id x = x
  ↓ 推論
id : ∀a. a → a

単一化 (unification) で型変数を解いていく。 OCaml、Haskell、Rust（局所的に）、 TypeScript（部分的に）が採用している。

表現力とのトレードオフ#

型システムを強くすると、 正しいのに型が付かないプログラムが増える。

健全+完全+決定可能は同時に満たせない

Rice の定理により、 プログラムの意味的な性質は一般に決定不能。 型システムは安全側に倒す（保守的に拒否する）ことで 決定可能性を保っている。

TypeScript のように、 利便性のために意図的に健全性を捨てる設計もある。

参考文献#

  • Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002.
  • Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences 17(3), 1978. https://doi.org/10.1016/0022-0000(78)90014-4
  • Luca Cardelli, Peter Wegner. On Understanding Types, Data Abstraction, and Polymorphism. ACM Computing Surveys 17(4), 1985. https://doi.org/10.1145/6041.6042