13
$\begingroup$

Is there some natural way to understand the essence of relational semantics for parametric polymorphism?

I have just started reading about the notion of relational parametricity, a la John Reynolds' "Types, Abstraction and Parametric Polymorphism", and I am having trouble understanding how the relational semantics is motivated. Set semantics makes perfect sense to me, and I realise that set semantics is insufficient to describe parametric polymorphism, but the leap to relational semantics seems to be magic, coming completely out of nowhere.

Is there some way of explaining it along the lines "Assume relations on the base types and terms, and then the interpretation of the derived terms is just the natural relationship between ...such and such a natural thing... in your programming language"? Or some other natural explanation?

$\endgroup$
20
$\begingroup$

Well, relational parametricity is one of the most important ideas introduces by John Reynolds, so it shouldn't be too much of a surprise that it looks like magic. Here is a fairy tale about how he might have invented it.

Suppose you're trying to formalize the idea that certain functions (identity, map, fold, reversal of lists) act "the same way on many types", i.e., you have some intuitive ideas about parametric polymorphism, and you have formulated some rules for creating such maps, i.e., the polymorphic $\lambda$-calculus or some early variant of it. You notice that naive set-theoretic semantics is not working.

For instance, we stare at the type $$\forall X : \mathsf{Type} . X \to X,$$ which should contain only the identity map, but naive set-theoretic semantics allows unwanted functions such as $$\lambda X : \mathsf{Type} . \lambda a : X . \mathsf{if}\ (X = \lbrace 0, 1 \rbrace) \ \mathsf{then} \ 0 \ \mathsf{else}\ a.$$ To eliminate this sort of thing, we need to impose some further conditions on functions. For instance, we could try some domain theory: equip each set $X$ with a partial order $\leq_X$ and require that all functions be monotone. But that doesn't quite cut it because the above unwanted function is either constant or identity, depending on $X$, and those are monotone maps.

A partial order $\leq$ is relfexive, transitive and antisymmetric. We can try to alter the structure, for instance we could try to use a strict partial order, or a linear order, or an equivalence relation, or just a symmetric relation. However, in each case some unwanted examples creep in. For instance, symmetric relations eliminate our unwanted function but allow other uwanted functions (exercise).

And then you notice two things:

  1. The wanted examples are never eliminated, whatever relations you use in place of partial orders $\leq$.
  2. For each particular unwnated example you look at, you can find a relation that eliminates it, but there is no single relation that eliminates all of them.

So, you have the brilliant thought that the wanted functions are those that preserve all relations, and the relational model is born.

$\endgroup$
  • 1
    $\begingroup$ Thanks Andrej. This raises the further question: is there any smaller subclass of relations that eliminate all the unwanted examples? $\endgroup$ – Tom Ellis Oct 27 '13 at 21:32
  • $\begingroup$ Well, we can probably limit the logical complexity of the relations because we only have to worry about computable maps. But I am not enough of an expert to answer. I summon @UdayReddy. $\endgroup$ – Andrej Bauer Oct 27 '13 at 22:07
  • 2
    $\begingroup$ @TomEllis. Yes, in special cases, a subclass of relations might suffice. The most immediate special case is that, if all operations are first-order, then functions (total, single-valued relations) are enough. For fields, partial isomorphisms are enough. Recall that Reynolds's leading example is the field of complex numbers, and his logical relation between Bessel and Descartes is a partial isomorphism. $\endgroup$ – Uday Reddy Nov 23 '13 at 21:53
  • 4
    $\begingroup$ @AndrejBauer. Note that $\forall X.\, X \to X$ has exactly one parametric element, but the ad hoc elements are too many to form a set! So, there is a lot of cutting to do. An alternative theory of how Reynolds might have gotten parametricity appears in our upcoming "Essence of Reynolds". $\endgroup$ – Uday Reddy Nov 23 '13 at 22:13
  • $\begingroup$ You show that if you interpret types as sets then there are unwanted functions. Doesn't the same apply to relations? \X:Type. \a:X. if X = {(0,0), (1,0), (0,1), (1,1)} then 0 else a $\endgroup$ – Jules Dec 3 '14 at 18:27
11
$\begingroup$

The answer to your question is really there in Reynolds's fable (Section 1). Let me try and interpret it for you.

In a language or formalism in which types are treated as abstractions, a type variable can stand for any abstract concept whatsoever. We don't assume that types are generated via some syntax of type terms, or some fixed collection of type operators, or that we can test two types for equality etc. In such a language, if a function involves a type variable then the only thing the function can do to values of that type is to shuffle around the values it has been given. It cannot invent new values of that type, because it doesn't "know" what that type is! That is the intuitive idea of parametricity.

