为什么说类型类是存在的？

Question

根据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.

但是具有类型 class 约束的函数定义不与类型 class 实例配对。

不是 forall f, exists Functor f, ...（因为很明显不是每个类型 f 都有 Functor f 的实例，因此 exists Functor f ... 不正确）。

不是exists f and Functor f, ...（因为它适用于满足f的所有实例，而不仅仅是选择的那个）。

对我来说，它是 forall f and instances of Functor f, ...，更像是 scala 的隐式参数而不是存在类型。

并且根据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)

类型 classes 和存在类型有什么区别，为什么它们都被认为是 "existential"？

Answer 1

您引用的 wiki 是错误的，或者至少是不准确的。 class 声明不是存在命题；它不是任何类型的命题，它只是 shorthand 的定义。然后，如果你愿意，可以继续使用该定义提出一个命题，但就其本身而言，它完全不是那样的。例如，

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

重新定义。然后可以使用它写一个 non-existential、non-universal 命题，比如说，

Eq ()

我们可以 "prove" 通过写作：

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

或者可以这样写

prop_ExistsFoo :: exists a. Eq a *> a

作为一个存在命题。（Haskell 实际上没有 exists 命题前者，也没有 (*>)。认为 (*>) 是 (=>) 的对偶——就像 exists 是 forall 的对偶。所以 (=>) 是一个接受约束证据的函数，(*>) 是一个包含约束证据的元组，就像 forall 是对于接受类型的函数，而 exists 是对于包含类型的元组。）我们可以 "prove" 这个命题，例如

prop_ExistsFoo = ()

这里注意，exists元组中包含的类型是()； (*>) 元组中包含的证据是我们上面写的 Eq () 实例。我很荣幸 Haskell 在这里使类型和实例保持沉默和隐含，因此它们不会出现在可见的证明文本中。

类似地，我们可以通过写类似

的东西从Eq中提出一个不同的、普遍的命题

prop_ForallEq :: forall a. Eq a => a

这不是非平凡可证明的，或者

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

我们可以"prove"，例如，写

prop_ForallEq2 x y = not (x == y)

或许多其他方式。

但是class声明本身绝对不是一个存在命题，它没有"existential nature"，不管它应该是什么意思.与其对此感到困惑和困惑，请祝贺自己正确地将这个不正确的声明标记为令人困惑！

Answer 2

第二个引用不准确。存在性声明来自实例，而不是 class 本身。考虑以下 class：

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

虽然这是一个完全有效的声明，但不可能有任何 Chaos 的实例（如果有，to . from 会存在，这会很有趣）。例如，to...

的类型

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

... 告诉我们，给定任何类型 a，如果 a 是 Chaos 的一个实例，则有一个可以将 a 转换为任何类型的值的函数。如果 Chaos 没有实例，则该语句是空洞的，因此我们无法从中推断出任何此类函数的存在。

暂且不提 classes，这种情况与 the absurd function:

的情况非常相似

absurd :: Void -> a

这种类型表示，给定一个 Void 值，我们可以生成任何类型的值。这听起来很荒谬——但是我们记得 Void 是空类型，这意味着没有 Void 值，这一切都很好。

为了对比，我们可能会注意到，一旦我们将 Chaos 分成两个 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 ()

例如，当我们写 instance Primordial Void 时，我们声称 Void 是 Primordial 的一个实例。这意味着必须存在一个函数 conjure :: Void -> y，此时我们必须通过提供实现来支持声明。

为什么说类型类是存在的？

Why is it said that typeclasses are existential?

haskell

typeclass