Theorems for Free
This SkillsCast is currently only available to registered attendees of Haskell eXchange 2020
It will be freely available to all Skills Matter members once the Haskell eXchange 2020 early-access window expires on December 04, 2020.
We can extract a lot of information from type signatures. But how does it work? In this talk Lars Hupel will revisit Philip Wadler's influential (and very cool) paper "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 influential paper "Theorems for free!".
YOU MAY ALSO LIKE:
Thank you to our sponsors and partners
Gold
Silver
Theorems for Free
Lars Hupel
Lars Hupel is a consultant in Munich, Germany. They 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, they are active in the open source community, particularly in Scala. They also enjoy programming in and talking about Haskell, TypeScript, Prolog, and Rust. Previously, they were a PhD student at TU München in the field of logic and verification.