类型类定律是在什么平等概念下编写的？

Under what notion of equality are typeclass laws written?

提问人：Quelklef 提问时间：2/25/2022 最后编辑：Quelklef 更新时间：2/27/2022 访问量：296

问：

Haskell类型类通常带有定律;例如，实例应观察到 .Monoidx <> mempty = mempty <> x = x

类型类定律通常用单等号（）而不是双等号（）来编写。这表明类型类法律中使用的相等概念不是 （这是有道理的，因为不是===EqEqMonoid)

四处搜索，我找不到任何关于类型类法律含义的权威声明。例如：=

  • Haskell 2010 报告甚至没有包含“法律”一词
  • 与其他 Haskell 用户交谈时，大多数人似乎认为这通常意味着扩展相等或替换，但从根本上依赖于上下文。没有人为这一说法提供任何权威来源。=
  • Haskell wiki 上关于单子定律的文章指出这是扩展的，但同样未能提供来源，我无法找到任何联系相关编辑作者的方法。=

那么问题来了：类型类法则的语义是否有任何权威的来源或标准？如果是这样，它是什么？此外，是否有示例中的预期含义特别具有异国情调？==

（顺便说一句，延伸治疗可能会变得棘手。例如，有一个实例，但并不真正清楚值的扩展相等性是什么样子的。=Monoid (IO a)IO

Haskell 等式

评论

5赞 Koz Ross 2/25/2022
据我一直以来的理解，法律指的是替代，而不是平等。所以说“我们总是可以替代，反之亦然”。这也恰好是 Typeclassopedia 对它的看法。=lhs = rhslhsrhs
0赞 Quelklef 2/26/2022
@KozRoss FWIW，我相信我和其他人在这种情况下使用“扩展平等”和“替代”本质上是相同的

答：

3赞 comingstorm 2/25/2022 #1

类型类定律不是 Haskell 语言的一部分，因此它们不受与语言本身相同的语言理论语义分析的影响。

相反，这些定律通常以非正式的数学符号形式呈现。大多数演示文稿不需要更详细的数学阐述，因此它们不提供。

评论

0赞 Quelklef 2/26/2022
> Typeclass 法则不是 Haskell 语言的一部分 这似乎是迄今为止最有力的迹象。如果法律不是语言的一部分，那么就必须由其他实体（如GHC或Hackage）给出定义，这两者似乎都不合适。=
8赞 Daniel Wagner 2/25/2022 #2

我怀疑大多数人习惯于“道德平等”，因为来自快速和松散的推理是道德正确的，你可以将其视为延伸到定义性的平等。=

但这里没有硬性规定。有很多图书馆，很多作者，如果你选择任何两个作者，他们可能有一些他们不同意的小细节。=

评论

0赞 dfeuer 2/26/2022
快速而松散的推理有时在道德上是正确的。我不认为懒惰之类的东西是合法的单子。他们只是......有时很方便。State
0赞 Daniel Wagner 2/26/2022
@dfeuer 你能稍微解释一下吗？这是怎么回事，这与道德正确性有什么关系？State
0赞 dfeuer 2/26/2022
@DanielWagner、.是的，从论文的意义上讲，它是“道德正确的”，但它严重破坏了对性能的推理，以至于我认为它不是真正的单子。每当我使用它的实例时，我都必须做很多临时推理。x <$ undefined = x
0赞 Daniel Wagner 2/26/2022
@dfeuer 如果我们选择一种更敏锐的平等感，会违反什么单子定律（假定的纠正）？x <$ undefined = pure x
0赞 md2perpe 2/27/2022 #3

我同意即将到来的风暴，即这些定律的平等是数学语言的平等。但我也要说，这是在运营商的尊重。==

为什么？因为应该实现数学相等。==

例如，查看分数（有理数）。它们可以实现为具有一些规则的整数对。该对表示分数。如果 ，则对 和 表示相同的有理数。然后说这两个对是等价的，我们谈论等价关系。在数学中，我们让有理数成为该等价下对的等价类。在编程中，我们定义运算符来判断两对是否相等，即它们是否代表相同的分数。(a, b)a/b(a, b)(c, d)a*d == b*c==

上一个：在Haskell中使用函数作为字段从数据类型派生Eq时出现的问题

下一个：：~： 和 ：~~： equalities 和有什么不一样？