Swiftプログラミングと論理 〜そして帰ってきた圏論〜 by 稲見 泰宏

「プログラミング」と「論理」の世界には直接的な対応関係があり、
私たちが普段書いているSwiftにおいても例外ではありません。

例えば、論理の世界における命題「AかつB」はタプル型 (A, B) 、
「AならばB」は関数型 A -> B を使って書くことができます。
これらの型（命題）を組み合わせ、適用していくことで、
あたかも論理式（や数式）を証明するかのように、アプリのプログラムが完成します。

この、「型 ⇔ 命題」、「プログラム ⇔ 証明」に対応することを「Curry-Howard同型対応」と言います。
この背景を知るには、「直感主義論理」と「型付きラムダ計算」の両方を学ぶことが重要です。

そこで、この発表では、理論的基盤となる「古典命題論理・述語論理」「ラムダ計算」の基本をおさらいした後、
「直感主義命題論理」「Curry-Howard同型対応」について、実際にSwift言語を使ってお話しします。
また、Swiftがサポートする「多相型」、「Protocol (Witness)」、「Opaque Result Type」等にも触れ、
圏論の図式を使った、より手軽で簡単な解説も予定しています。

なお、今回の発表は、昨年のiOSDCの発表の続編になります。
事前の予習として、下記のスライドをご参考ください。

代数的データ型 https://speakerdeck.com/inamiy/algebraic-data-type-in-swift
圏論とSwiftへの応用 https://speakerdeck.com/inamiy/iosdc-japan-1