如何为 Category 实例定义相等性？答案

【问题标题】：How to define equality for Category instances?如何为 Category 实例定义相等性？
【发布时间】：2012-09-16 22:54:57
【问题描述】：

为了证明例如类别法则适用于对数据类型的某些操作，如何决定如何定义相等？考虑以下类型来表示布尔表达式：

data Exp
    = ETrue
    | EFalse
    | EAnd Exp Exp
    deriving (Eq)

试图证明 Exp 形成一个具有身份 ETrue 和运算符的类别是否可行：

(<&>) = EAnd

没有重新定义 Eq 实例？使用 Eq 的默认实例，left-identity 法则打破，即：

ETrue <&> e == e

评估为假。但是，定义一个 eval 函数：

eval ETrue =  True
eval EFalse = False
eval (EAnd e1 e2) = eval e1 && eval e2

和 Eq 实例为：

instance Eq Exp where
    e1 == e2 = eval e1 == eval e2

解决了这个问题。 (==) 方面的比较是声称满足此类定律的一般要求，还是说定律适用于特定类型的相等运算符就足够了？

【问题讨论】：

您没有义务使用(==) 的默认实现作为结构相等。如果您希望它表示与某些同构的等价，那很好。但是，如果可以通过其他方式轻松区分等价但不相同的值，那么这样做可能是不好的形式。这同样适用于类型类法律中的“平等”概念。
类别在哪里？只是好奇。
@n.m 我的印象是数学意义上的Exp 与箭头<&> 和标识ETrue 形成一个类别。但是，这与 Haskell 中的 Category 类型类不符，因为它需要更高种类的实例。对于这种数据类型，证明 Monoid 定律会是更好的选择。
嗯，它是一个幺半群，也是一个类别（每个幺半群都是一个类别），但是''不是一个箭头。 '' 是箭头组合。 Exps 是箭头。
作为使用非结构相等的类型示例，请参阅惰性字节串。

标签： haskell category-theory

【解决方案1】：

平等是EVIL。你很少（如果有的话）需要结构平等，因为它太强了。您只需要 足够强 的 等价性 你在做什么。范畴论尤其如此。

在 Haskell 中，deriving Eq 将为您提供结构平等，这意味着您将经常想自己编写==//=的实现。

一个简单的例子：将有理数定义为整数对， data Rat = Integer :/ Integer。如果你使用结构相等（Haskell 是 deriving)，您将拥有(1:/2) /= (2:/4)，但作为分数1/2 == 2/4。什么你真正关心的是你的元组表示的值，而不是它们的表示。这意味着您需要一个 equivalence 来比较 reduced 分数，所以你应该实现它。

旁注：如果有人使用代码假定您已经定义了结构相等性测试，即使用== 进行检查证明替换数据子组件是合理的通过模式匹配，他们的代码可能会中断。如果这很重要，您可以隐藏构造函数以禁止模式匹配，或者定义您的拥有class（比如Equiv 与=== 和=/=）来区分这两个概念。（这对于像 Agda 或 Coq 这样的定理证明者来说最重要，在 Haskell 中很难得到实用/真实世界的代码如此错误以至于最终出现问题。）

Really Stupid(TM) 示例：假设某人想要打印很长的列表 Rats 并相信记忆 Integers 的字符串表示将节省关于二进制到十进制的转换。 Rats 有一个查找表，这样等于 Rats 永远不会被转换两次，并且有一个整数查找表。如果 (a:/b) == (c:/d)，缺少的整数条目将通过在a-c/之间复制来填充 b-d 跳过转换（哎哟！）。对于列表[ 1:/1, 2:/2, 2:/4 ]，1 获取转换然后，因为1:/1 == 2:/2，1 的字符串被复制到 2 查找条目。最终结果"1/1, 1/1, 1/4" 很烂。

【讨论】：

这是否意味着单子定律应该适用于== 的给定实现，或者如果它们在您不直接实现为@ 987654350@实例？
@VicSmith：无论您使用什么平等/等价概念，它们都应该成立。如果您使用/实施==，法律应该坚持这一点。如果您有（并且已经实施）另一个比较，请在检查法律时使用它。我想说最好不要在您的类型上定义/派生==，如果您有不同的等效概念以确保不会混淆两者，因为（如答案中所述）混合不同的概念可能会破坏逻辑。