为什么所有Haskell类型类都具有法则? [英] Why do all Haskell typeclasses have laws?

问题描述

Typeclassopedia 中的所有类型类都具有关联的法则，例如某些运算符的关联性或可交换性. 法律"的定义似乎是无法在类型系统中表达的约束.我当然理解您为什么要拥有monad法则，但是是否存在一个根本原因，使得可以在类型系统中完全表达的类型类毫无意义呢?

All the typeclasses in Typeclassopedia have associated laws, such as associativity or commutativity for certain operators. The definition of a "law" seems to be a constraint that cannot be expressed in the type system. I certainly understand why you want to have, say, monad laws, but is there a fundamental reason why a typeclass that can be expressed fully within the type system is pointless?

推荐答案

您将注意到，几乎所有定律都是代数定律.可以通过类型系统使用一些扩展来表达它们，但是要表达这些证明会很麻烦.因此，您有不受约束的法律，可能的实现可能会破坏它们.为什么这样好?

You will notice that almost always the laws are algebraic laws. They could be expressed by the type system by using some extensions, but the proofs would be cumbersome to express. So you have unchecked laws and potentially implementations might break them. Why is this good?

原因是Haskell中使用的设计模式通常是由抽象代数的数学结构驱动的(在大多数情况下是镜像的).尽管大多数其他语言都对某些功能(例如安全性，性能和语义)具有直观的概念，但我们的Haskell程序员更喜欢建立 formal 概念.这样做的好处是:一旦您的类型和功能服从安全法则，就基本的代数结构而言，它们是安全的.他们可证明是安全的.

The reason is that the design patterns used in Haskell are motivated (and in most cases mirrored) by mathematical structures, usually from abstract algebra. While most other languages have an intuitive notion of certain features like safety, performance and semantics, we Haskell programmers prefer to establish a formal notion. The advantage of doing this is: Once your types and functions obey the safety laws, they are safe in the sense of the underlying algebraic structure. They are provably safe.

以函子为例. Haskell函子具有以下两个定律:

Take functors as an example. A Haskell functor has the following two laws:

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

首先，这非常重要:Haskell中的函数是不透明的.您无法对其进行检查，比较或任何其他操作.虽然这在Haskell中听起来像是一件坏事，但实际上却是一件好事. fmap函数无法检查您传递给它的函数.特别是，它无法检查您是否已通过标识函数或已通过合成.简而言之:它不能作弊！它遵守这两个定律的唯一方法实际上是不引入自己的任何影响.这意味着，在适当的函子中，fmap不会绝不会做任何意外的事情.实际上，除了映射给定的函数外，它无能为力.这是一个非常简单的示例，我没有解释为什么fmap不能作弊的所有微妙之处，但它说明了这一点.

Firstly this is very important: Functions in Haskell are opaque. You cannot examine, compare or whatever them. While this sounds like a bad thing in Haskell it is actually a very good thing. The fmap function cannot examine the function you've passed it. Particularly it can't check that you've passed the identity function or that you've passed a composition. In short: it can't cheat! The only way for it to obey these two laws is actually not to introduce any effects of its own. That means, in a proper functor fmap will never do anything unexpected. In fact it cannot do anything else than to map the given function. This is a very simple example and I haven't explained all the subtleties why fmap can't cheat, but it demonstrates the point.

现在将其扩展到所有语言，基本库和最明智的第三方库.这为您提供了一种语言可以预测的语言.当您编写代码时，您知道它会做什么.这就是Haskell代码经常开箱即用的主要原因之一.我经常在编译之前编写Haskell代码页.解决了我的类型错误后，我的程序通常可以正常工作.

Now extend this all over the language, the base libraries and most sensible third party libraries. This gives you a language that is as predictable as a language can get. When you write code, you know what it's going to do. That's one of the main reasons why Haskell code often works out of the box. I often write pages of Haskell code before compiling. Once my type errors are fixed, my program usually works.

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

The other reason why this is desirable is that it allows a more compositional style of programming. This is particularly useful when working as a team. First you map your application to algebraic structures and establish the necessary laws. For example: You express what it means for something to be a Valid Web Server. In particular you establish a formal notion of web server composition. If you compose two Valid Web Servers, the result is a Valid Web Server. Do you see where this is going? After establishing these laws the teammates go to work, and they work in isolation. Little to no communication is necessary to get their job done. When they meet again, everybody presents their Valid Web Servers and they just compose them to make the final product, a web site. Since the individual components were all Valid Web Servers, the final result must be a Valid Web Server. Provably.

这篇关于为什么所有Haskell类型类都具有法则?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！