Why is it said that typeclasses are existential?

Question

According to this link describing existential types:

A value of an existential type like ∃x. F(x) is a pair containing some type x and a value of the type F(x). Whereas a value of a polymorphic type like ∀x. F(x) is a function that takes some type x and produces a value of type F(x). In both cases, the type closes over some type constructor F.

But a function definition with type class constraints doesn't pair with the type class instance.

It's not forall f, exists Functor f, ... (because it's obvious not every type f has instance of Functor f, hence exists Functor f ... not true).

It's not exists f and Functor f, ... (because it's applicable to all instances of satisfied f, not only the chosen one).

To me, it's forall f and instances of Functor f, ..., more like to scala's implicit arguments rather than existential types.

And according to this link describing type classes:

[The class declaration for Eq] means, logically, there is a type a for which the type a -> a -> Bool is inhabited, or, from a it can be proved that a -> a -> Bool (the class promises two different proofs for this, having names == and /=). This proposition is of existential nature (not to be confused with existential type)

What's the difference between type classes and existential types, and why are they both considered "existential"?

Answer 1

The wiki you quote is wrong, or at least being imprecise. A class declaration is not an existential proposition; it is not a proposition of any kind, it is merely a definition of a shorthand. One could then move on to making a proposition using that definition if you wanted, but on its own it's nothing like that. For example,

class Eq a where (==) :: a -> a -> Bool

makes a new definition. One could then write a non-existential, non-universal proposition using it, say,

Eq ()

which we could "prove" by writing:

instance Eq () where () == () = True

Or one could write

prop_ExistsFoo :: exists a. Eq a *> a

as an existential proposition. (Haskell doesn't actually have the exists proposition former, nor (*>). Think of (*>) as dual to (=>) -- just like exists is dual to forall. So where (=>) is a function which takes evidence of a constraint, (*>) is a tuple that contains evidence of a constraint, just like forall is for a function that takes a type while exists is for a tuple that contains a type.) We could "prove" this proposition by, e.g.

prop_ExistsFoo = ()

Note here that the type contained in the exists tuple is (); the evidence contained in the (*>) tuple is the Eq () instance we wrote above. I have honored Haskell's tendency to make types and instances silent and implicit here, so they don't appear in the visible proof text.

Similarly, we could make a different, universal proposition out of Eq by writing something like

prop_ForallEq :: forall a. Eq a => a

which is not nontrivially provable, or

prop_ForallEq2 :: forall a. Eq a => a -> a -> Bool

which we could "prove", for example, by writing

prop_ForallEq2 x y = not (x == y)

or in many other ways.

But the class declaration in itself is definitely not an existential proposition, and it doesn't have "existential nature", whatever that is supposed to mean. Instead of getting hung up and confused on that, please congratulate yourself for correctly labeling this incorrect claim as confusing!

Answer 2

The second quote is imprecise. The existential claim comes with the instances, not with the class itself. Consider the following class:

class Chaos a where
    to :: a -> y
    from :: x -> a

While this is a perfectly valid declaration, there can't possibly be any instances of Chaos (it there were, to . from would exist, which would be quite amusing). The type of, say, to...

GHCi> :t to
to :: Chaos a => a -> y

... tells us that, given any type a, if a is an instance of Chaos, there is a function which can turn an a into a value of any type whatsoever. If Chaos has no instances, that statement is vacuously true, so we can't infer the existence of any such function from it.

Putting classes aside for a moment, this situation is rather similar to what we have with the absurd function:

absurd :: Void -> a

This type says that, given a Void value, we can produce a value of any type whatsoever. That sounds, well, absurd -- but then we remember that Void is the empty type, which means there are no Void values, and it's all good.

For the sake of contrast, we might note that instances become possible once we break Chaos apart in two classes:

class Primordial a where
    conjure :: a -> y

class Doom a where
    destroy :: x -> a


instance Primordial Void where
    conjure = absurd

instance Doom () where
    destroy = const ()

When we, for example, write instance Primordial Void, we are claiming that Void is an instance of Primordial. That implies there must exist a function conjure :: Void -> y, at which point we must back up the claim by supplying an implementation.