10

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

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

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

(<&>) = EAnd

没有重新定义Eq实例？使用Eq的默认实例，左恒等式违反了，即：

ETrue <&> e == e

评估为False。但是，定义一个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

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

4

1 回答 1

8

平等是邪恶的。 你很少（如果有的话）需要结构平等，因为它太强大了。你只想要一个对你正在做的事情足够强大的等价物。对于范畴论尤其如此。

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

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

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

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

于 2012-09-19T23:51:33.417 回答