8
$\begingroup$

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"?

$\endgroup$
  • $\begingroup$ There's a typo in your equation (*): it should be $\forall Y$ rather than $\forall y$. $\endgroup$ – cody Sep 12 '15 at 22:15
  • $\begingroup$ Also, in your last equation: $y$ may not appear in $T$! $\endgroup$ – cody Sep 12 '15 at 22:39
8
$\begingroup$

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

$\endgroup$
  • $\begingroup$ Andrej, you are as fast as lightning! $\endgroup$ – cody Sep 12 '15 at 22:37
  • $\begingroup$ 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 $(*)$? $\endgroup$ – socumbersome Sep 13 '15 at 11:11
  • 3
    $\begingroup$ 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 makes sure that all elements of the cartesian product are nicely behaved and recovers the isomorphism. $\endgroup$ – Andrej Bauer Sep 13 '15 at 19:46
  • $\begingroup$ @AndrejBauer is the underlying system impredicative? And in case of a positive answer does the isomorphism hold for predicative systems? $\endgroup$ – Giorgio Mossa Jan 26 at 20:36
  • $\begingroup$ @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). $\endgroup$ – Andrej Bauer Jan 26 at 22:50
3
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ 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.) $\endgroup$ – Andrej Bauer Sep 12 '15 at 22:41
  • $\begingroup$ @AndrejBauer: that's fair, though sometimes it's useful to forget information... my intuition is partly based on the elimination rule of $\exists$. $\endgroup$ – cody Sep 14 '15 at 13:52
  • $\begingroup$ 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. $\endgroup$ – Andrej Bauer Sep 14 '15 at 15:27
1
$\begingroup$

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

$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – socumbersome Sep 13 '15 at 16:14
  • $\begingroup$ @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 but it's written for a specialised audience. $\endgroup$ – Martin Berger Sep 14 '15 at 8:48

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.