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

Question

根据此链接描述存在类型：

存在类型的值，例如？x。F（x）是一对包含x类型和F（x）类型值的对。而一个多态类型的值，如？x。F（x）是采用某种x类型并产生F（x）类型值的函数。在这两种情况下，类型都在某个类型构造函数F上关闭。

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

并非如此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的隐式参数，而不是存在的类型。

并根据此链接描述类型类：

[ Eq从逻辑上讲，[类的声明]表示一个类型a a -> a -> Bool居住于该类型，或者从a可以证明a -> a -> Bool（该类为此提供了两个不同的证明，分别是name ==和/=）。该命题具有存在性（不要与存在性类型混淆）

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

Answer 1

您引用的Wiki是错误的，或者至少是不精确的。类声明不是一个存在命题。它不是任何形式的命题，而只是速记的定义。然后，如果您愿意的话，可以继续使用该定义提出一个建议，但它本身并非如此。例如，

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

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

Eq ()

我们可以这样写：

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

或者一个人可以写

prop_ExistsFoo :: exists a. Eq a *> a

作为存在命题。（Haskell实际上没有exists命题前体，也没有(*>)。被认为是(*>)对偶的(=>)-就像对偶的对exists偶一样forall。所以一个包含(=>)约束证据的函数在哪里是(*>)包含约束证据的元组，就像forall是针对具有类型的函数，而exists针对包含类型的元组。）我们可以通过例如“证明”该命题

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)

或其他许多方式。

但是，类声明本身绝对不是一个存在命题，并且它不具有“存在性”，无论这意味着什么。不要为这个挂断电话而感到困惑，而是祝贺您自己正确地将此错误标签标记为令人困惑！