Playlist "BOB Konferenz 2025"
Abstraction and program design, or the power of parametricity
In this talk I want to revisit the parametricity theorem: from parametrically polymorphic types, i.e., types that contain type variables that can be arbitrarily instantiated, we can directly infer certain properties of the underlying functions, without ever having to look at their implementation.
A simple example in Haskell is the type forall a. a -> a, which (apart from looping or crashing functions) can only be inhabited by the identity function.
This may sound like a curiosity, but I will argue that it is in fact an invaluable tool in program design and day-to-day reasoning about programs, and explain how to build an intuition that allows you to do so without the need for deep or complicated theory. We will look at several interesting examples and hopefully make a few perhaps surprising discoveries along the way.
I will also try to explain how in the case of parametricity, making types more abstract can really help in making functions easier to understand, whereas it often feels like the opposite may be true. To this end, I will try to contrast abstraction in the context of parametricity with other kinds of type-level abstraction common in Haskell, in particular abstraction via type classes, and show how they are different.
Licensed to the public under https://creativecommons.org/licenses/by/3.0/de