Parametricity
Types Are Documentation
Slides for a presentation, with specific reference to the morality of fast & loose reasoning[1^] and obtaining theorems for free[2^].
The goal of this presentation is to demonstrate the efficiency and robustness of reasoning about and comprehending source code using types. Some type system implementations include properties that diminish the overall reliability and this point is a primary one that is addressed directly.
-
[^] Danielsson, N. A., Hughes, J., Jansson, P., & Gibbons, J. (2006, January). Fast and loose reasoning is morally correct. In ACM SIGPLAN Notices (Vol. 41, No. 1, pp. 206-217). ACM.
-
[^] Wadler, P. (1989, November). Theorems for free!. In Proceedings of the fourth international conference on Functional programming languages and computer architecture (pp. 347-359). ACM.