[Haskell-cafe] Re: existential types

[Ryan Ingram]

The name "existential types" comes from the logical connective
"exists", which is the dual of "for all".

For example, given some property P of objects of type T, you can say
forall x : T.  P(x)  -- means that P holds for all things of type x
or
exists x : T. P(x) -- means that there is some x for which P holds.

For example, take P(x) to be "x is an integer".

Then:
forall x : Int, P(x) -- valid, all objects of type Int are integers
forall x : Float, P(x) -- not valid
exists x : Float, P(x) -- valid, for example, 1.0 :: Float is an integer

In Haskell, forall is only used for kinds, such as *, the type of
types, and * -> *, the kind of type constructor used for monads &
lists (among other things).

A couple of examples:

(+) :: forall a. Num a => a -> a -> a
means
forall a : *, Num a implies (+) has type (a -> a -> a)

return False :: forall a. Monad m => m Bool
means
forall m : * -> *, Monad m implies that (return False) has type (m Bool).

Similarily, you might want to say (note: this is not valid haskell)
[0 :: Int, 2 :: Double] :: [ t such that there exists a Num instance for t ],

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

Consider this function:
isZero (N n) = (n == 0)

You have a Number and you are pattern matching on N, so what do you
know about the type of n?

Well, you know that N was called with an object of some type a, and
that Num a holds.
That is: exists a : *, Num a & type(n) == a

You can now express that list:
[ N (0 :: Int), N (2 :: Double) ] :: [ Number ]
and use it like any other list:
map isZero [ N (0 :: Int), N (2 :: Double) ] :: [Bool]

  -- ryan

On 2/13/08, Simeon Mattes <simeon.mattes at gmail.com> wrote:
> The help of all was very useful. But since Jake gave me an example I prefer to
> follow this up.
>
> Although I 'm not so familiar generally with datatypes I have understood you. It
> seems in this example that with existential types we can put in the same list
> different types although generally this is not allowed. I have tried to write
> this example with the ghc compiler 6.8.2 but there was an error
>
> pare error in data/newtype declaration.
>
>
> I have also tried to find the etymology of the word existential, since some
> times somebody can easily find a better answer, but I can't figure out why this
> is so. (really why "existential" types?). Maybe a completed example would be
> more helpful.
>
> existence Look up existence at Dictionary.com c.1384, from O.Fr. existence, from
> L.L. existentem "existent," prp. of L. existere "stand forth, appear," and, as a
> secondary meaning, "exist;" from ex- "forth" + sistere "cause to stand" (see
> assist). Existential as a term in logic is from 1819. Existentialism is 1941
> from Ger. Existentialismus (1919), ult. from Dan. writer Søren Kierkegaard
> (1813-55), who wrote (1846) of Existents-Forhold "condition of existence,"
> existentielle Pathos, etc.
>
> (I hope this way of questioning is not so strange)
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>