What is relational parametricity?

Question

A complicated-sounding term with no good explanations from a simple google search... are there any more academically-oriented folk who could explain this one?

Answer 1

Both answers are mostly right. I would say that parametricity is a possible property of polymorphism. And polymorphism is parametric if polymorphic terms behave the same under all instantiations. To "behave the same" is a vague, intuitive term. Relational parametricity was introduced by John Reynolds as a mathematical formalization of this. It states that polymorphic terms preserve all relations, which intuitively forces it to behave the same:

Consider f: a list -> a list. If we have the relation a~1, b~2, c~3, ..., then we can lift it to lists and hav e.g. [a, d, b, c] ~ [1, 4, 2, 3]

Now, if f([a, d, b, c]) = [c, b, d, a] and f preserves relations, then f([1, 4, 2, 3]) = [3, 2, 4, 1]. In other words, if f reverses list of strings, it also reverses lists of numbers.

So relationally parametric polymorphic functions cannot "inspect the type argument", in that they cannot alter their behaviour based on the type.

Answer 2

Relational parametricity seems to be the property that a function abstracted over types (like a generic in Java) can have. If it has this property, it means it never inspects its type argument or deconstructs it / uses it in some special way. For example, the function "id or inc" here is not relationally parametric:

public class Hey<T>
{
    public T idOrInc(T var)
    {
        if (var instanceof Integer)
            return (T)(new Integer(((Integer)var).intValue()+1));
        return var;
    }
    public static void main(String[] args) {
        Hey<Integer> h = new Hey<Integer>();
        System.out.println(h.idOrInc(new Integer(10)));
        Hey<Double> h2 = new Hey<Double>();
        System.out.println(h2.idOrInc(new Double(10)));
    }
}

The output is:

$ java Hey
11
10.0