6

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

存在类型的值，如 ∃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（该类对此有两种不同的证明，具有名称==和/=）。这个命题具有存在性质（不要与存在类型混淆）

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

4

2 回答 2

8

您引用的维基是错误的，或者至少是不精确的。类声明不是存在命题；它不是任何形式的命题，它只是简写的定义。然后，如果您愿意，可以继续使用该定义提出命题，但就其本身而言，并非如此。例如，

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

做出新的定义。然后可以用它写一个不存在的、非普遍的命题，比如说，

Eq ()

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

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

或者可以写

prop_ExistsFoo :: exists a. Eq a *> a

作为一个存在命题。（Haskell 实际上并没有exists命题前者，也没有(*>)。认为是(*>)对偶的(=>)——就像对exists偶一样forall。所以哪里(=>)是一个接受约束证据的函数，(*>)是一个包含约束证据的元组，就像forallis 用于接受类型的函数，而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)

或以许多其他方式。

但是类声明本身绝对不是一个存在命题，它不具有“存在性”，无论它应该是什么意思。与其对此感到困惑和困惑，请祝贺自己正确地将这个错误的声明标记为令人困惑！

于 2019-07-01T13:37:09.933 回答
2

第二个引用不准确。存在主义主张伴随着实例，而不是类本身。考虑以下类：

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，则有一个函数可以将 aa转换为任何类型的值。如果Chaos没有实例，则该陈述是空洞的，因此我们无法从中推断出任何此类函数的存在。

暂时将类放在一边，这种情况与我们使用函数的absurd情况非常相似：

absurd :: Void -> a

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

为了对比，我们可能会注意到，一旦我们Chaos分成两个类，实例就成为可能：

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 ()

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

于 2019-07-01T22:13:24.940 回答