Is it possible to get hold of free theorems as propositional equalities?
agda
Solution
No, the type theory on which Agda is build is not strong enough to prove this. This would require a feature called "internalized parametricity", see the work by Guilhem:
- Jean-Philippe Bernardy and Guilhem Moulin: A Computational Interpretation of Parametricity (2012)
- Guilhem Moulin: Pure Type Systems with an Internalized Parametricity Theorem (2013)
This would allow you for example to prove that all inhabitants of "(A : Set) → A → A" are equal to the (polymorphic) identity function. As far as I know, this has not been implemented in any language yet.
Problem
"Free theorems" in the sense of Wadler's paper "Theorems for Free!" are equations about certain values are derived based only on their type. So that, for example, ``` f : {A : Set} → List A → List A ``` automatically satisfies ``` f . map g = map g . f ``` Can I get my hands on an Agda term, then, of the following type: ``` (f : {A : Set} → List A → List A) {B C : Set} (g : B → C) (xs : List B) → f (map g xs) ≡ map g (f xs) ``` or if so/if not, can I do something more/less general? I'm aware of the existence of the Lightweight Free Theorems library but I don't think it does what I want (or if it does, I don't understand it well enough to do it). (An example use case is that I have a functor `F : Set → Set` and would like to prove that a polymorphic function `F A × F B → F (A × B)` is automatically a natural transformation.)