型の住人を数える

いっぱしの関数型プログラマなら ∀ a. a → a は 1つの住人しか持たないことを知っていますが、それはどうしてでしょうか? 本セッションでは、型代数、パラメトリック性、Yoneda / Coyoneda の補題、表現可能な関手、コンテナ関手を駆使して System F の項を厳密に数える方法を解説します。これにより、Theorems for Free 同様の新しい強力な推論ツールを手に入れることができます。

トークの長さ

90分

発表言語

英語

聴衆の対象

中級者: 分野の基礎は分かるが、細かい所は不安

こんな人におすすめ

型理論、Yoneda / Coyoneda の補題、表現可能な関手、Theorems for free などをしっかりと理解したい人

発表者

Alexander Konovalov (Compellon, Analytics Engineer)

• WWW2017 で論文を発表しました https://www.slideshare.net/AlexanderKonovalov13/learning-event-extractors-from-knowledge-base-revisions
• Lambdaconf 2018 でも scalaz summit の一環としてインフォーマルな発表を行いました https://alexknvl.com/docs/scalaz_summit_presentation.pdf

貢献

• Scalaz コントリビューターであり、チームメンバーです