如何定义类别实例的相等性？

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

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

是否可行试图证明精通形式与身份为ETrue和运营商类别：

(<&>) = EAnd

不需要重新定义式实例？使用默认实例的式的左身份法符，即：

ETrue <&> e == e

评估为假。然而，限定eval函数：

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

和等式实例为：

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

修复该问题。根据（==）比较是否声称满足这些法律的一般要求，还是足以说法律适用于特定类型的平等运营商？

来源

2012-09-16 esevelos

您没有义务将'（==）'的默认实现用作结构相等。如果你想让它等同于某种同构，那很好。不过，如果可以通过其他方式轻松区分等价但不相同的值，那么这样做也许是不好的形式。这同样适用于类型法中的“平等”概念。 –

类别在哪里？只是好奇。 –

@ C.A.McCann - 谢谢，在许多情况下，甚至不可能实施适当的比较，所以我认为，至少在monad/monoid/categery定律在某些替代同构方面得到满足方面是完全错误的。 – esevelos

平等为EVIL。你很少（如果有的话）需要结构性等于, 因为它是太强。你只想要一个等效就是足够强对于你在做什么。这对于分类理论尤其如此。

在Haskell，deriving Eq会给你结构相等，这意味着你会经常想写自己实现==//=。

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

附注：如果有人使用代码假定您已经定义了一个结构平等的测试，即与==证明通过模式匹配替换数据子组件检查，他们的代码可能会断裂。如果这很重要，您可以隐藏构造函数以禁止模式匹配，或者可以定义您自己的class（例如，Equiv和===和=/=）来分隔这两个概念。（这是定理证明像阿格达或勒柯克大多是重要的，在Haskell它真的很难得到实际/真实世界的代码错到最后东西坏了。）

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

来源

2012-09-19 23:51:33 nobody

这是否意味着monad规则应该适用于'=='的给定实现，或者如果它们持有某种你没有直接作为'Eq'实例实现的类型同构，那么事情就没有问题？ –

@VicSmith：他们应该坚持你使用的任何平等/等值的概念。如果你使用/执行'=='，法律应该坚持。如果你有（并已经实施）另一个比较，那么在检查法律时使用它。如果你有不同的等价概念以确保不可能混淆这两者，最好不要在你的类型上定义/派生'=='，因为（如答案中所指出的）混合不同的概念可能会中断逻辑。 – nobody

如何定义类别实例的相等性？

回答

相关问题