LambdaConf's video: Emily Pillmore Alexander Konovalov- Isomorphic Reasoning: Counting with Types Part 1- C 2019

This is a 3 video talk; Please see: Part 2: https://youtu.be/UScWv37aJhY Part 3: https://youtu.be/kKZTd7D33KY *We are aware of the sound issue for parts 2 and 3, but have chosen to leave the video as-is for you to follow along as desired. Slides for this talk: https://github.com/cohomolo-gy/Isomorphic-Reasoning/blob/master/main.pdf. Blog post by Alex that explains much of his portion: https://alexknvl.com/posts/counting-type-inhabitants.html FP developers know that ∀ a. a → a has only one inhabitant, but how? Using the language of category theory (Yoneda, representable and Naperian functors, etc.), we can show that there is a secret type-level arithmetic embedded in languages that support parametric polymorphism, allowing us to reason about types and even manipulate them as you would basic arithmetic. It is a common theme among developers beginning to study parametrically polymorphic type systems in functional programming that they come across blog posts or tutorials that make analogies between types and arithmetic in order to express how easy it is to reason about type signatures. Often, one will find algebraic data types (ADTs) expressed in terms of polynomials, coproducts in terms of addition, products in terms of multiplication, etc., applying seemingly magical arithmetic using this language to simplify and prove properties about the types. As often, these transformations are poorly motivated or cryptically taken to be axiomatic and soon forgotten as a curiosity of the type system. But there is more to these transformations than meets the eye. In this talk, we will explain how one can reason about type signatures arithmetically and count the number of inhabitants of polymorphic types using a simple arithmetic derived from the language of category theory. From category theory, we will use the (Double, co-) Yoneda Lemma, representable, Naperian, and Container Functors, products, coproducts, initial and terminal objects, and nominal results surrounding these as points of study to build a theory, which we will call “Isomorphic Reasoning”– because that is really what it all comes down to: exploiting isomorphisms to achieve simple and elegant transformations that we are all familiar with. We will also discuss the fundamental topic of observational equality (identity of indiscernibles) and its relation to isomorphisms on types, and work our way towards parametricity and free theorems. We will discuss System F, its type-level language and its encoding using de Brujin indices. Taking a short break from the theory, we will implement this type algebra in Haskell / Scala / Idris, together with a minimal parser & printer. By lifting our search from individual types to sequences of isomorphisms ending with types, we will be able to explicitly enumerate all of its inhabitants. We will talk about further improvements to the tool that we could add: support for functor fixpoints, double-negation translation, and System Fω. Requirements While we will cover a lot of advanced topics, we will attempt to explain things in the simplest possible terms. Basic knowledge of functional concepts will be assumed. Bring pen & paper as well as your laptop.