Then Reynolds thought about how to capture this intuitive idea mathematically, and noticed the following principle. Suppose we instantiate the type variable, say $t$, to two different concrete types, say $A$ and $A'$, in separate instantiations, and keep in our mind some correspondence $R : A \leftrightarrow A'$ between the two concrete types. Then we can imagine that, in one instance, we provide a value $x \in A$ to the function and, in the other instance, a corresponding value $x' \in A'$ (where "corresponding" means that $x$ and $x'$ are related by $R$). Then, since the function knows nothing about the types we are supplying for $t$ or the values of that type, it has to treat $x$ and $x'$ in exactly the same way. So, the results we get from the function should again correspond by the relation $R$ we have kept in our mind, i.e., wherever the element $x$ appears in the result of one instance, the element $x'$ must appear in the other instance. Thus, a parametrically polymorphic function should preserve all possible relational correspondences between possible instantiations of type variables.

This idea of preservation of correspondences is not new. Mathematicians have known about it for a long time. In the first instance, they thought that polymorphic functions should preserve isomorphisms between type instantiations. Note that isomorphism means some idea of a one-to-one correspondence. Apparently, isomorphisms were originally called "homomorphisms". Then they realized that what we now call "homomorphisms", i.e., some idea of many-to-one correspondences, would be preserved too. Such preservation goes by the name of natural transformation in category theory. But, if we think about it keenly, we realize that preservation of homomorphisms is utterly unsatisfying. The types $A$ and $A'$ we mentioned are completely arbitrary. If we pick $A$ as $A'$ and $A'$ as $A$, we should get the same property. So, why should "many-to-one correspondence", an asymmetric concept, play a role in formulating a symmetric property? Thus, Reynolds took the big step of generalizing from homomorphisms to logical relations, which are many-to-many correspondences. The full impact of this generalization is not yet fully understood. But the underlying intuition is fairly clear.

There is one further subtlety here. Whereas the instantiations of type variables can be arbitrarily varied, constant types should stay fixed. So, when we formulate the relational correspondence for a type expression with both variable types and constant types, we should use the chosen relation $R$ wherever the type variable appears and the identity relation $I_K$ wherever a constant type $K$ appears. For instance, the relation expression for the type $t \times Int \to Int \times t$ would be $R \times I_{Int} \to I_{Int} \times R$. So, if $f$ is a function of this type, it should map a pair $(x,n)$ and a related $(x',n)$ to some pair $(m,x)$ and related $(m,x')$. Note that we are obliged to test the function by putting the same values for constant types in the two cases, and we are guaranteed to get the same values for constant types in the outputs. So, in formulating relational correspondences for type expressions, we should make sure that, by plugging in identity relations (representing the idea that those types are going to be consant), we get back identity relations, i.e., $F(I_{A_1},\ldots,I_{A_n}) = I_{F(A_1,\ldots,A_n)}$. This is the crucial identity extension property.

To understand parametricity intuitively, all you need to do is to pick some samplee function types, think of what functions can be expressed of those types, and think about how those functions behave if you plug in different instantiations of type variables and different values of those instantiation types. Let me suggest a few function types to get you started: $t \to t$, $t \to Int$, $Int \to t$, $t \times t \to t \times t$, $(t \to t) \to t$, $(t \to t) \to (t \to t)$.

$\endgroup$
  • $\begingroup$ Finally, my summon worked! $\endgroup$ – Andrej Bauer Nov 23 '13 at 19:24
  • 2
    $\begingroup$ @AndrejBauer. Hmm, I didn't get a summon actually. It may be that the @ UdayReddy incantation works only at the beginning of the comment. In any case, no summons needed. "Parametricity" is among my filters. $\endgroup$ – Uday Reddy Nov 23 '13 at 21:45
  • $\begingroup$ "the only thing the function can do to values of that type is to shuffle around the values it has been given" - actually, apart from the shuffling, the function can erase the given value (weakening) and copy it (contraction). Since these operations are always available, the value is not as abstract as it may seem. $\endgroup$ – Łukasz Lew Jun 7 '18 at 20:30
  • $\begingroup$ @ŁukaszLew, you are right. I don't know if that can be characterized as loss of "abstraction" though. $\endgroup$ – Uday Reddy Jun 9 '18 at 18:06
  • $\begingroup$ @UdayReddy I've removed the commend and asked this as a stand-alone question. $\endgroup$ – Łukasz Lew Jun 9 '18 at 20:32
3
$\begingroup$

Another possible answer different from Andrej's is the given by the example of the $\omega$-set model of polymorphism. Since every function in the polymorphic calculus is computable, it's natural to interpret a type by a set of numbers which represent the computable functions of that type.

Furthermore, it's tempting to identify functions with the same extensional behavior, thus leading to an equivalence relation. The relation is partial if we exclude the "undefined" functions, that is the functions which "loop" for some well-formed input.

The PER models are a generalization of this.

Another way to see these models are as a (very) special case of the simplicial set models of Homotopy Type Theory. In that framework, types are interpreted as (a generalization of), sets with relations, and relations between those relations, etc. At the lowest level, we simply have the PER models.

Finally, the field of constructive mathematics has seen the appearance of related notions, in particular the Set Theory of Bishop involves describing a set by giving both elements and an explicit equality relation, which must be an equivalence. It's natural to expect some principles of constructive mathematics make their way into type theory.

$\endgroup$
  • 1
    $\begingroup$ Ah, but the PER models are not very nice and can contain uwnanted polymorphic functions. One has to pass to the relational PER models to get rid of them. $\endgroup$ – Andrej Bauer Oct 28 '13 at 21:01
  • $\begingroup$ I still feel it motivates the relational approach though. $\endgroup$ – cody Oct 28 '13 at 22:55
  • $\begingroup$ @cody. I agree. I think of PERs as a way of building in relations into the "set theory" so that we can get impredicative models in the first place. Thanks for mentioning Homotopy type theory. I didn't know it had similar ideas. $\endgroup$ – Uday Reddy Nov 23 '13 at 22:24
  • $\begingroup$ @UdayReddy: the ideas are very similar! In particular, the idea of "compatible dependent implementations" which relate abstract types with dependencies can be understood through the lens of the univalent equality. $\endgroup$ – cody Nov 24 '13 at 0:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.