[Haskell-cafe] Re: existential types

[Dan Licata]

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