Why is it said that typeclasses are existential?
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!
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.