将文字分配给 GHC 中的术语

Question

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

1 = 0

"hello" = "world"

由 GHC 有效和编译？这仅仅是一个错误还是一个功能？谢谢！

Answer 1

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

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

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"

数字文字和字符串文字是模式。（前一个 desugars 变成一个调用 的守卫(==)。）所以这些也是允许的：

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

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

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

x@3 = 3

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

x@3 = 4

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

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

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

Answer 2

因为这些文字是模式，所以您正在使用模式绑定。

letHaskell 中的绑定是惰性的，因此不执行实际的模式匹配。

但是如果我们强制匹配，它确实失败了：

> :{
  let
    x@1 = 0
  in
    1
  :}
1                    -- no assignment!     NB
it :: Num a => a

> :{
  let
    x@1 = 0
  in
    x
  :}
*** Exception: <interactive>:87:1-7: Irrefutable pattern failed for pattern x@1

因为1确实不是 0。

因此，这不是 GHC实现的错误或功能，而是 Haskell 语言本身的功能。