如何定义类别实例的相等性？ [英] How to define equality for Category instances?

问题描述

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

 数据Exp 
 = ETrue 
 | EFalse 
 | EAnd Exp Exp 
 deriving（Eq）
  

是否可行试图证明 Exp 形成一个带有标识 ETrue 和运算符的类别：

 （<& >）= EAnd 
  

没有重新定义 Eq 实例？使用 Eq 的默认实例，左身份违反法则，即：

  ETrue<&> e == e 
  

评估为 False 。然而，定义一个 eval函数：

$ b

  eval ETrue = True 
 eval EFalse = False 
 eval（EAnd e1 e2）= eval e1&& eval e2 
  

和 Eq 实例：

instance Eq Exp其中
e1 == e2 = eval e1 == eval e2

解决了这个问题。比较（==）是声称满足这些法律的一般要求，还是足以说法律适用于特定类型的平等运营商？

解决方案

平等是 EVIL 。 您很少（如果曾经）需要结构性相等，
因为太强大。你只需要一个等价足够强大的
你在做什么。这对于类别理论尤其如此。在Haskell中，派生Eq 会给你结构上的相等性，这意味着你
经常要编写自己的 == / / = 。

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

注意：如果使用代码的人假定你已经定义了一个结构性的
相等性测试，即用 == 组件
通过模式匹配，它们的代码可能会中断。如果这很重要，
可以隐藏构造函数以禁止模式匹配，或者可以定义您的
自己的 class （比如 Equiv 与 === 和 = / = ）来分离两个概念。 （这个
对于像Agda或Coq这样的定理证明者来说是非常重要的，在Haskell中，真正的
很难让实际/现实世界的代码错误到最终出现问题。）

真正的Stupid（TM）例子：假设那个人想要打印一个巨大的
Rat s的长列表并且相信记忆字符串表示 Integer s可以节省
的二进制到十进制转换。有一个查找表 Rat s，这样等于
Rat s将永远不会被转换两次，并且有一个整数查找表。如果
（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已被冻结。

In order to prove that for instance the Category laws hold for some operations on a data type, how do one decide how to define equality? Considering the following type for representing boolean expressions:

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

Is it feasible trying to prove that Exp forms a Category with identity ETrue and operator:

(<&>) = EAnd

without redefining the Eq instance? Using the default instance of Eq the left-identity law breaks, i.e:

ETrue <&> e == e

evaluates to False. However, defining an eval function:

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

and the Eq instance as:

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

fixes the problem. Is comparison in terms of (==) a general requirement for claiming to satisfy such laws, or is it sufficient to say that the laws hold for a particular type of equality operator?

解决方案

Equality is EVIL. You rarely (if ever) need structural equality, because it is too strong. You only want an equivalence that is strong enough for what you're doing. This is particularly true for category theory.

In Haskell, deriving Eq will give you structural equality, which means that you'll often want to write your own implementation of == / /=.

A simple example: Define rational number as pairs of integers, data Rat = Integer :/ Integer. If you use structural equality (what Haskell is deriving), you'll have (1:/2) /= (2:/4), but as a fraction 1/2 == 2/4. What you really care about is the value that your tuples denote, not their representation. This means you'll need an equivalence that compares reduced fractions, so you should implement that instead.

Side note: If someone using the code assumes that you've defined a structural equality test, i.e. that checking with == justifies replacing data sub-components through pattern matching, their code may break. If that is of importance, you may hide the constructors to disallow pattern matching, or maybe define your own class (say, Equiv with === and =/=) to separate both concepts. (This is mostly important for theorem provers like Agda or Coq, in Haskell it's really hard to get practical/real-world code so wrong that finally something breaks.)

Really Stupid(TM) example: Let's say that person wants to print long lists of huge Rats and believes memoizing the string representations of the Integers will save on binary-to-decimal conversion. There's a lookup table for Rats, such that equal Rats will never be converted twice, and there's a lookup table for integers. If (a:/b) == (c:/d), missing integer entries will be filled by copying between a-c / b-d to skip conversion (ouch!). For the list [ 1:/1, 2:/2, 2:/4 ], 1 gets converted and then, because 1:/1 == 2:/2, the string for 1 gets copied into the 2 lookup entry. The final result "1/1, 1/1, 1/4" is borked.

这篇关于如何定义类别实例的相等性？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！