3
$\begingroup$

I am having trouble using parametricity to show that existential types work in System F (or System Fω) in the way one would expect them to work.

It is known that an existential type $\exists t.~P~t$ (where $P$ is any type constructor, not necessarily covariant) is encoded as: $$\forall r.~(\forall t.~P~t \to r)\to r $$

(I think it is assumed that $\forall r$ implies a parametricity constraint.)

Let's denote this encoding as the type constructor $E : (* \to *) \to *$ that takes any $P : * \to *$ and makes a new type $\exists t.~P~t$ out of $P$. (Here, the notation * means the kind of types.)

So, for any type constructor $P$ we define: $$E~P = \forall r.~(\forall t.~P~t \to r)\to r $$

 E P = ∀(r : *) → (∀(t : *) → P t → r) → r

To create values of the type $E~P$, one uses the standard function pack defined as:

 pack : ∀(s : *) → P s → E P
 pack = λ(s : *) → λ(ps : P s) → λ(r : *) → λ(c : ∀(t : *) → P t → r) → c s ps

Now, the main question is:

How to write a function type $(\exists t.~P~t) \to q$, where $q$ is a fixed type.

There are two ways of writing that type:

  1. Just use the encoding $ E~P$ as shown above, and write: $$ T_1= E~P\to q = (\forall r.~(\forall t.~P~t \to r)\to r)\to q $$

  2. Squint at $(\exists t.~P~t) \to q$ and notice that it should be just a function $P~t \to q$ but universally quantified in $t$. So, we should have: $$ T_2 = \forall t.~(P~t \to q) $$

I want to prove that the types $T_1$ and $T_2$ are equivalent, under appropriate parametricity assumptions.

I don't seem to be able to do that, though. What I tried:

  • Write explicit code for functions $\mathrm{out} : T_1 \to T_2 $ and $\mathrm{in}:T_2\to T_1$ and then prove that in and out are inverses.

    out : (E P → q) → ∀(t : *) → P t → q
    out = λ(y : E P → q) → λ(t : *) → λ(pt : P t) → y (pack t pt)
    
    in : (∀(t : *) → P t → q) → E P → q
    in = λ(c : ∀(t : *) → P t → q) → λ(ep : E P) → ep q c
    

I can prove that out . in = id (this is just straightforward substitution).

The difficult direction is to prove that in . out = id; this requires some parametricity assumptions. I tried using the naturality law of $ E~P$ but that does not seem to be enough.

Specifically, after using the naturality law, it still remains to prove that, for any $e : E~P$, that is, $e : \forall r.~(\forall t.~P~t \to r)\to r$, we will have: $$ e~ (E~ P)~ \mathrm{pack} = e $$

  • The Yoneda identities do not apply because of the universal quantifier inside $\forall t. ~P~t\to r$.

  • I have read Wadler's "Recursive types for free" but the techniques in there don't seem to help so far. The identity e (E P) pack == e is superficially similar to the identity (4) shown in Wadler: fold T in = id but the types are different and I can't prove what I need.

$\endgroup$

1 Answer 1

3
$\begingroup$

Using function extensionality, it suffices to prove:

$$∀ Z\ z. e\ (E\ P)\ \mathrm{pack}\ Z\ z = e\ Z\ z$$

The naturality rule for $e$ is:

$$f\ (e\ A\ k) = e\ B\ (ΛR. λr. f\ (k\ R\ r))$$

If we pick $k = \mathrm{pack}$, so $A = E\ P$, and $f\ e = e\ Z\ z$, then we get:

$$e\ (E\ P)\ \mathrm{pack}\ Z\ z = e\ Z\ (ΛR. λr. \mathrm{pack}\ R\ r\ Z\ z) = e\ Z\ (ΛR. λr. z\ R\ r) = e\ Z\ z$$

So that gets you the $e\ (E\ P)\ \mathrm{pack} = e$ equation you want.

$\endgroup$
1
  • $\begingroup$ Thank you, that looks perfect. I didn't think of writing out the extensional equality of functions like you did (with an arbitrary Z z). Without that, I could not find a suitable f for the naturality law. I will need to go through your derivation once again before approving the answer. $\endgroup$
    – winitzki
    Apr 1 at 21:34

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.