<p>Regarding question 1): the variable $Y$ <em>must not</em> appear in $Y$, indeed it needs to be unconstrained. If you want to have any hope of the lhs being equal to the rhs, certainly you should have the same number of free variables on each side, which is impossible if $Y$ gets captured in $T$. The intuition is that $\exists T$ should be equal to the infinite conjunction
$$ ((\forall x. T\rightarrow U_0)\rightarrow U_0)\wedge((\forall x. T\rightarrow U_1)\rightarrow U_1)\wedge\ldots $$
for every possible type $U_i$. Indeed, it is not hard to show for any <em>specific</em> type $U$ that $$\exists x.T \rightarrow ((\forall x. T\rightarrow U)\rightarrow U)$$</p>

<p>In words:</p>

<blockquote>
  <p>Proving that if there is <em>some</em> (arbitrary) $x$ such that $T(x)$ holds, then $U$ holds is the same as proving that for <em>any</em> $x$, if $T(x)$ holds than so does $U$.</p>
</blockquote>

<p>Note that $U$ must not itself depend on $x$.</p>

<p>The intuition behind the equality is that this fact, for <em>every possible $U$</em> is sufficient to characterize the existential quantifier.</p>

<p>For 2), the set theoretic intuition is a bit difficult here, I'm afraid. It's not <em>naively</em> possible to think of types as sets of elements and arrows as the set-theoretic functions between them. However, intuitively, if some intersection $\bigcap_S A(S)$ is non-empty, then $A(\varnothing)$ should be non empty. In your case this gives
$$ \left(\bigcap_R \left(T[x:=R]\rightarrow \varnothing\right)\right)\rightarrow\varnothing$$</p>

<p>(note the parenthesization) which needs to be non-empty. But the only way for that is that there is some $R$ such that
$T[x:=R]\rightarrow \varnothing$ is empty, which means that $T[x:=R]$ needs to be non-empty.</p>

CC BY-SA 3.0
2015-09-12T22:41:49.317Z
No! Not an infinite conjunction. It is an infinite *product*. The conjunction forgets what happened at each type $U_i$ and that's nasty. (Let's not tell anybody that in the realizability models of System F the universal quantifier *is* intersection.)
Andrej Bauer
CC BY-SA 3.0
2015-09-14T13:52:19.747Z
@AndrejBauer: that's fair, though sometimes it's useful to forget information... my intuition is partly based on the elimination rule of $\exists$.
cody
CC BY-SA 3.0
2015-09-14T15:27:32.500Z
You can only forget information under suitable circumstances that guarantee that you will still get away with it. For instance, in the realizability models where $\forall$ actually is $\bigcap$ we can forget information because of the amazing amount of uniformity of the realizers. If you forget information when you should not be doing it, then you'll just invalidate the laws.
Andrej Bauer
CC BY-SA 3.0
2015-09-12T22:37:09.403Z
2015-09-12T22:37:09.403Z
cody
<p>I suggest not to give up on the operational intuition. Operational 
is primary, all semantics are derived, and are but proof techniques
for operational semantics. The key ideas are as follows.</p>

<p>A program $P$ uses a variable $x$ <strong>universal-polymorphically</strong>, provided $P$
doesn't do anything with $x$ that requires knowledge of $x$'s type. For example in the
$\lambda$-calculus the following operations could be polymorphic (whether
they are or not depends on the precise language semantics).</p>

<ul>
<li>forwarding, e.g. $\lambda x.x.$,</li>
<li>reordering, e.g. $\lambda (x,y,z). (z,x, y)$.</li>
<li>duplicating, e.g. $\lambda x.(x,x)$.</li>
<li>dropping, e.g. $\lambda x.7$.</li>
</ul>

<p>Now existential-polymophism is the exact <strong>dual</strong> of
universal-polymorphism: a program $P$ uses a variable $x$
<strong>existential-polymophially</strong>, if $P$ provides $x$ only to <strong>contexts</strong>
that don't require knowledge of $x$'s type. In other words, $P$ provides
$x$ only to contexts that use $x$ universal-polymorphically.</p>

