2
$\begingroup$

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?

$\endgroup$
4
  • $\begingroup$ Have you considered types of the form $(\forall x.a) \rightarrow b$? $\endgroup$ Commented Jan 8 at 18:50
  • $\begingroup$ 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. dl.acm.org/doi/10.1145/44501.45065 $\endgroup$
    – cody
    Commented Jan 8 at 19:56
  • $\begingroup$ See the paper "Recursive types for free" for encoding of greatest fixpoints using $\exists$. homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/… $\endgroup$
    – winitzki
    Commented Apr 1 at 13:40
  • $\begingroup$ @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? cstheory.stackexchange.com/questions/54124 $\endgroup$
    – winitzki
    Commented Apr 1 at 15:37

1 Answer 1

6
$\begingroup$

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.

$\endgroup$
2
  • 1
    $\begingroup$ 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 with many message-passing parametricity properties. (Sorry for self-cite!) See also lots of subsequent work on polarised linear logic and session types. $\endgroup$ Commented Jan 9 at 10:57
  • $\begingroup$ 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 cstheory.stackexchange.com/questions/54124 $\endgroup$
    – winitzki
    Commented Apr 1 at 13:33

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.