Dan Licata drl at cs.cmu.edu
Wed Feb 13 16:31:10 EST 2008

```Hi Ryan,

On Feb13, Ryan Ingram wrote:
> However, you can express "exists" in terms of "forall":
> exists x, P(x) is equivalent to (not (forall x, not P(x)))
> that is, if it is not true for all x that P(x) does not hold, then
> there must be some x for which it does hold.
>
> The existential types extension to haskell uses this dual:
> data Number = forall a. Num a => N a
>
> means that the constructor N has type
> N :: forall a. Num a => a -> Number

Actually, the encoding of existential types doesn't use the negation
trick, which doesn't even work in intuitionistic logic.

The encoding of existentials is just currying:

Given a function of type

(A , B) -> C

we can produce a function

A -> B -> C

"exists" is a lot like pairing, and "forall" is a lot like ->.  So if
all we want is existentials to the left of an -> we can just curry them
away:

(exists a.B) -> C

becomes

forall a. B -> C

The existential type extension allows forall's to the left of the -> in
the signature of a datatype constructor, so constructors can
have existentially bound variables.

I.e.

data AnyNum where
N : forall a. Num a => a -> AnyNum

could just as well be written

data AnyNum =
N (exists a. Num a and a)

but Haskell doesn't allow the latter syntax.

-Dan
```