<p>In my opinion this <strong>beautiful symmetry</strong>, is obscured when thinking about universal/existential polymorphism in the
$\lambda$-calculus. The reason is the 
heavy reliance on the function space operator which alas is not really a
dualising operator, but something more complicated (covariant in one argument, contravariant in the other).</p>

CC BY-SA 3.0
2015-09-13T16:14:27.110Z
An interesting point of view (even though I don't understand it fully :)). The idea is then to check if laws derived in such general view hold in concrete settings of type systems? And where can I find some introductory text about this?
socumbersome
CC BY-SA 3.0
2015-09-14T08:48:59.597Z
@socumbersome Most existing implementations of polymorphism don't get this quite right. Indeed existential quantification is rarely implemented directly. I'm afraid there is no introductory text describing the duality. We have explained it [here](http://users.sussex.ac.uk/~mfb21/publications/fossacs03/index.html) but it's written for a specialised audience.
Martin Berger
CC BY-SA 3.0
2015-09-13T12:56:07.397Z
2015-09-13T12:56:07.397Z
Martin Berger
<p>Set theory is doing you some harm here and the sooner you liberate yourself from it the better it will be for your understanding of computer science.</p>

<p>Forget the intersections and unions. People get this idea that $\forall$ and $\exists$ are like $\bigcap$ and $\bigcup$, which is the sort of thing the Polish school was doing a long time ago with Boolean algebras, but it's really not the way to go (definitely not in computer science).</p>

<p>You would like to look at these as sets. Ok, but then we have to ignore issues of size and pretend that there is a set of all sets. (It is possible to fix the issues of size by passing to a different category.) The type $\forall x . T$ is really like the cartesian product
$$\forall X . T \mathrel{{:}{=}} \prod_{S : \mathsf{Set}} T[X \mapsto S].$$
That is, an element of $\forall X . T$ is a <em>function</em> $f$ from sets to sets: for each set $S$ it gives an element $f(S)$ of type $T[x \mapsto S]$. For instance, an element of $\forall X. (X \to X) \to (X \to X)$ is a function $f$ which takes a set $S$ and gives a function of type $(S \to S) \to (S \to S)$. Here are some such functions:
\begin{align*}
f_0(S)(g)(x) &amp;\mathrel{{:}{=}} x \\
f_1(S)(g)(x) &amp;\mathrel{{:}{=}} g(x) \\
f_2(S)(g)(x) &amp;\mathrel{{:}{=}} g(g(x)) \\
f_3(S)(g)(x) &amp;\mathrel{{:}{=}} g(g(g(x)))
\end{align*}
So we get one for every natural number, and it's kind of hard to think of any other examples. (Exercise: google "Church encoding of natural numbers".)</p>

<p>Next, let us look at the existential types. Firstly, the correct encoding of $\exists$ in terms of $\forall$ is
$$\exists X . T \mathrel{{:}{=}} \forall Y . (\forall X . (T \to Y)) \to Y$$
<em>where the variable $Y$ does not appear in $T$</em>! (This should be mentioned in Pierce's TAPL.) Before we look at this encoding, let us do $\exists X . T$ directly in terms of sets. This time it is a coproduct:
$$\exists X . T \mathrel{{:}{=}} \coprod_{S : \mathsf{Set}} T[X \mapsto S].$$
An element of $\exists X . T$ is a <em>pair</em> $(S, a)$ where $S$ is a set and $a$ is an element of $T[X \mapsto S]$. An example would the the type $\exists X . (X \times X \to X)$, whose elements are pairs $(S, m)$ where $S$ is a set and $m : S \times S \to S$ is a binary operation on it. This is also known as a <em>magma</em>. If you get a bit fancier you can express well known structures such as groups and rings (you need to invent <em>identity types</em> first).</p>

<p>Let us see how the encoding of $\exists$ in terms of $\forall$ works. It is <em>wrong</em> to expect that we will get an <em>equality</em> between $\exists X. T$ and $\forall Y . (\forall X . (T \to Y)) \to Y$ (NB: $Y$ is fresh) – only set theory would give people such expectations. We should expect the two to be <em>isomorphic</em>. So the task is to find a bijection between
$$A \mathrel{{:}{=}} \coprod_{S : \mathsf{Set}} T[X \mapsto S]$$
and
$$B \mathrel{{:}{=}} \prod_{R : \mathsf{Set}} \left(\prod_{S : \mathsf{Set}} (T[X \mapsto S] \to R) \right) \to R.$$
This is an exercise in $\lambda$-calculus. In one direction we have the map $f : A \to B$ defined as
$$f(S,a)(R)(h) \mathrel{{:}{=}} h(S)(a)$$
and in the other a map $g : B \to A$ defined by
$$g(\phi) \mathrel{{:}{=}} \phi(A)(\lambda S . \lambda a . (S, a)).$$
(The notation $\lambda S . \lambda a . (S, a)$ means the function $S \mapsto a \mapsto (S, a)$.) Now we can check whether $f$ and $g$ are inverses of each other. One direction is easy:
$$g(f(S,a)) = f(S,a)(A)(\lambda S' . \lambda a' . (S', a'))
  = (\lambda S' . \lambda a' . (S', a')(S)(a) = (S, a).$$
The other direction looks like this:
$$f(g(\phi))(R)(h) = h(\pi_1(g(\phi))(\pi_2(g(\phi))).$$
We could go on a bit more by rewriting $g(\phi)$ to $\phi(A)(\lambda S . \lambda a . (S, a))$, but then we would get stuck!</p>

<p>It turns out that in set theory the encoding of $\exists$ in terms of $\forall$ <em>does</em> not work. But it does work in other setups, where types are not sets. For instance, you can convince yourself that in logic the statements
$$\exists x . \phi(x)$$
is equivalent to
$$\forall{P : \mathsf{Prop}} . (\forall x . (\phi(x) \Rightarrow P)) \Rightarrow P,$$
where $P$ ranges over all propositions (truth values, logical statements). Again, the variable $P$ should not occur in $\phi$.</p>

CC BY-SA 3.0
2015-09-12T22:37:52.313Z
Andrej, you are as fast as lightning!
cody
CC BY-SA 3.0
2015-09-13T11:11:59.023Z
This is enlightening, thank you! But I still have questions :) 1) do I understand correctly, that the setup you presented is still set-theoretic (but not as naive as mine) and that's why $(*)$ doesn't hold and we have no hopes for finding appropriate $f$ and $g$? 2) I understand that in logic those statements are equivalent but it seems to me that it escapes a bit from type theory (well, because where are the types? :)). So, what would be the setting of type system in which $(*)$ holds? 3) if I'm implementing language based on lambda calculus -- should I be careful about using $(*)$?
socumbersome
CC BY-SA 3.0
2015-09-13T19:46:10.050Z
Correct: the set-theoretic "model" (it is *not* a model because we pretend that we can make cartesian products indexed by *all* sets) violates the encoding of $\exists$ in terms of $\forall$. Type theory likewise does *not* validate the encoding either. Instead, it gives you a retraction (just use the same $f$ and $g$ above for type theory), but not an isomorphism. To get an isomorphism you need something extra, for instance [*parametricity*](https://en.wikipedia.org/wiki/Parametricity) makes sure that all elements of the cartesian product are nicely behaved and recovers the isomorphism.
Andrej Bauer
CC BY-SA 4.0
2019-01-26T20:36:53.100Z
@AndrejBauer is the underlying system impredicative? And in case of a positive answer does the isomorphism hold for predicative systems?
Giorgio Mossa
CC BY-SA 4.0
2019-01-26T22:50:57.590Z
@GiorgioMossa: what system? Are you asking whether one needs impredicativity to establish the validity of the encoding of $\exists$ in terms of $\forall$? No, parametricity is sufficient, although sometimes impredicativity helps (for instance when we express $\exists$ using $\forall$ ni a topos).
Andrej Bauer
CC BY-SA 4.0
2019-01-27T13:35:07.067Z
@AndrejBauer that's exactly what I was looking for. Thank you.
Giorgio Mossa
CC BY-SA 3.0
2015-09-12T22:35:01.267Z
2015-09-12T22:35:01.267Z
Andrej Bauer
<p>I'm trying to wrap my head around the concepts of universal and existential types but everywhere I look, I see either logical or operational intuitions (or implementations) (e.g. TAPL book by B. Pierce), which, well... is good, but I'd like to see the definitions (where we look at them as sets) -- and from them, derivations of some laws, as well as justifications for our intuitions.</p>

<p>So, because I cannot find those definitions, I decided to do it myself and I think these may be reasonable:</p>

<p>$$\forall x.T \overset{def}{:=} \bigcap_{S - type} T[x := S] $$
$$\exists x.T \overset{def}{:=} \bigcup_{S - type} T[x := S] $$</p>

<p>But, in the aforementioned TAPL book, we are given this definition (although I would call it an identity)</p>

<p>$$\exists x.T \overset{def}{:=} \forall y. (\forall x. T \rightarrow y) \rightarrow y \quad (*)$$</p>

<p>I have two problems with this:</p>

<ol>
<li>On the LHS of $(*)$ I would expect that $x$ was the only free variable of $T$ (because how to view a type "not-yet-built" with some free variables dangling in it?), but on the RHS it seems like $y$ may have some impact on $T$, so it better be a free variable in $T$. Hence LHS cannot be equal to RHS because sets of free variables of $T$ differ on both sides, right?</li>
<li>Even disregarding the concern at the point 1. -- I tried to rewrite RHS using my definitions and see if I can get my definition of existential type but I stuck:
$$ RHS = \bigcap_{S} (\forall x.T \rightarrow y)[y := S] \rightarrow S  = \bigcap_{S} \left(\bigcap_{R} T[x := R, y := S] \rightarrow S\right) \rightarrow S $$</li>
</ol>

<p>It doesn't even remotely resemble my definition. Is it possible to simplify the formula I arrived at? Intuitively, because there are function types, it probably will never be equal to my definition. But if they are not equal -- are they at least 'isomorphic' in some sense? If not -- what "went wrong"?</p>

CC BY-SA 3.0
2015-09-12T22:15:51.917Z
There's a typo in your equation (*): it should be $\forall Y$ rather than $\forall y$.
cody
CC BY-SA 3.0
2015-09-12T22:39:34.750Z
Also, in your last equation: $y$ may not appear in $T$!
cody
<lo.logic><type-theory><type-systems><set-theory>
Universal and existential types
socumbersome
# Universal and existential types

(Asked by: username_0 on 2015-09-12)

I'm trying to wrap my head around the concepts of universal and existential types but everywhere I look, I see either logical or operational intuitions (or implementations) (e.g. TAPL book by B. Pierce), which, well... is good, but I'd like to see the definitions (where we look at them as sets) -- and from them, derivations of some laws, as well as justifications for our intuitions.

So, because I cannot find those definitions, I decided to do it myself and I think these may be reasonable:

$$\forall x.T \overset{def}{:=} \bigcap\_{S - type} T[x := S] $$
$$\exists x.T \overset{def}{:=} \bigcup\_{S - type} T[x := S] $$

But, in the aforementioned TAPL book, we are given this definition (although I would call it an identity)

$$\exists x.T \overset{def}{:=} \forall y. (\forall x. T \rightarrow y) \rightarrow y \quad (\*)$$

I have two problems with this:

1. On the LHS of $(\*)$ I would expect that $x$ was the only free variable of $T$ (because how to view a type "not-yet-built" with some free variables dangling in it?), but on the RHS it seems like $y$ may have some impact on $T$, so it better be a free variable in $T$. Hence LHS cannot be equal to RHS because sets of free variables of $T$ differ on both sides, right?
2. Even disregarding the concern at the point 1. -- I tried to rewrite RHS using my definitions and see if I can get my definition of existential type but I stuck:
   $$ RHS = \bigcap\_{S} (\forall x.T \rightarrow y)[y := S] \rightarrow S = \bigcap\_{S} \left(\bigcap\_{R} T[x := R, y := S] \rightarrow S\right) \rightarrow S $$

It doesn't even remotely resemble my definition. Is it possible to simplify the formula I arrived at? Intuitively, because there are function types, it probably will never be equal to my definition. But if they are not equal -- are they at least 'isomorphic' in some sense? If not -- what "went wrong"?

**Tags:** lo.logic, type-theory, type-systems, set-theory

> **Comments:**
> **username_1**: There's a typo in your equation (*): it should be $\forall Y$ rather than $\forall y$.  
> **username_1**: Also, in your last equation: $y$ may not appear in $T$!  

---

## 3 answers

### Answer by username_2 on 2015-09-12. Score: 10 | Accepted answer

Set theory is doing you some harm here and the sooner you liberate yourself from it the better it will be for your understanding of computer science.

Forget the intersections and unions. People get this idea that $\forall$ and $\exists$ are like $\bigcap$ and $\bigcup$, which is the sort of thing the Polish school was doing a long time ago with Boolean algebras, but it's really not the way to go (definitely not in computer science).

You would like to look at these as sets. Ok, but then we have to ignore issues of size and pretend that there is a set of all sets. (It is possible to fix the issues of size by passing to a different category.) The type $\forall x . T$ is really like the cartesian product
$$\forall X . T \mathrel{{:}{=}} \prod\_{S : \mathsf{Set}} T[X \mapsto S].$$
That is, an element of $\forall X . T$ is a *function* $f$ from sets to sets: for each set $S$ it gives an element $f(S)$ of type $T[x \mapsto S]$. For instance, an element of $\forall X. (X \to X) \to (X \to X)$ is a function $f$ which takes a set $S$ and gives a function of type $(S \to S) \to (S \to S)$. Here are some such functions:
\begin{align\*}
f\_0(S)(g)(x) &\mathrel{{:}{=}} x \\
f\_1(S)(g)(x) &\mathrel{{:}{=}} g(x) \\
f\_2(S)(g)(x) &\mathrel{{:}{=}} g(g(x)) \\
f\_3(S)(g)(x) &\mathrel{{:}{=}} g(g(g(x)))
\end{align\*}
So we get one for every natural number, and it's kind of hard to think of any other examples. (Exercise: google "Church encoding of natural numbers".)

Next, let us look at the existential types. Firstly, the correct encoding of $\exists$ in terms of $\forall$ is
$$\exists X . T \mathrel{{:}{=}} \forall Y . (\forall X . (T \to Y)) \to Y$$
*where the variable $Y$ does not appear in $T$*! (This should be mentioned in Pierce's TAPL.) Before we look at this encoding, let us do $\exists X . T$ directly in terms of sets. This time it is a coproduct:
$$\exists X . T \mathrel{{:}{=}} \coprod\_{S : \mathsf{Set}} T[X \mapsto S].$$
An element of $\exists X . T$ is a *pair* $(S, a)$ where $S$ is a set and $a$ is an element of $T[X \mapsto S]$. An example would the the type $\exists X . (X \times X \to X)$, whose elements are pairs $(S, m)$ where $S$ is a set and $m : S \times S \to S$ is a binary operation on it. This is also known as a *magma*. If you get a bit fancier you can express well known structures such as groups and rings (you need to invent *identity types* first).

Let us see how the encoding of $\exists$ in terms of $\forall$ works. It is *wrong* to expect that we will get an *equality* between $\exists X. T$ and $\forall Y . (\forall X . (T \to Y)) \to Y$ (NB: $Y$ is fresh) – only set theory would give people such expectations. We should expect the two to be *isomorphic*. So the task is to find a bijection between
$$A \mathrel{{:}{=}} \coprod\_{S : \mathsf{Set}} T[X \mapsto S]$$
and
$$B \mathrel{{:}{=}} \prod\_{R : \mathsf{Set}} \left(\prod\_{S : \mathsf{Set}} (T[X \mapsto S] \to R) \right) \to R.$$
This is an exercise in $\lambda$-calculus. In one direction we have the map $f : A \to B$ defined as
$$f(S,a)(R)(h) \mathrel{{:}{=}} h(S)(a)$$
and in the other a map $g : B \to A$ defined by
$$g(\phi) \mathrel{{:}{=}} \phi(A)(\lambda S . \lambda a . (S, a)).$$
(The notation $\lambda S . \lambda a . (S, a)$ means the function $S \mapsto a \mapsto (S, a)$.) Now we can check whether $f$ and $g$ are inverses of each other. One direction is easy:
$$g(f(S,a)) = f(S,a)(A)(\lambda S' . \lambda a' . (S', a'))
= (\lambda S' . \lambda a' . (S', a')(S)(a) = (S, a).$$
The other direction looks like this:
$$f(g(\phi))(R)(h) = h(\pi\_1(g(\phi))(\pi\_2(g(\phi))).$$
We could go on a bit more by rewriting $g(\phi)$ to $\phi(A)(\lambda S . \lambda a . (S, a))$, but then we would get stuck!

It turns out that in set theory the encoding of $\exists$ in terms of $\forall$ *does* not work. But it does work in other setups, where types are not sets. For instance, you can convince yourself that in logic the statements
$$\exists x . \phi(x)$$
is equivalent to
$$\forall{P : \mathsf{Prop}} . (\forall x . (\phi(x) \Rightarrow P)) \Rightarrow P,$$
where $P$ ranges over all propositions (truth values, logical statements). Again, the variable $P$ should not occur in $\phi$.

> **Comments:**
> **username_1**: Andrej, you are as fast as lightning!  
> **username_0**: This is enlightening, thank you! But I still have questions :) 1) do I understand correctly, that the setup you presented is still set-theoretic (but not as naive as mine) and that's why $(*)$ doesn't hold and we have no hopes for finding appropriate $f$ and $g$? 2) I understand that in logic those statements are equivalent but it seems to me that it escapes a bit from type theory (well, because where are the types? :)). So, what would be the setting of type system in which $(*)$ holds? 3) if I'm implementing language based on lambda calculus -- should I be careful about using $(*)$?  
> **username_2**: Correct: the set-theoretic "model" (it is *not* a model because we pretend that we can make cartesian products indexed by *all* sets) violates the encoding of $\exists$ in terms of $\forall$. Type theory likewise does *not* validate the encoding either. Instead, it gives you a retraction (just use the same $f$ and $g$ above for type theory), but not an isomorphism. To get an isomorphism you need something extra, for instance [*parametricity*](https://en.wikipedia.org/wiki/Parametricity) makes sure that all elements of the cartesian product are nicely behaved and recovers the isomorphism.  
> **username_4**: @AndrejBauer is the underlying system impredicative? And in case of a positive answer does the isomorphism hold for predicative systems?  
> **username_2**: @GiorgioMossa: what system? Are you asking whether one needs impredicativity to establish the validity of the encoding of $\exists$ in terms of $\forall$? No, parametricity is sufficient, although sometimes impredicativity helps (for instance when we express $\exists$ using $\forall$ ni a topos).  
> **username_4**: @AndrejBauer that's exactly what I was looking for. Thank you.  

---

### Answer by username_1 on 2015-09-12. Score: 3

Regarding question 1): the variable $Y$ *must not* appear in $Y$, indeed it needs to be unconstrained. If you want to have any hope of the lhs being equal to the rhs, certainly you should have the same number of free variables on each side, which is impossible if $Y$ gets captured in $T$. The intuition is that $\exists T$ should be equal to the infinite conjunction
$$ ((\forall x. T\rightarrow U\_0)\rightarrow U\_0)\wedge((\forall x. T\rightarrow U\_1)\rightarrow U\_1)\wedge\ldots $$
for every possible type $U\_i$. Indeed, it is not hard to show for any *specific* type $U$ that $$\exists x.T \rightarrow ((\forall x. T\rightarrow U)\rightarrow U)$$

