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!”.