为什么 Haskell 没有比 Eq 更强大的替代方案？答案

【问题标题】：Why doesn't Haskell have a stronger alternative to Eq?为什么 Haskell 没有比 Eq 更强大的替代方案？
【发布时间】：2023-03-22 10:25:01
【问题描述】：

Set 不是函子的原因是here。似乎可以归结为a == b && f a /= f b 是可能的。那么，为什么 Haskell 没有标准的 Eq 替代方案，比如

class Eq a => StrongEq a where
    (===) :: a -> a -> Bool
    (/==) :: a -> a -> Bool
    x /== y = not (x === y)
    x === y = not (x /== y)

哪些情况应该遵守法律

∀a,b,f. not (a === b) || (f a === f b)
∀a. a === a
∀a,b. (a === b) == (b === a)

也许还有其他人？那么我们可以：

instance StrongEq a => Functor (Set a) where
    -- ...

还是我错过了什么？

编辑：我的问题不是“为什么会有没有Eq 实例的类型？”，就像你们中的一些人似乎已经回答的那样。恰恰相反：“为什么Eq 的实例在扩展上不相等？为什么Eq 实例太多？”，结合“如果a == b 确实暗示外延相等，为什么Set 不是Functor 的实例？”。

另外，我的实例声明是垃圾（感谢@n.m.）。我应该说：

newtype StrongSet a = StrongSet (Set a)
instance Functor StrongSet where
    fmap :: (StrongEq a, StrongEq b) => (a -> b) -> StrongSet a -> StrongSet b
    fmap (StrongSet s) = StrongSet (map s)

【问题讨论】：

我认为迈克尔的例子是无效的。 == is 应该见证“通过所有可观察的方式等效”（这并不一定要求 a == b 必须仅适用于 相同的实现；但是您可以做的任何事情“正式“与a 和b 一起做应该再次产生相同的结果。所以unAlwaysEq 不应该首先暴露）。如果您无法确保某些类型的这一点，则不应为其提供 Eq 实例。
如果你定义了一个没有意义的实例，你应该期望你编写的代码有奇怪的行为。 Set 不是函子，因为Set.map 的输出类型需要Ord 约束。实例instance Functor (Set a) where ... 甚至无效。
在 Scala 中存在 fmap 对应于 Set，它曾多次咬过我（和同事）。
对于任何有趣的类型，你的第一个属性如何才能成立？ Int 肯定不可能是 StrongEq 的实例，因为存在 f :: Int -> Int 其中 a === b && not (f a === f b)。
@JamesWood 问题总是映射一个Set，这样两个不同的元素被映射为相等；但目的是保留重复项。例如。你有一组对象，想要总结它们的成本。如果您将对象映射到它们的成本然后求和，如果您得到一组介于两者之间的成本，那么您只计算具有相同成本的对象一次。

标签： haskell functional-programming functor typeclass

【解决方案1】：

instance StrongEq a => Functor (Set a) where

无论 StrongEq 是什么意思，这在 Haskell 和宏伟的数学/分类方案中都没有意义。

在 Haskell 中，Functor 需要一个类型为 * -> * 的类型构造函数。箭头反映了在范畴论中，函子是一种映射。 [] 和（假设的）Set 就是这样的类型构造函数。 [a] 和 Set a 具有类 * 并且不能是函子。

在 Haskell 中，很难将 Set 定义为可以制成 Functor，因为无论如何都无法为某些类型合理地定义相等。例如，您无法比较 Integer->Integer 类型的两个事物。

假设有一个函数

goedel :: Integer -> Integer -> Integer
goedel x y = -- compute the result of a function with 
             -- Goedel number x, applied to y

假设您有一个值s :: Set Integer。 fmap goedel s 应该是什么样子？如何消除重复？

在您的典型集合论中，平等被神奇地定义为所有事物，包括函数，因此Set（或准确地说是Powerset）是一个函子，这没有问题。

【讨论】：

好的，我明白了第一点。我需要newtype StrongEq a => StrongSet a = StrongSet (Set a) 然后instance Functor StrongSet where ---。但是你的goedel 不会导致类型错误吗？ fmap :: (a -> b) -> f a -> f b，但其中(a -> b) = (Integer -> (Integer -> Integer)) 和f = Set，f b，即Set (Integer -> Integer) 不存在（或创建它的函数不存在）。这是设计使然。
goedel 不会导致类型错误。这是一个完美的功能。如果您尝试为instance Functor StrongSet 定义fmap，则会出现类型错误。
啊，所以函子必须能够包含任何类型。我想这是有道理的。这是范畴论函子中的标准吗？
@JamesWood，我不是范畴论者，但我对此表示怀疑。您可能会处理类似函子之类的东西，其域是 Hask 的 non-full 子类别。

【解决方案2】：

由于我不是范畴论者，我会尝试写一个更具体/实用的解释（即我能理解的）：

关键点是@leftaroundabout 在评论中所做的：

== 应该是见证“通过所有可观察的方式等效”（不一定要求 a == b 必须仅适用于相同的实现；但你可以“正式”用 a 和 b 做的任何事情都应该再次产生等效的结果。所以unAlwaysEq不应该在第一时间暴露地方）。如果你不能确保某些类型的，你不应该给它 Eq 实例。

