[Haskell-cafe] Re: existential types
drl at cs.cmu.edu
Wed Feb 13 16:31:10 EST 2008
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
(exists a.B) -> C
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.
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.
More information about the Haskell-Cafe