Counting type inhabitants

FP developers know that ∀ a. a → a has only one inhabitant, but how? In this talk you will learn how to rigorously count System F terms using type algebra, parametricity, Yoneda & Coyoneda lemmas, representable & container functors. We will discover that this gives us a new and powerful reasoning tool akin to Theorems for Free.

Session length

90 minutes

Language of the presentation

English

Target audience

Intermediate: Requires a basic knowledge of the area

Who is your session intended to

People who want to get a deeper understanding of type theory, Yoneda / Coyoneda lemmas, representable functors, theorems for free.

Speaker

Alexander Konovalov (Compellon, Analytics Engineer)

• I have presented an academic paper at WWW2017, https://www.slideshare.net/AlexanderKonovalov13/learning-event-extractors-from-knowledge-base-revisions and presented https://alexknvl.com/docs/scalaz_summit_presentation.pdf at Lambdaconf 2018 but in an informal setting during scalaz summit and without much preparation.

Contributes

• I am a contributor and a team member of Scalaz.