为什么Haskell没有更强的替代Eq？

Question

这里Set给出了不是算子的原因.它似乎归结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？".

另外,我的实例声明是垃圾(感谢@nm).我应该说:

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)

Answer 1

instance StrongEq a => Functor (Set a) where

无论在什么方面,无论是在哈斯克尔还是在数学/分类方案中,这都没有意义StrongEq.

在Haskell中,Functor需要一种类型的构造函数* -> *.箭头反映了这样一个事实:在类别理论中,仿函数是一种映射.[]和(假设的)Set是这种类型的构造函数.[a]并且Set a善良*,不能成为玩家.

在Haskell中,很难定义Set它可以被制作为a,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说确切地说)是一个算子,没有问题.

Answer 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因此您可以将其粘贴到需要排序的数据结构中,但如果排序不是真正的抽象值的总排序,则可能会出现所有类型的破坏.例如,除非文档绝对保证它,否则调用的函数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在后室使用拉斯维加斯式随机算法或相互竞争线程以从最快速度获得答案的功能甚至可以在不同时间给出不同的结果,只要它们==彼此相对即可.

tl;博士:让事物Eq成为一种向世界发表强烈声明的方式; 如果你不是那个意思,不要发表这个声明.

Answer 3

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

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)

这段代码声称不管函子fandg和函数hand 都可以工作j。它无法检查其中一个函子是否是对 具有额外约束的特殊函数，也无法检查fmap它所应用的函数之一是否会违反这些约束。

说 Set 是 Haskell 中的一个函子，就是说有一个（合法的） operation fmap :: (a -> b) -> Set a -> Set b，具有那种确切的类型。这是正是什么Functor手段。fmap :: (Eq a -> Eq b) => (a -> b) -> Set a -> Set b不是这种操作的一个例子。

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