In words:

> Proving that if there is *some* (arbitrary) $x$ such that $T(x)$ holds, then $U$ holds is the same as proving that for *any* $x$, if $T(x)$ holds than so does $U$.

Note that $U$ must not itself depend on $x$.

The intuition behind the equality is that this fact, for *every possible $U$* is sufficient to characterize the existential quantifier.

For 2), the set theoretic intuition is a bit difficult here, I'm afraid. It's not *naively* possible to think of types as sets of elements and arrows as the set-theoretic functions between them. However, intuitively, if some intersection $\bigcap\_S A(S)$ is non-empty, then $A(\varnothing)$ should be non empty. In your case this gives
$$ \left(\bigcap\_R \left(T[x:=R]\rightarrow \varnothing\right)\right)\rightarrow\varnothing$$

(note the parenthesization) which needs to be non-empty. But the only way for that is that there is some $R$ such that
$T[x:=R]\rightarrow \varnothing$ is empty, which means that $T[x:=R]$ needs to be non-empty.

> **Comments:**
> **username_2**: No! Not an infinite conjunction. It is an infinite *product*. The conjunction forgets what happened at each type $U_i$ and that's nasty. (Let's not tell anybody that in the realizability models of System F the universal quantifier *is* intersection.)  
> **username_1**: @AndrejBauer: that's fair, though sometimes it's useful to forget information... my intuition is partly based on the elimination rule of $\exists$.  
> **username_2**: You can only forget information under suitable circumstances that guarantee that you will still get away with it. For instance, in the realizability models where $\forall$ actually is $\bigcap$ we can forget information because of the amazing amount of uniformity of the realizers. If you forget information when you should not be doing it, then you'll just invalidate the laws.  

