将文字分配给 GHC 中的术语 [英] Assigning literals to terms in GHC

问题描述

出于好奇，为什么是下面的程序

Out of curiosity, why is the following program

1 = 0

"hello" = "world"

有效且可由 GHC 编译?这仅仅是一个错误还是一个功能?谢谢！

valid and compilable by GHC? Is this merely a bug or a feature? Thanks!

推荐答案

这是允许的，因为它是语言规则的自然结果，并没有大到足以在语言规范中设置特殊情况来阻止它的问题.

It is allowed because it is a natural consequence of the language rules, and not problematic enough to make a special case in the language specification to prevent it.

>

自然后果
有两种标准的定义:函数定义和数据定义.在函数定义中，你可以在等号左边写模式作为函数的参数.在数据定义中，您可以在等号左侧单独编写模式以匹配等号右侧的数据.所以，这些事情都是允许的:

Natural consequence
There are two standard kinds of definitions: function definitions and data definitions. In a function definition, you are allowed to write patterns as arguments to the function on the left of the equality sign. In data definitions, you are allowed to write a pattern by itself to the left of the equality sign to match against the data to the right of the equality sign. So, these kinds of things are all allowed:

x = 3
x@y = 3
[x, y, z] = [3, 4, 5]
[x, _, z] = [3, 4, 5]
[x, 4, z] = [3, 4, 5]
x:_ = "xsuffix"
x:"suffix" = "xsuffix"

数字文字和字符串文字是模式.(前者脱糖为调用 (==) 的守卫.)所以这些也是允许的:

Number literals and string literals are patterns. (The former desugars into a guard that calls (==).) So these are allowed, too:

3 = 3
x@3 = 3
[3, 4, 5] = [3, 4, 5]
"xsuffix" = "xsuffix"
-- and yes, these too
3 = 4
"xsuffix" = "lolno"

没问题
与语言的所有其他部分一样，数据定义是惰性的:它们表示的模式匹配计算在需要之前不会执行(通过检查匹配绑定的变量之一).由于 你好"= "world" 和 1 = 0 不绑定任何变量，它们代表的模式匹配计算——会抛出异常——永远不会执行.因此，避免允许它们并不是非常重要.

Not problematic
As with all other parts of the language, data definitions are lazy: the pattern match calculation they represent is not performed until it's demanded (by inspecting one of the variables bound by the match). Since "hello" = "world" and 1 = 0 do not bind any variables, the pattern match calculation they represent -- which would throw an exception -- is never performed. So it's not super important to avoid allowing them.

...除非是
但是等等......我们说这是一个有效的模式:

...except when it is
But wait... we said this was a valid pattern:

x@3 = 3

这个类似的发散并绑定一个变量:

And this similar one diverges and binds a variable:

x@3 = 4

为什么那个是允许的?这更难回答！我认为尝试考虑一些可以防止这种情况的语言规则是非常合理的.一般而言，合理且完备的规则当然是不可判定的，因为等式的右侧可以进行任意计算.但是您还可以做出其他选择；例如:

How come that one is allowed? That's much harder to answer! I think it would be quite reasonable to try to think of some language rules that would prevent this. In general, a rule that is sound and complete would of course be undecidable, since the right hand side of the equation can do arbitrary computation. But there are other choices you could make; for example:

• 不允许在数据定义中使用可反驳的模式.如果模式可能无法匹配，则它是可反驳的.例如，x 是无可辩驳的，x@y 是无可辩驳的，_ 是无可辩驳的，但是 x:y 是可反驳，True 可反驳，() 可反驳(因为当 RHS 处于底部时它会发散).这是迄今为止最简单的，并且会排除 x@3 = 4 和 hello";=世界" 两者.不幸的是，它也会排除非常有用的东西，比如 [x, y, z] = [3, 4, 5].
• 实施终止检查器，并要求可反驳模式的 RHS 终止.如果您的分析可以决定某些计算终止——例如，通过发现其中的所有递归都是结构性的或其他东西，那么有一个终止检查算法的整个家庭手工业——那么您可以让编译器检查它.如果它确实终止，编译器实际上可以在编译期间运行计算，并仔细检查给定的模式实际上是否与值匹配.这样做的缺点是终止检查算法非常复杂，因此这给编译器编写者带来了很大的负担，并且有些是人类难以预测的，这使得针对它的编程让用户感到沮丧.
• 要求程序员证明匹配不会失败.您可以为程序员引入一种机制来编写有关其程序的证明，并要求他们证明匹配不会失败.这朝着依赖类型的方向发展；此举的两个主要成本通常是程序效率的降低，以及使用此类语言编写程序需要付出更多努力.

• Do not allow refutable patterns in data definitions. A pattern is refutable if it could fail to match. For example, x is irrefutable, x@y is irrefutable, _ is irrefutable, but x:y is refutable, True is refutable, () is refutable (because it diverges when the RHS is bottom). This is by far the simplest, and would rule out x@3 = 4 and "hello" = "world" both. Unfortunately, it would also rule out very useful things like [x, y, z] = [3, 4, 5].
• Implement a termination checker, and require refutable patterns' RHS to terminate. If you had an analysis that could decide that some calculations terminate -- for example, by discovering that all recursion in it were structural or something, there's a whole cottage industry of termination checking algorithms -- then you could have the compiler check that. If it does terminate, the compiler can actually run the computation during compilation, and double-check that the pattern given actually will match the value. The downside of this is that termination-checking algorithms are very complicated, so this puts a big burden on the compiler writer, and some are difficult for humans to predict, which makes programming against it frustrating for the user.
• Demand that the programmer prove the match can't fail. You could introduce a mechanism for the programmer to write proofs about their programs, and demand that they prove the match won't fail. This moves in the direction of dependent types; the two main costs of such a move are typically a reduction in program efficiency and that writing programs in such languages requires much more effort.

语言设计者做出了许多选择(不仅仅是在模式匹配语义方面)，这些选择在让程序员和编译器编写者的生活更轻松方​​面是错误的，但允许更多的程序抛出异常或永远不会完成.这是一个这样的地方 - 数据定义中允许可反驳的模式，即使这可能会导致崩溃，因为该策略的实施是有用、简单且可预测的.

The language designers made a number of choices (not just in the pattern-matching semantics) that err on the side of making programmers' and compiler-writers' lives a bit easier, but allow a few more programs that throw exceptions or never finish. This is one such spot -- refutable patterns are allowed in data definitions, even if that can cause a crash, because the implementation of that policy is useful, simple, and predictable.

这篇关于将文字分配给 GHC 中的术语的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！