Why is it said that typeclasses are existential?

6
votes

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"?

2
haskelltypeclass
Eh? Type classes are not considered existentials. What makes you think they are? Nothing you quoted implies anything like that to me. - Daniel Wagner
@DanielWagner I'm trying to understand the sentence in the second link: "This proposition is of existential nature", for what is that "existential nature". - Jiaming Lu
I think it's that eg Eq A means "there exists a function (==) :: A -> A -> Bool" - luqui
@JiamingLu It doesn't work like an existential, it works more like "forall a. when Eq a, then this function exists for a and has type a -> a". - Cubic
That part of the wiki looks simply wrong to me, or -at best- quite misleading. A declaration class C a where ... does not imply that there is a type a for which we can instantiate the class, inhabiting the methods. It is using the word "existential" quite liberally. It is similar to saying that f :: (Int -> Bool) -> Char assumes that "it exists some function Int->Bool" before generating a Char. I would ignore that sentence. - chi

2 Answers

8
votes

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!

2
votes

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.