Triggered by Paul Levy’s recent post on the TYPES mailing list (and my reply) I reviewed the concept of parametricity for System F. First I talked about impredicative encodings: In System F, any type with a positive occurence of a type variable gives rise to a functor, i.e. there is a term , and we can construct a weakly initial algebra with the structure map by
The fold operation is simply since the type of fold motivated this encoding. It is easy to see that is weakly initial because . This also dualizes to weakly terminal coalgebras where can be encoded impredicatively as and .
To show that these encodings are strong, we need the additional assumption of parametricity. For any type we give a relational interpretation, which assigns to a relation — I am simplifying here since we have to interpret types with any number of free variables. This is given by
Parametricity means that every closed is related to itself .
An important lemma is the map-property which relates the relational and functorial properties of types. Any function gives rise to a relation . Now given a type with a positive occurence of we can show that and agree.
As Phil Wadler noticed we can derive initiality from parametricity for . Interestingly, we have to use parametricity twice! Parametricity for fold implies that fold is natural, i.e. given two T-algebras and a T-algebra morphism , s.t. , this entails that . Assuming parametricity we obtain that for any , i.e.
Initiality means that for any such that it holds that . This is indeed a consequence of the naturality of fold if we instantiate , the precondition follows from weak initiality. However, it remains to show that . Interestingly, this also follows from naturality using . From here, follows by unfolding fold and applying -equality.
Paul asked whether is isomorphic to , where both T,U have positive occurences of a type variable X. Indeed, I have now checked that this follows by adapting the reasoning above and using the map property of U as well.