Since parametrically-polymorphic functions should handle values of different types in the same way, their ability to use information about incoming values is significantly limited. These limitations can be used to prove some useful properties of polymorphic functions. Philip Wadler proposed a method for generation of such theorems (known as "free theorems") for any polymorphic type. In the talk, we will consider this method, and also will look at certain examples of free theorems and their possible applications.
Philip Wadler. Theorems for free!
Presenter: Dmitri Rozplokhas
Date: December 4, 2017
Venue: room 3248, Faculty of Mathematics and Mechanics, Saint Petersburg State University, Stary Peterhof, Universitetski pr., 28