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