2
$\begingroup$

This question is similar to Can we use relational parametricity to simplify the type $\forall a. ( (a \to r) \to r ) \to (a \to r) \to r$? but looks more complicated. It is about using relational parametricity to resolve practical questions in pure functional programming in System F.

Consider the following types of polymorphic functions:

$$ \forall a.\, (a \to r) \to a $$

$$ \forall a.\, (a \to a) \to a $$

$$ \forall a.\, ((a \to a) \to a) \to a $$

$$ \forall a.\, ((a \to r) \to a) \to a $$

$$ \forall a.\, ((a \to r) \to s) \to a $$

where $r$ and $s$ are free type variables, i.e., fixed arbitrary types. Here we only consider pure lambda terms from System F, there are no side effects, all code is fully parametric, and so the parametricity theorems apply.

Question

Under these assumptions, can we simplify these types? What methods are available for this task? Presumably, either we can find simpler equivalent types that have no type quantifiers, or we cannot find such a general simplification (because different models of System F will have different results?).

Discussion

Let me show how I proved the the first two types are void.

I denote the void type by $\underline0$ and the unit type by $\underline1$.

First example

The first type, $\forall a.\, (a \to r) \to a$, is of the form $(\forall a.\,F\,a)$ where $F$ is a covariant functor. The covariant Yoneda lemma shows that $(\forall a.\,F\,a)$ is equivalent to $F\, \underline0$. So, we find:

$$ \forall a.\, (a \to r) \to a \cong \forall a.\,F\,a \cong F\,\underline0 = (\underline0\to r)\to\underline0 \cong \underline1\to\underline0 \cong \underline0$$

Second example

To show that the type $\forall a.\, (a \to a) \to a$ is void, we cannot use the Yoneda lemma. Instead, we need to use the full parametricity theorem with carefully chosen types and relations. I have a shorter proof using something called "strong dinaturality" but this is not a widely known technique, so let me stick to straightforward relational reasoning.

The parametricity theorem says that any value $\phi : \forall a.\, (a \to a) \to a$ is in a certain relation with itself, the relation being the lifting of the identity relation to the type $\forall a.\, (a \to a) \to a$. Denote by superscript the type application, so $\phi^a$ is the function $\phi$ specialized to the type $a$. So, I write $\phi^a : (a \to a) \to a$. To write down the relational parametricity law, we need to lift the identity relation explicitly to the type $\forall a.\, (a \to a) \to a$. After some calculation, we find that, for any types $a$ and $b$ and any relation $r$ between values of types $a$ and $b$, the function $\phi$ must satisfy:

$$ \forall p: a\to a, q: b\to b. \, \textrm{ if } (p,q)\in s \textrm{ then } (\phi^a(p), \phi^b(q))\in r $$

where the relation $s$ is defined between values of types $a\to a$ and $b\to b$ as follows: For any $p: a\to a$ and $q: b\to b$, the values $p$ and $q$ are in relation $s$ if and only if:

$$ \forall x: a, y: b.\,\textrm { if } (x, y)\in r\textrm{ then }(p(x), q(y))\in r$$

Now we apply this condition to the types chosen as follows: $a = \underline0$, $b$ remains arbitrary, $r$ is the empty relation. Then $(x,y)\in r$ never holds for any $x:a$ and $y:b$, since the type $a$ is void.

It follows that any two functions $p: a\to a$ and $q: b\to b$ are always in the relation $s$. Indeed, there are never any values $x:a$ and $y:b$ for which $(x,y)\in r$, so the condition for $(p,q)\in s$ is a condition of the form "if false then ...". That formula is always true.

Now, $p$ must be of type $\underline0 \to\underline0$ and there is only one such $p$: the empty function. But $q: b\to b$ is still arbitrary.

Then the relational parametricity law of $\phi$ says that for arbitrary $q: b\to b$ we must have:

$$ (\phi^a(p), \phi^b(q))\in r $$

Now, $\phi^b(q)$ is the value of $\phi$ for a specific argument $q$. But $r$ is an empty relation to which no values may belong. This contradicts the assumption that a function $\phi$ exists. So, there are no functions $\phi$ of type $\forall a\,(a\to a)\to a$ that satisfy the relational parametricity law.

