[Haskell-cafe] Re: existential types

[Derek Elkins]

On Wed, 2008-02-13 at 16:31 -0500, Dan Licata wrote:
> 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

Or categorically: Existentials are left adjoints.  Universals are the
dual of existentials. (->) is continuous in its first argument (because
it's a right adjoint [to itself no less]) so it takes limits to limits,
but it's also contravariant so it takes limits in the opposite category
to limits or, effectively, it takes colimits to limits.  Since we know
the relevant universals exist, we have the above by continuity of right
adjoints.