こんにちは、@inamiy です。
今年も恒例、iOSの夏祭りイベントである iOSDC Japan 2019 (2019年9月5日〜7日) に参加・登壇してきましたので、iwillblogします。
4年目となる今年は、開催期間が 3.5 → 2.5日間に短縮、かつ60分の長い登壇枠が追加されたこともあり、 昨年よりもCfPの当選者数が減って激戦になる ことが予想されました。
今回、私は「Swiftと論理（カリー・ハワード対応）」をテーマに話そうと前々から決めていましたが、 このショボいタイトルでは落選する と判断し、急遽 サブタイトルを加えて話を盛る ことに。
昨年の「圏論」の話 を絡めた、総合的な内容に（無理やり）拡張しつつ、混み合いそうな「レギュラートーク枠」を回避して「技術パッション共有トーク」で応募するなど、必死 考えられる限りの最善の選択肢を取りました。
結果的に無事当選を果たすことができて、とても嬉しかったのですが、やはりタイトルの盛りすぎで、前日ギリギリまでスライド作りに苦戦したことをここに懺悔いたします。
当日の発表内容
当日は、以下の内容で発表させていただきました。
- プロポーザル： Swiftプログラミングと論理 〜そして帰ってきた圏論〜 by 稲見 泰宏 | トーク | iOSDC Japan 2019 #iosdc - fortee.jp
- スライド： https://speakerdeck.com/inamiy/swift-and-logic-and-category-theory
- 動画： (TBD)
- サンプルコード： https://github.com/inamiy/SwiftAndLogic
この中で、個人的ハイライトを幾つか上げると、まず最もシンプルかつクレイジーな実装として、次の **「矛盾律」**と呼ばれる absurd 関数があります。
/// `⊥ ===> A`
func absurd<A>(_ x: Never) -> A {
// Swift 5.1 では何も書かなくて良い ¯\_(ツ)_/¯
}
なんと、 スコープの中で何も実装しなくても、Swift 5.1 ではコンパイルが通ります。
これにはかなり驚かれた方も多いのではないでしょうか？
（Swift 5.0以下の場合は、 switch x {} 空パターンマッチを実装すればOK）
また、古典論理と [直観主義論理] (https://ja.wikipedia.org/wiki/%E7%9B%B4%E8%A6%B3%E4%B8%BB%E7%BE%A9%E8%AB%96%E7%90%86) の違いの簡単な説明として、 「Boolの2択で閉じた世界」と「無限に広がる型の世界」 で解釈が異なる ことも見てきました。
Boolの世界では、 true の否定は false （= true以外の値）ですが、型の世界では Int の否定は 「Int以外の(無限に存在する)型」という解釈はできず（無限は実在しないため）、Int -> Never の関数型として表されます。
（数学的には、ブール代数の「補元」が成り立たず、ハイティング代数の「擬補元」として解釈されます）
そして、 グリベンコの定理 (Glivenko's theorem) と呼ばれる 二重否定を加える翻訳 が、古典論理を直観主義論理 (≒ Swiftの世界) へと誘う（CPSで埋め込む）ことを見ていきました。
これは例えば、排中律であれば、「何もないところ（空引数）から Either<A, Not<A>> を作る」という 無理ゲー を、「Not<Either<A, Not<A>>> から Never を作る」という 実装可能な型パズル に変換します。
詳しくは、上述のスライドやサンプルコードをご参考の上、ぜひ Swift Playground等で遊んでみて下さい。
ちなみに当日は、あまり圏論について解説できませんでしたが、圏論の図式を使うと、一見非対称な論理学のANDとORの推論規則が、 圏論の双対性によって対称的に説明できる ほか、随伴・冪対象・ デカルト閉圏と論理の関係 や、 トポスを使った意味論 などの話につながっていきます。
このように、論理に加えて圏論を学ぶことで、 論理 ⇔ プログラミング ⇔ 圏論 のトライフォースが完成します。
Swiftに限らず、型を学ぶプログラマーの皆様にとっての参考になれば幸いです。
最後に
このように、日々のiOS開発現場で１㍉も役に立たない話でも、発表できたり、交流できるのがiOSDCの魅力だと常々感じています。
今年はついに参加者が1000人超えを達成ということで、来年の開催がますます楽しみです。
スタッフの皆様、スピーカー・参加者の皆様、今年もおつかれさまでした ＆ どうもありがとうございました！
来年までに、頂いた電子ブロックでHomePodを作ろうと思います！！
まさかのスタッフ推薦で学研電子ブロックをいただきました！
— Yasuhiro Inami (@inamiy) September 7, 2019
ありがとうございます！
来年はこれとSwiftを絡めて発表がんばります💪 #iosdc pic.twitter.com/cv4IMfXASf