Parametricity, Types are Documentation
This talk will build on the work of Philip Wadler (1) and Danielsson et al (2) to demonstrate using types to document source code behaviour and to assist in reasoning about code. Specifically, the concept of parametricity is used to tacitly eliminate possibilities in code behaviour leaving only a few, sometimes even one, remaining potential candidates.
- Theorems for free!, Wadler, Philip, Proceedings of the fourth international conference on Functional programming languages and computer architecture,
pp 347 – 359, 1989, ACM
- Fast and loose reasoning is morally correct, Danielsson, Nils Anders and Hughes, John and Jansson, Patrik and Gibbons, Jeremy, ACM SIGPLAN Notices, vol 41, num 1, pp 206 – 217, 2006, ACM