Abstract
Free theorems are a popular tool in reasoning about parametrically polymorphic code. They are also of instructive use in teaching. Their derivation, though, can be tedious, as it involves unfolding a lot of definitions, then hoping to be able to simplify the resulting logical formula to something nice and short. Even in a mechanised generator it is not easy to get the right heuristics in place to achieve good outcomes. Dinaturality is a categorical abstraction that captures many instances of free theorems. Arguably, its origins are more conceptually involved to explain, though, and generating useful statements from it also has its pitfalls. We present a simple approach for obtaining dinaturality-related free theorems from the standard formulation of relational parametricity in a rather direct way. It is conceptually appealing and easy to control and implement, as the provided Haskell code shows.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Something we will not mention again and again is that \( g \) is also itself non-\(\bot \). Disregarding types that contain only \(\bot \), this follows from totality of \( g \) anyway.
- 2.
Additional code for parsing input strings into type expressions and pretty-printing generated theorem expressions back into pleasingly looking strings is of comparable complexity between the different generators.
References
http://hackage.haskell.org/package/free-theorems. Accessed Sept 2019
http://free-theorems.nomeata.de. Accessed Sept 2019
http://hackage.haskell.org/package/lambdabot-haskell-plugins. Accessed Sept 2019
http://hackage.haskell.org/package/ft-generator. Accessed Sept 2019
Bainbridge, E., Freyd, P., Scedrov, A., Scott, P.: Functorial polymorphism. Theor. Comput. Sci. 70(1), 35–64 (1990)
Berger, U., Schwichtenberg, H.: An inverse of the evaluation functional for typed lambda-calculus. In: Logic in Computer Science, Proceedings, pp. 203–211. IEEE Press (1991)
Gill, A., Launchbury, J., Peyton Jones, S.: A short cut to deforestation. In: Functional Programming Languages and Computer Architecture, Proceedings, pp. 223–232. ACM Press (1993)
Hackett, J., Hutton, G.: Programs for cheap! In: Logic in Computer Science, Proceedings, pp. 115–126. IEEE Press (2015)
Johann, P., Voigtländer, J.: Free theorems in the presence of seq. In: Principles of Programming Languages, Proceedings, pp. 99–110. ACM Press (2004)
Mehner, S., Seidel, D., Straßburger, L., Voigtländer, J.: Parametricity and proving free theorems for functional-logic languages. In: Principles and Practice of Declarative Programming, Proceedings, pp. 19–30. ACM Press (2014)
Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Programming Language Design and Implementation, Proceedings, pp. 199–208. ACM Press (1988)
Reynolds, J.: Types, abstraction and parametric polymorphism. In: Information Processing, Proceedings, pp. 513–523. Elsevier (1983)
Stenger, F., Voigtländer, J.: Parametricity for Haskell with imprecise error semantics. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol. 5608, pp. 294–308. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02273-9_22
Wadler, P.: Theorems for free! In: Functional Programming Languages and Computer Architecture, Proceedings, pp. 347–359. ACM Press (1989)
Acknowledgements
Many of the ideas here, most notably the conjuring lemma (including that name), but also the criterion proposed in Sect. 3.5, originated during past collaboration with Stefan Mehner.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
A Implementation
A Implementation
See Sect. 4 for some explanation of the implementation.
Module \(\mathsf {Generate}\), generation and simplification of free theorems
Module \(\mathsf {Syntax}\), datatypes for types and different forms of (higher-order abstract syntax) terms, and eta-reduction
Module \(\mathsf {Main}\), putting the generator together with input and output
An example session
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Voigtländer, J. (2020). Free Theorems Simply, via Dinaturality. In: Hofstedt, P., Abreu, S., John, U., Kuchen, H., Seipel, D. (eds) Declarative Programming and Knowledge Management. INAP WLP WFLP 2019 2019 2019. Lecture Notes in Computer Science(), vol 12057. Springer, Cham. https://doi.org/10.1007/978-3-030-46714-2_16
Download citation
DOI: https://doi.org/10.1007/978-3-030-46714-2_16
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-46713-5
Online ISBN: 978-3-030-46714-2
eBook Packages: Computer ScienceComputer Science (R0)