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

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.

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

这不是forall f, exists Functor f, ... (因为很明显不是每个类型 f 都有仿函数 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)

类型类和存在类型之间有什么区别，为什么它们都被认为是“存在的”？

Answer 1

您引用的维基是错误的，或者至少是不精确的。类声明不是一个存在命题；而是一个命题。它不是任何类型的命题，而只是速记的定义。如果你愿意的话，人们可以继续使用该定义提出一个命题，但就其本身而言，情况并非如此。例如，

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

做出了新的定义。然后，人们可以使用它写出一个不存在的、非普遍的命题，例如，

Eq ()

我们可以通过写来“证明”:

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

或者可以写

prop_ExistsFoo :: exists a. Eq a *> a

作为一个存在主义命题。 (Haskell 实际上没有 exists 命题前者，也没有 (*>)。将 (*>) 视为与 (=>) -- 就像 exists 与 forall 是对偶一样。所以其中 (=>) 是一个函数，接受约束的证据，(*>) 是一个包含约束证据的元组，就像 forall 是一个在 存在时接受类型的函数 用于包含类型的元组。)我们可以通过以下方式“证明”这个命题:

prop_ExistsFoo = ()

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

类似地，我们可以通过编写类似的内容，从 Eq 中提出一个不同的、通用的命题

prop_ForallEq :: forall a. Eq a => a

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

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

我们可以“证明”，例如，通过写作

prop_ForallEq2 x y = not (x == y)

或者以许多其他方式。

但是类声明本身绝对不是一个存在命题，并且它不具有“存在性质”，无论它的含义是什么。不要对此感到困惑和困惑，请祝贺自己正确地将这个不正确的主张标记为令人困惑!