More generally, I can prove the type equivalence:

$$ \forall a.\,(a \to a)\to F\,a \cong F\,\underline 0 $$

when $F$ is a covariant functor. I write the relational law with the type $a=\underline0$ and find that any function $\phi$ of type $ \forall a.\,(a \to a)\to F\,a $ must ignore its argument (of type $a\to a$). Then the type $ \forall a.\,(a \to a)\to F\,a $ is effectively equivalent to just $\forall a.\,F\,a$, which is in turn equivalent to $F\,\underline0$.

However, these techniques do not apply to the other types listed at the beginning of this post.

$\endgroup$
4
  • $\begingroup$ When you say "p must be of type 0 -> 0 and there is only one such p: the empty function", I think you meant "the identity function"? Your conclusion still holds as you can't extract a value out of an arbitrary endomorphism, which is what the type asks for. $\endgroup$ Sep 30, 2022 at 7:20
  • $\begingroup$ Yes, we have the intuition that "one can't extract information from an arbitrary value of type $a\to a$". But the whole problem here is to convert this intuition into a precise proof. To your comment about the function $p$: There is only one function of type $\underline 0\to\underline0$. I described it as an "empty function" because that function does not have any function body and is never applied to any arguments. You can also think of it as an "identity function for the type $\underline0$". It's still going to be the same function. The type $\underline0\to\underline0$ is equivalent to unit. $\endgroup$
    – winitzki
    Sep 30, 2022 at 8:54
  • $\begingroup$ A relevant paper is Logarithm and program testing. $\endgroup$
    – Li-yao Xia
    Apr 5 at 0:18
  • $\begingroup$ As far as I understood the "Logarithm" paper, their technique will sometimes produce a slightly larger type than necessary. Their focus is on testing, and for testing that's perfectly fine. But it's not so good for deriving type equivalence. $\endgroup$
    – winitzki
    yesterday

2 Answers 2

0
$\begingroup$

We can simplify the five type expressions given in the question. But we need to use different methods for these cases. Parametricity theorems give us a law that a value will satisfy, but we are not always able to derive useful information from those laws directly. We need other techniques.

One technique looks like this: given a type constructor $F$ check whether $F \,\textrm{Void} \cong \textrm{Void}$. It turns out that then we also have $\forall a.\,F\,a \cong \textrm{Void}$.

The reason is that a value of type $\forall a.\,F\,a $ is supposed to work in the same way for every type $a$, including the Void type. For every type $a$ there must be a value of type $F\,a$. If $F \,\textrm{Void} \cong \textrm{Void}$ then we cannot have a value of type $F\,a$ for some $a$, which means that the type $\forall a.\,F\,a$ has no values (is void).

Now we apply this technique to the five cases (assuming that the fixed types $r$ and $s$ are not themselves Void). We find that setting $a = \textrm{Void}$ we get Void for the following types:

$$ \forall a.\, (a \to r) \to a $$

$$ \forall a.\, (a \to a) \to a $$

$$ \forall a.\, ((a \to r) \to s) \to a $$

It means that these three types are void (uninhabited).

The question about this type:

$$ F\, r = \forall a.\, ((a \to r) \to a) \to a $$

is much more complicated. It turns out that $ F\,r \cong r$. Here is a solution:

First, use the contravariant Yoneda identity to get: $$ ((a \to r) \to a) \to a \cong \forall b.\, (b\to a)\to ((b \to r) \to a) \to a $$

This allows us to rewrite the type $F\,r$ equivalently as:

$$ F \, r = \forall a.\, \forall b.\, (b\to a)\to ((b \to r) \to a) \to a $$

Exchange the quantifiers and uncurry some arguments:

$$ F\,r = \forall b.\, \forall a.\, ((b + (b\to r))\to a)\to a $$

Use the covariant Yoneda identity: $$ \forall a. \, (x \to a)\to a \cong x $$

and simplify $F\, r$ further:

$$ F\,r = \forall b.\, b + (b\to r) $$

Now use the "disjunctivity lemma" (see at the end of my answer to Can we use relational parametricity to simplify the type $\forall a. ( (a \to a) \to a ) \to a$?) and simplify:

