Idris == 运算符在哪里有用？

Question

作为类型驱动编程的初学者，我很好奇 == 运算符 的用法。示例表明，证明某种类型的两个值之间的相等性是不够的，并且针对特定数据类型引入了特殊的相等性检查类型。在那种情况下，== 有什么用处？

Answer 1

你仍然需要古老的平等，因为有时你无法证明事情。有时你甚至不需要证明。考虑下一个例子：

countEquals : Eq a => a -> List a -> Nat
countEquals x = length . filter (== x)

您可能只想计算相等元素的数量以向用户显示一些统计信息。另一个例子：测试。是的，即使使用强类型系统和依赖类型，您也可能希望执行良好的旧单元测试。所以你想检查期望值，使用 (==) 运算符很方便。

我不会写出您可能需要的完整案例列表 (==)。相等运算符不足以证明，但您并不总是需要证明。

Answer 2

(==)（作为Eq接口的单一构成函数）是T到Bool类型的函数，适合等式推理。而 x = y（其中 x : T 和 y : T）又名 "intensional equality" 本身是一个类型，因此是一个命题。您可以而且经常会想要在两种不同的表达特定类型相等性的方式之间来回切换。

x == y = True 也是一个命题，通常是推理 (==) 和推理 =.

之间的中间步骤

这两种相等性之间的确切关系相当复杂，您可以阅读 https://github.com/pdorrell/learning-idris/blob/9d3454a77f6e21cd476bd17c0bfd2a8a41f382b7/finished/EqFromEquality.idr 以尝试理解它的某些方面。（需要注意的一件事是，即使归纳定义的类型将具有可决定的内涵相等性，您仍然需要经过几道工序来证明这一点，并且还要经过几道工序才能定义 Eq 的相应实现。）

一个特别方便的代码片段是这样的：

-- for rel x y, provide both the computed value, and the proposition that it is equal to the value (as a dependent pair)
has_value_dpair : (rel : t -> t -> Bool) -> (x : t) -> (y : t) -> (value: Bool ** rel x y = value)
has_value_dpair rel x y = (rel x y ** Refl)

当你有一个从 rel x y 返回的值并且你想对命题 rel x y = True 或 rel x y = False 进行推理时，你可以将它与 with 结构一起使用（并且rel 是一些函数，可能表示 x 和 y 之间的相等概念。

（在这个答案中，我假设 (==) 对应于 = 的情况，但您完全可以自由定义不对应于 [=20 的 (==) 函数=]，例如在定义 Setoid 时。所以这是使用 (==) 而不是 = 的另一个原因。）

Idris == 运算符在哪里有用？

Where is the Idris == operator useful?

idris