标准的 Haskell 类型类应该遵守哪些法律？答案

【问题标题】：What laws are the standard Haskell type classes expected to uphold?标准的 Haskell 类型类应该遵守哪些法律？
【发布时间】：2013-01-29 11:04:01
【问题描述】：

众所周知，Monad 实例应该遵循 Monad 定律。 Functor 实例应该遵循函子定律可能不太为人所知。不过，我对编写优化 fmap id == id 的 GHC 重写规则感到相当有信心。

还有哪些其他标准类有隐含的规律？ (==) 必须是真正的等价关系吗？ Ord 一定要形成偏序吗？总订单？我们至少可以假设它是传递的吗？反对称？

Haskell 2010 报告中似乎没有指定最后几个，我也没有信心编写重写规则来利用它们。但是，是否有任何通用库可以做到？一个实例的病态到什么程度可以自信地写作？

最后，假设这样一个实例的病态程度是有界限的，那么每个类型类实例必须遵守的法律是否有一个标准、全面的资源？

举个例子，我要定义多少麻烦

newtype Doh = Doh Bool
instance Eq Doh where a == (Doh b) = b

仅仅是难以理解还是编译器会在任何地方错误地优化？

【问题讨论】：

请注意，Ord、Num 可能会提出相当多听起来合理的法律（包括现有代码默认假设的法律），并且相关类将被 @ 的实例违反987654331@ 和Double。例如，使用 NaN 作为键会破坏 Data.Map 中的查找，并且精度问题意味着浮点加法不具有关联性。
@C.A.McCann 这只是意味着前奏有它不应该的实例！ Float 和 Double 不应是 Eq 的成员
@PhilipJF：一方面，我同意。但是他们的Num 实例稍好一些，并且按照这一论点得出其逻辑结论会导致删除所有使浮点类型实际有用的实例。顺便说一句，I gave a demonstration of how broken their Ord instance is in an old post.
@C.A.McCann 我可以接受这些实例，只要这些类型仅限于特殊的“性能”导向模块。为什么Prelude 中有浮点类型？如果你真的需要一个浮点数（而不是一个比率或一个建设性的实数），你可能知道你在做什么。
可能值得注意的是，在标准 ML 中，reals are not equality types。因此，至少另一种语言更注重正确性而不是实用性。 :)

【解决方案1】：

Haskell report 提及以下法律：

这就是我能找到的。具体来说，关于 Eq (6.3.1) 的部分没有提到任何规律，下一个关于 Ord 的部分也没有提到。

【讨论】：

【解决方案2】：

并非所有标准实例都支持我对法律“应该是”的看法，但我认为

许多代码会假定这些“法则”成立，即使它们不成立。这不是 Haskell 特定的问题，早期的 C 允许编译器根据代数定律重新排序算术，并且大多数编译器可以选择重新启用这种优化，即使它们不受当前标准的允许并且可能会改变您的程序结果。

【讨论】：

我基本上同意你的看法，但据我所知，如果违反这些定义，一切都会变得糟糕。这就是我想知道的核心——我到底错在哪里？定义一个非自反的 Eq 实例不仅“具有挑战性”，而且实际上还被优化为不正确？
@tel 我怀疑“优化不正确”，但肯定“使许多函数产生不可预测的结果”
是的，在我看来，“硬”失败是指重写规则把你弄得一团糟，而“软”失败是指你违背了整个语言中的主要假设，这真的让人很困惑。两者都不好，但有一个更糟。典型的例子可能是Eq Double。
@tel 不仅会让人感到困惑。某些函数会给出不正确的结果。考虑 Map Float a（其中 Float 可能违反排序假设）或 sortBy 和 nubBy 的行为，其类型违反排序/相等假设。你会得到不正确的行为。我认为这是一个严重的失败，尽管它与编译器的行为无关。
身份依赖于一些全局状态——我的 Agda 头脑中说这意味着 Eq 使用全局状态级证明 refl :: Eq x x。

【解决方案3】：

过去，违反 Ix 定律可以让你做任何事情。这些天我认为他们已经解决了这个问题。更多信息在这里：Does anyone know (or remember) how breaking class laws could cause problems in GHC?

【讨论】：