---

### Answer by username_3 on 2015-09-13. Score: 1

I suggest not to give up on the operational intuition. Operational
is primary, all semantics are derived, and are but proof techniques
for operational semantics. The key ideas are as follows.

A program $P$ uses a variable $x$ **universal-polymorphically**, provided $P$
doesn't do anything with $x$ that requires knowledge of $x$'s type. For example in the
$\lambda$-calculus the following operations could be polymorphic (whether
they are or not depends on the precise language semantics).

* forwarding, e.g. $\lambda x.x.$,
* reordering, e.g. $\lambda (x,y,z). (z,x, y)$.
* duplicating, e.g. $\lambda x.(x,x)$.
* dropping, e.g. $\lambda x.7$.

Now existential-polymophism is the exact **dual** of
universal-polymorphism: a program $P$ uses a variable $x$
**existential-polymophially**, if $P$ provides $x$ only to **contexts**
that don't require knowledge of $x$'s type. In other words, $P$ provides
$x$ only to contexts that use $x$ universal-polymorphically.

In my opinion this **beautiful symmetry**, is obscured when thinking about universal/existential polymorphism in the
$\lambda$-calculus. The reason is the
heavy reliance on the function space operator which alas is not really a
dualising operator, but something more complicated (covariant in one argument, contravariant in the other).

> **Comments:**
> **username_0**: An interesting point of view (even though I don't understand it fully :)). The idea is then to check if laws derived in such general view hold in concrete settings of type systems? And where can I find some introductory text about this?  
> **username_3**: @username_0 Most existing implementations of polymorphism don't get this quite right. Indeed existential quantification is rarely implemented directly. I'm afraid there is no introductory text describing the duality. We have explained it [here](http://users.sussex.ac.uk/~mfb21/publications/fossacs03/index.html) but it's written for a specialised audience.  

---

