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

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

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
iosdc-japan-2018 sponsors iosdc-japan-2018 potential-sponsors 開催後請求
ブースWL 要支払確認 要モノクロロゴ
仮採択 採択しない Rookie
仮採択 採択済 保留 情熱加点 採択しない 前夜祭 目玉 ルーキーズLT参加
Order#確認 アンケートメール不要