iOSDC Japan 2019 のセッション動画です。
2019/09/06(60分)
スピーカー: 稲見 泰宏 ( @inamiy )
タイトル: Swiftプログラミングと論理 〜そして帰ってきた圏論〜
「プログラミング」と「論理」の世界には直接的な対応関係があり、
私たちが普段書いているSwiftにおいても例外ではありません。
例えば、論理の世界における命題「AかつB」はタプル型 `(A, B)` 、
「AならばB」は関数型 `A -＞ B` を使って書くことができます。
これらの型（命題）を組み合わせ、適用していくことで、
あたかも論理式（や数式）を証明するかのように、アプリのプログラムが完成します。
この、「型 ⇔ 命題」、「プログラム ⇔ 証明」に対応することを「Curry-Howard同型対応」と言います。
この背景を知るには、「直感主義論理」と「型付きラムダ計算」の両方を学ぶことが重要です。
そこで、この発表では、理論的基盤となる「古典命題論理・述語論理」「ラムダ計算」の基本をおさらいした後、
「直感主義命題論理」「Curry-Howard同型対応」について、実際にSwift言語を使ってお話しします。
また、Swiftがサポートする「多相型」、「Protocol (Witness)」、「Opaque Result Typ…
https://fortee.jp/iosdc-japan-2019/proposal/9529444c-a849-47cd-94a7-bf2b694320aa