也就是说，应该不需要你的 StrongEq，因为 Eq 应该已经是这样了。

Haskell 值通常旨在表示某种数学或“现实生活”值。很多时候，这种表示是一对一的。例如，考虑类型

data PlatonicSolid = Tetrahedron | Cube |
   Octahedron | Dodecahedron | Icosahedron

这种类型只包含每个柏拉图立体的一种表示。我们可以通过在声明中添加deriving Eq 来利用这一点，它会生成正确的实例。

然而，在许多情况下，同一个抽象值可能由多个 Haskell 值表示。例如，红黑树Node B (Node R Leaf 1 Leaf) 2 Leaf 和Node B Leaf 1 (Node R Leaf 2 Leaf) 都可以表示集合{1,2}。如果我们将deriving Eq 添加到我们的声明中，我们将获得一个Eq 的实例，它可以区分我们希望被视为相同的事物（在集合操作的实现之外）。

确保类型仅在适当的时候成为Eq（和Ord）的实例，这一点很重要！将某些东西设为Ord 的实例非常诱人，这样您就可以将其粘贴在需要排序的数据结构中，但如果排序不是真正的抽象值的total 排序，所有方式可能会发生破损。除非文档绝对保证它，例如，一个名为 sort :: Ord a => [a] -> [a] 的函数可能不仅是一个不稳定排序，甚至可能不会生成一个包含所有 Haskell 值的列表。 sort [Bad 1 "Bob", Bad 1 "James"] 可以合理地产生[Bad 1 "Bob", Bad 1 "James"]、[Bad 1 "James", Bad 1 "Bob"]、[Bad 1 "James", Bad 1 "James"] 或[Bad 1 "Bob", Bad 1 "Bob"]。所有这些都是完全合法的。一个函数在后台使用unsafePerformIO 来实现拉斯维加斯风格的随机算法或使线程相互竞争以从最快的速度获得答案，甚至可能在不同的时间给出不同的结果，只要它们是@987654343 @彼此。

tl;dr：将某物作为Eq 的实例是一种向世界做出非常强烈的声明的方式；如果您不是故意的，请不要发表这种声明。

【讨论】：

【解决方案3】：

您的第二个 Functor 实例也没有任何意义。 Set 在 Haskell 中不能成为 Functor 的最大原因是 fmap 不能有约束。发明不同的相等概念为 StrongEq 并不会改变这样一个事实，即您不能在 Set 实例中对 fmap 编写这些约束。

fmap 通常不应该有你需要的约束。例如，拥有函数的函子是非常有意义的（没有它，使用 Applicative 在函子中应用函数的整个概念就失效了），并且函数不能是 Eq 或一般的 StrongEq 的成员。

fmap 不能只对某些实例有额外的约束，因为代码如下：

fmapBoth :: (Functor f, Functor g) => (a -> b, c -> d) -> (f a, g c) -> (f b, g d)
fmapBoth (h, j) (x, y) = (fmap h x, fmap j y)

无论函数 f 和 g 以及 h 和 j 函数如何，此代码都声称可以正常工作。它无法检查其中一个函子是否是对fmap 具有额外约束的特殊函子，也无法检查其应用的某个函数是否会违反这些约束。

说 Set 是 Haskell 中的 Functor，就是说有一个（合法的）操作fmap :: (a -> b) -> Set a -> Set b，具有那个确切的类型。这正是Functor 的意思。 fmap :: (Eq a -> Eq b) => (a -> b) -> Set a -> Set b 不是此类操作的示例。

据我所知，可以使用ConstraintKinds GHC extendsion 编写一个不同的 Functor 类，该类允许对随 Functor 不同的值进行约束（而您实际需要的是 Ord约束，而不仅仅是Eq)。 This blog post 谈论这样做是为了创建一个新的 Monad 类，该类可以具有 Set 的实例。我从来没有玩过这样的代码，所以我对这种技术的存在知之甚少。它不会帮助您将 Set 移交给需要 Functor 的现有代码，但如果您愿意，您应该能够在自己的代码中使用它而不是 Functor。

【讨论】：

【解决方案4】：

StrongEq 这个概念很难。一般来说，平等是计算机科学比典型数学更加严格的地方，这使得事情变得具有挑战性。

特别是，典型的数学喜欢谈论对象，就好像它们存在于一个集合中并且可以唯一标识一样。计算机程序通常处理并不总是可计算的类型（作为一个简单的反例，告诉我与类型 data U = U (U -> U) 对应的集合是什么）。这意味着可能无法确定两个值是否可识别。

这在依赖类型语言中成为一个巨大的话题，因为类型检查需要识别相似类型，而依赖类型语言的类型可能具有任意值，因此需要一种投影相等性的方法。

因此，StrongEq 可以定义在 Haskell 的受限部分上，该部分仅包含可以确定比较是否相等的类型。我们可以将其视为具有箭头的类别作为可计算函数，然后将Set 视为从类型到该类型值集的类型的内函子。不幸的是，这些限制使我们与标准 Haskell 相去甚远，并且使定义 StrongEq 或 Functor (Set a) 不太实用。

【讨论】：