<p>Universal types can be used to encode the <em>least fixed point</em>, while dually, existential types can be used to encode the <em>greatest fixed point</em>. For example, consider <span class="math-container">$F(X) = 1 + A \times X$</span>, then the least fixed point of <span class="math-container">$F$</span> is the type of lists (of <span class="math-container">$A$</span>). It is encoded by <span class="math-container">$\forall X. (F(X) \to X) \to X$</span>. Expanding this you get
<span class="math-container">$$ \begin{aligned}
\forall X. (F(X) \to X) \to X &amp;= \forall X. ((1 + A \times X) \to X) \to X \\
&amp;= \forall X. (X \times (A \to X \to X)) \to X \\
&amp;= \forall X. X \to (A \to X \to X) \to X \\
\end{aligned} $$</span>
The dual notion here is <em>potentially infinite lists</em>, encoded by <span class="math-container">$\exists X. X \times (X \to F(X))$</span>. Similarly if <span class="math-container">$F(X) = 1 + X \times X$</span> you get potentially infinite binary trees, etc.</p>
<p>Another interesting interaction is the relation between <span class="math-container">$\forall$</span> and <span class="math-container">$\exists$</span>. We have <span class="math-container">$(\exists X. F(X)) \to Y$</span> is isomorphic to <span class="math-container">$\forall X. F(X) \to Y$</span>, and with parametricity there are more interesting isomorphisms.</p>

CC BY-SA 4.0
2024-01-09T10:57:12.897Z
The duality between $\forall$  and $\exists$ becomes even more clear when you generalise from functions to message passing. Then it becomes
a clear input/output duality, see [Genericity and the $\pi$-calculus](https://users.sussex.ac.uk/~mfb21/publications/fossacs03/fossacs03.pdf)
with many message-passing parametricity properties. (Sorry for self-cite!) See also lots of subsequent work on polarised linear logic and session types.
Martin Berger
CC BY-SA 4.0
2024-04-01T13:33:13.913Z
You say "with parametricity there are more interesting isomorphisms". What are those? Where can I read about them? Right now I am having trouble proving an equivalence between existential types encoded as universal types, and straight universal types, and I just posted that as a question https://cstheory.stackexchange.com/questions/54124
winitzki
CC BY-SA 4.0
2024-01-09T07:57:04.497Z
2024-01-09T07:57:04.497Z
Trebor
<p>It is well known that simply typed lambda calculus becomes much more expressive if you allow <strong>universal types</strong>, as in Girards system F. Thus, for example, you can encode the booleans as forall a. a -&gt; a -&gt; a and the integers as forall a. a -&gt; (a-&gt; a) -&gt; a and furthermore, you can encode all logical operators and primitive recursive functions as well.</p>
<p>What happens if you use the dual concept, that of <strong>existential types</strong>? Can you encode any of the above structures? (It doesnt seem so) Can you encode <em>any</em> other interesting structure?</p>

CC BY-SA 4.0
2024-01-08T18:50:14.940Z
Have you considered types of the form $(\forall x.a) \rightarrow b$?
Martin Berger
CC BY-SA 4.0
2024-01-08T19:56:52.630Z
It is well known that existential types help one encode the concept of *encapsulation*, e.g. $\exists X. (X \rightarrow 1)\times(\mathrm{Int}\rightarrow X)$ could encode an `Int` container with an "increment" operation. See e.g. https://dl.acm.org/doi/10.1145/44501.45065
cody
CC BY-SA 4.0
2024-04-01T13:40:59.883Z
See the paper "Recursive types for free" for encoding of greatest fixpoints using $\exists$. https://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt
winitzki
CC BY-SA 4.0
2024-04-01T15:37:22.957Z
@MartinBerger I'm having trouble working with types of the form $(\forall x. a)\to b$.  Not sure how to use parametricity arguments in that case. I just posted a question where I get stuck with that sort of type expression. Maybe you could help? https://cstheory.stackexchange.com/questions/54124
winitzki
<lo.logic><type-theory><type-systems>
Power of existential types
manu fava
# Power of existential types

(Asked by: username_0 on 2024-01-08)

It is well known that simply typed lambda calculus becomes much more expressive if you allow **universal types**, as in Girards system F. Thus, for example, you can encode the booleans as forall a. a -> a -> a and the integers as forall a. a -> (a-> a) -> a and furthermore, you can encode all logical operators and primitive recursive functions as well.

What happens if you use the dual concept, that of **existential types**? Can you encode any of the above structures? (It doesnt seem so) Can you encode *any* other interesting structure?

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

> **Comments:**
> **username_1**: Have you considered types of the form $(\forall x.a) \rightarrow b$?  
> **username_2**: It is well known that existential types help one encode the concept of *encapsulation*, e.g. $\exists X. (X \rightarrow 1)\times(\mathrm{Int}\rightarrow X)$ could encode an `Int` container with an "increment" operation. See e.g. https://dl.acm.org/doi/10.1145/44501.45065  
> **username_3**: See the paper "Recursive types for free" for encoding of greatest fixpoints using $\exists$. https://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt  
> **username_3**: @MartinBerger I'm having trouble working with types of the form $(\forall x. a)\to b$.  Not sure how to use parametricity arguments in that case. I just posted a question where I get stuck with that sort of type expression. Maybe you could help? https://cstheory.stackexchange.com/questions/54124  

---

## 1 answers

### Answer by username_4 on 2024-01-09. Score: 6 | Accepted answer

Universal types can be used to encode the *least fixed point*, while dually, existential types can be used to encode the *greatest fixed point*. For example, consider $F(X) = 1 + A \times X$, then the least fixed point of $F$ is the type of lists (of $A$). It is encoded by $\forall X. (F(X) \to X) \to X$. Expanding this you get
$$ \begin{aligned}
\forall X. (F(X) \to X) \to X &= \forall X. ((1 + A \times X) \to X) \to X \\
&= \forall X. (X \times (A \to X \to X)) \to X \\
&= \forall X. X \to (A \to X \to X) \to X \\
\end{aligned} $$
The dual notion here is *potentially infinite lists*, encoded by $\exists X. X \times (X \to F(X))$. Similarly if $F(X) = 1 + X \times X$ you get potentially infinite binary trees, etc.

Another interesting interaction is the relation between $\forall$ and $\exists$. We have $(\exists X. F(X)) \to Y$ is isomorphic to $\forall X. F(X) \to Y$, and with parametricity there are more interesting isomorphisms.

> **Comments:**
> **username_1**: The duality between $\forall$  and $\exists$ becomes even more clear when you generalise from functions to message passing. Then it becomes a clear input/output duality, see [Genericity and the $\pi$-calculus](https://users.sussex.ac.uk/~mfb21/publications/fossacs03/fossacs03.pdf) with many message-passing parametricity properties. (Sorry for self-cite!) See also lots of subsequent work on polarised linear logic and session types.  
> **username_3**: You say "with parametricity there are more interesting isomorphisms". What are those? Where can I read about them? Right now I am having trouble proving an equivalence between existential types encoded as universal types, and straight universal types, and I just posted that as a question https://cstheory.stackexchange.com/questions/54124  

---

