博士

ロボ子、今日のITニュースはすごいぞ！TypeScriptで論理学ができるようになったらしいのじゃ！

ロボ子

TypeScriptで論理学ですか？一体どういうことでしょう？

博士

TypeScriptの型システムを使って、論理的な推論を表現できるようになったらしいのじゃ。例えば、Falseは再帰型としてエンコードされるみたいじゃ。`{ false: { false: { false: ... }}}`みたいな感じじゃな。

ロボ子

なるほど、型定義で無限に続くFalseを表現するんですね。Trueはどのように表現するんですか？

博士

Trueは、文字列 "I" を持つシングルトン型 "I" としてエンコードされるらしいぞ。シンプルじゃな。

ロボ子

連言（AND）や選言（OR）も表現できるんですか？

博士

もちろんじゃ！AとBの連言は、Aを持つ "left" プロパティとBを持つ "right" プロパティを含むオブジェクトとしてエンコードされるみたいじゃ。選言は、Aを持つ "left" フィールドを含むオブジェクトと、Bを持つ "right" フィールドを含むオブジェクトの和型としてエンコードされるぞ。

ロボ子

含意（ならば）はどうでしょう？

博士

含意は単なる関数としてエンコードされるらしいぞ。関数で表現できるのは面白いな。

ロボ子

否定（NOT）も表現できるんですね。非存在型への含意としてエンコードされるとのことですが、少し難しいですね。

博士

そうじゃな。でも、TypeScriptの型システムで論理学の基本的な規則が証明できるのはすごいことじゃ！例えば、含意導入(ImpI)は`(b : B) => (_: A) => b`で、含意除去(ImpE)は`(a : A) => (a_imp_b : Imp) => a_imp_b(a)`で表現できるぞ。

ロボ子

連言導入(ConjI)は`(a : A) => (b : B) => ({ left: a, right: b })`ですね。型定義を見るだけで、論理演算の意味が理解できるのが面白いです。

博士

じゃろじゃろ？選言除去(DisjE)はちょっと複雑で、`(a_or_b : Dis) => (a_imp_c : Imp) => (b_imp_c : Imp) => "left" in a_or_b ? a_imp_c(a_or_b.left) : b_imp_c(a_or_b.right)`となるみたいじゃ。

ロボ子

条件分岐を使って、leftかrightかを判定しているんですね。

博士

そうそう！トートロジーの例として、`(A -> B -> C) -> (A -> B) -> A -> C`や`A -> A -> A`が挙げられているぞ。これもTypeScriptで表現できるなんて、すごい時代になったものじゃ。

ロボ子

対偶の法則`(A -> B) -> (~B -> ~A)`も使えるんですね。型レベルで論理的な推論ができるようになると、プログラムの安全性を高めるのに役立ちそうですね。

博士

その通り！型システムは、プログラムのバグを防ぐための強力なツールになるのじゃ。今回の発見は、TypeScriptの可能性をさらに広げるものじゃな。

ロボ子

TypeScriptでここまでできるとは驚きです。私ももっと型について勉強しないといけませんね。

博士

ロボ子ならすぐにマスターできるぞ！…ところでロボ子、TypeScriptで「真実はいつも一つ！」を表現するとどうなると思う？

ロボ子

えっと… True型が一つだけ、ということでしょうか？

博士

ぶっぶー！残念！答えは「型エラー」なのじゃ！