Universal and existential types 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:


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?
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"?
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) &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".)

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$.