$$ F\, r = (\forall b.\, b) + (\forall b.\, b\to r) $$

By the Yoneda identity again, we simplify $\forall b. \, b \cong\mathrm{Void}$ and $\forall b.\, b\to r \cong \mathbb1 \to r\cong r$. So, we have finally: $$ F\, r \cong \mathrm{Void} + r \cong r$$

Simplifying the type $\forall a.\,((a\to a)\to a)\to a$ can be done via a similar derivation shown in my answer here: Can we use relational parametricity to simplify the type $\forall a. ( (a \to a) \to a ) \to a$?

$\endgroup$
0
$\begingroup$

Another proof technique that is more intuitive in my biased opinion is to enumerate normal forms of System F terms of the given type.

The most interesting example among those five given is $\forall a. ((a \to r) \to a) \to a$.

  1. A term (or derivation) of $\vdash \forall a. ((a \to r) \to a) \to a$ in $\beta\eta$-normal form must start with introduction rules. There is only one way forward.

  2. An open term of $a : \star, x : (a \to r) \to a \vdash a$ in $\beta\eta$-normal form can only be an application of a variable (because a $\beta$-normal form is a head-normal form). There is only $x$, which expects one argument.

  3. A term of $a : \star, x : \dots \to a \vdash (a \to r)$ in $\beta\eta$-normal form must start with an introduction rule.

  4. Since there were no choices to be made in the previous steps, we have thus obtained a bijection between terms of $\vdash \forall a. ((a \to r) \to a)$ and terms of $a : \star, x : \dots \to a, y : a \vdash r$, which can be closed into terms of type $\forall a. (\dots \to a) \to a \to r$.

  5. Concluding with standard argument by semantic parametricity, that is isomorphic to $r$.

$\endgroup$
6
  • $\begingroup$ This is an interesting technique. I have seen that blog post by G. Scherer and yourself. But I still have questions about that technique. 1) At step 4 you still require a relational parametricity argument (or Yoneda's identity) to show that $\forall a.\,((a\to r)\to a)\to a\to r \cong r$? 2) Would that technique also apply to all other examples in my question and, in particular, to $\forall a.\,((a\to a)\to a)\to a)$? At some point I thought I was able to prove that there was only one term of that type, because I thought there was only one proof in normal form, but I was wrong about that. $\endgroup$
    – winitzki
    Apr 6 at 9:32
  • $\begingroup$ 1. Yes, I don't know how to make that argument syntactically. My point is, in the cases where syntactic parametricity does apply, even if incomplete, it makes things simpler. 2. Yes. For $((a \to a) \to a) \to a$ I just haven't come up with a recipe to distinguish the normal forms thus enumerated, but at the very least, writing down the decision tree like I did makes it obvious that there are more than 2 normal forms. For $(a \to a) \to a$ you run into an infinite descent which implies there is no solution. And for the two others the enumeration terminates immediately. $\endgroup$
    – Li-yao Xia
    Apr 7 at 22:16
  • $\begingroup$ What is the difficulty for $\forall a.\, (...)\to a \to r \cong r$? Is the syntactic technique unable to deal with fixed types (such as $r$ here)? I am getting an impression that the syntactic parametricity technique is good only for terms of the form $\forall a.\, P a$ where $P$ depends only on $a$ and contains no other types. $\endgroup$
    – winitzki
    yesterday
  • $\begingroup$ Now that I think about it in the semantic argument, you never say what the semantic model is. You basically postulate that it somehow internalizes many categorical concepts (notably that polymorphic functions satisfy naturality). But you can instantiate it with the syntactic model, so any "semantic parametricity" argument is actually also a syntactic parametricity argument. $\endgroup$
    – Li-yao Xia
    yesterday
  • $\begingroup$ To me, the important question is what techniques of derivation do we have for solving various problems. The question of model theory is not directly relevant. Suppose we implement a System F interpreter as a specific computer program. Then some kind of semantic model will exist in the computer. And, most likely, that model will be based on sets, because everything in a computer's memory is a set. Maybe theorists have trouble with set-theoretic models of polymorphic lambda calculus, but that only says that the theorists haven't done their job properly, because our program already works. $\endgroup$
    – winitzki
    yesterday

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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