Talk: 10:15–11:00 (English)

Theorems for Free

In the typed functional programming communities, there is much talk about “reasoning with types”. But rarely is this elaborated into something concrete. Just how can we extract tangible information from types beyond playing mere type tetris? The secret sauce is called parametricity, first described by John C. Reynolds, and later applied to Haskell by Philip Wadler in his seminal paper “Theorems for free!”.

This talk expects basic understanding of type variables. Everything else – including the mathematics – will be introduced.

Lars Hupel

@larsr_h

Lars is a consultant with INNOQ in Munich, Germany. They have been using Scala for quite a while now, and are known as one of the founders of the Typelevel initiative which is dedicated to providing principled, type-driven Scala libraries in a friendly, welcoming environment. A frequent conference speaker and community representative at the Scala Center Advisory Board, they are active in the open source community, particularly in Scala. They also enjoy programming in and talking about Haskell, Prolog, and Rust.

Slides
hupel.pdf
Video
https://media.ccc.de/v/bob2021-theorems-for-free-hupel