by Thorsten on January 26, 2008. Tagged as: Lunches.

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.