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

iOSDC Japan 2019
採択
2019/09/06 16:00〜
Track D
技術パッション共有トーク(60分)

Swiftプログラミングと論理 〜そして帰ってきた圏論〜

inamiy 稲見 泰宏 inamiy

「プログラミング」と「論理」の世界には直接的な対応関係があり、
私たちが普段書いている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