如何定义Category实例的相等性？

Question

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

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

尝试证明Exp与身份ETrue和运算符形成一个类别是否可行:

(<&>) = EAnd

没有重新定义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

解决了这个问题.是否(==)对声称满足此类法律的一般要求进行比较,或者是否足以说法律适用于特定类型的平等运营商？

Answer 1

平等是邪恶的. 你很少(如果有的话)需要结构平等,因为它太强大了.您只需要一个等价是足够强大的你在做什么.类别理论尤其如此.

在Haskell中,deriving Eq会给你结构上的平等,这意味着你经常想要自己编写==/ 的实现/=.

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

旁注:如果使用代码的人假定您已经定义了结构相等性测试,即==通过模式匹配替换数据子组件进行检查,则其代码可能会中断.如果这很重要,您可以隐藏构造函数以禁止模式匹配,或者可以定义自己的class(例如,Equivwith ===和=/=)来分隔这两个概念.(这对于像Agda或Coq这样的定理证明来说非常重要,在Haskell中很难得到实际/现实世界的代码,所以最终会出现问题.)

Really Stupid(TM)示例:假设有人想要打印大型Rats的长列表 并且认为记住s的字符串表示Integer将节省二进制到十进制的转换.有一个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"是borked.