博士

やあ、ロボ子。今日のITニュースは型システムについてじゃ。

ロボ子

博士、こんにちは。型システムですか、興味深いですね。Leanという言語が豊富な型システムを持っているそうですね。

博士

そうじゃ、Leanは関数型、積型、和型、商型の4種類をサポートしておる。型は、データの使い方を定めるルールみたいなものじゃな。

ロボ子

なるほど。型には階層があるんですね。宇宙（Universes）、型（Types）、項（Terms）という構造になっていると。

博士

その通り！型は項を分類し、項は型を持つ。そして、ラッセルのパラドックスを避けるために、宇宙は無限の階層になっておるのじゃ。

ロボ子

`#check`コマンドで式の型を照会できるのは便利ですね。型が期待通りか確認できる。

博士

そうじゃ、型理論では`:`を使って項が特定の型を持つことを示すのじゃ。集合論の`∈`（メンバーシップ）と似ておるな。

ロボ子

宇宙には`Type`と`Prop`があるんですね。`Type`は数学的オブジェクト、`Prop`は命題を含むと。

博士

その通り！そして、カリー・ハワード対応によって、命題は`Prop`の型であり、証明はその型の項となるのじゃ。

ロボ子

関数型（Pi型）は型間のマッピングを表すんですね。依存型と非依存型があるとのことですが。

博士

`Π (x : A), B x`は、戻り値の型`B x`が入力値`x`に依存する依存関数型じゃ。難しく聞こえるかもしれんが、要は引数によって返り値の型が変わるということじゃな。

ロボ子

積型は複数の値の組み合わせ、和型は代替案を表すと。商型は同等の値を表すんですね。

博士

その通り！そして、差分型じゃ。これは、ある型から別の型を「減算」することを表すのじゃ。

ロボ子

差分型ですか。Leanでは直接サポートされていないけれど、依存型と証明義務を使ってエンコードできるんですね。

博士

そうじゃ！例えば、非ゼロ数、空でないリスト、偶数などを表現できるのじゃ。

ロボ子

除算を安全にする例が分かりやすいですね。ゼロ除算の場合を削除できる。

博士

じゃろ？型システムは、単にデータの種類を区別するだけでなく、プログラムの安全性を高めるためにも使えるのじゃ。

ロボ子

関数型は高階関数、積型はデータ構造、和型はエラー処理、商型はモジュラー算術に応用できるんですね。型システム、奥が深いですね。

博士

そうじゃろう？型システムを理解すると、より安全で信頼性の高いプログラムを書けるようになるぞ。…ところでロボ子、型にはまらない私の魅力、どう思う？

ロボ子

博士、それは型システムとは関係ないと思いますが…。