日本語

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)
Contributes
  • I am a contributor and a team member of Scalaz.

voted / votable

Candidate sessions