Is it possible to get hold of free theorems as propositional equalities?

Question

"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.)

Answer 1

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.

Answer 2

Chantal Keller and Marc Lasson developped a tactic for Coq generating the parametricity relation corresponding to a (closed) type and proving that this type's inhabitants satisfy the generated relation. You can find more details about this work on Keller's website.

Now in Agda's case, it is in theory possible to do the same sort of work by implementing the tactic in pure Agda using a technique called reflection.