haskell - 为什么所有 Haskell 类型类都有规律？

Question

Typeclassopedia中的所有类型类都有相关的规律，例如某些运算符的结合性或交换性。“法则”的定义似乎是一种无法在类型系统中表达的约束。我当然理解你为什么想要拥有 monad 法则，但是有一个根本原因为什么可以在类型系统中完全表达的类型类毫无意义吗？

Answer 1

你会注意到几乎所有的定律都是代数定律。它们可以通过类型系统通过一些扩展来表达，但是证明表达起来会很麻烦。所以你有未经检查的法律，潜在的实施可能会破坏它们。为什么这样好？

原因是 Haskell 中使用的设计模式是由数学结构驱动的（并且在大多数情况下是镜像的），通常来自抽象代数。虽然大多数其他语言对某些特性（如安全性、性能和语义）都有直观的概念，但我们 Haskell 程序员更喜欢建立一个正式的概念。这样做的好处是：一旦你的类型和函数遵守安全法则，它们在底层代数结构的意义上是安全的。它们被证明是安全的。

以函子为例。Haskell 函子有以下两条定律：

fmap f . fmap g = fmap (f . g)
fmap id         = id

首先这很重要：Haskell 中的函数是不透明的。你不能检查、比较或其他任何东西。虽然这在 Haskell 中听起来像是一件坏事，但实际上是一件非常好的事情。该fmap函数无法检查您传递给它的函数。特别是它无法检查您是否通过了身份功能或您是否通过了组合。简而言之：它不能作弊！它遵守这两条规律的唯一方法实际上是不引入任何自身的影响。这意味着，在一个适当的仿函数fmap中，永远不会做任何意想不到的事情。事实上，除了映射给定的函数之外，它不能做任何事情。这是一个非常简单的例子，我没有解释为什么fmap不能作弊的所有细节，但它证明了这一点。

现在将其扩展到整个语言、基础库和最明智的第三方库。这为您提供了一种语言可以预测的语言。当你编写代码时，你就知道它会做什么。这是 Haskell 代码经常开箱即用的主要原因之一。我经常在编译之前写几页 Haskell 代码。一旦我的类型错误得到修复，我的程序通常可以工作。

这样做的另一个原因是它允许一种更具组合性的编程风格。这在团队合作时特别有用。首先，您将应用程序映射到代数结构并建立必要的定律。例如：您表达了成为有效 Web 服务器的含义。特别是，您建立了 Web 服务器组合的正式概念。如果您组合两个 Valid Web Server，则结果是一个 Valid Web Server。你知道这是怎么回事吗？在制定了这些法律之后，队友们开始工作，他们孤立地工作。完成工作几乎不需要沟通。当他们再次见面时，每个人都会展示他们的有效 Web 服务器，然后他们只是将它们组合成最终产品，一个网站。由于各个组件都是有效的 Web 服务器，最终结果必须是有效的 Web 服务器。可以证明。

Answer 2

是和不是。例如，Show该类没有任何与之相关的法律，它当然是有用的。

但是，类型类表示接口。一个接口需要满足的不仅仅是一堆函数——你希望这些函数满足一个规范。规范通常比用 Haskell 的类型系统表达的要复杂。例如，Eq上课。它只需要为我们提供一个函数，其类型必须是a -> a -> Bool. 这是 Haskell 的类型系统允许我们从一个Eq类型的实例中要求的最多的东西。但是，我们通常会期望从这个函数中得到更多——你可能希望它是一个等价关系（自反、对称和传递）。因此，您将这些要求声明为单独的“法律”。

Answer 3

类型类不需要有规律，但如果有规律，它通常会更有用。许多类型类都希望以某种方式发挥作用，这些法律规定了用户的期望。法律允许用户对类型类实例的工作方式做出假设。如果你违反了 typeclass 法律，你不会被 Haskell 警察逮捕，你只会让用户感到困惑。