作者:林俊雯868043 | 来源:互联网 | 2023-10-14 11:20
出于好奇,为什么下面的程序
1 = 0
"hello" = "world"
由 GHC 有效和编译?这仅仅是一个错误还是一个功能?谢谢!
回答
这是允许的,因为它是语言规则的自然结果,并且没有足够的问题在语言规范中设置特殊情况来阻止它。
自然后果
有两种标准的定义:函数定义和数据定义。在函数定义中,您可以将模式作为参数写入等号左侧的函数。在数据定义中,您可以在等号左侧单独编写模式以匹配等号右侧的数据。所以,这些事情都是允许的:
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 终止。如果您的分析可以决定某些计算终止——例如,通过发现其中的所有递归都是结构性的或其他东西,则存在终止检查算法的整个家庭手工业——那么您可以让编译器进行检查。如果它确实终止,编译器实际上可以在编译期间运行计算,并仔细检查给定的模式实际上是否与值匹配。这样做的缺点是终止检查算法非常复杂,因此这给编译器编写者带来了很大的负担,并且有些是人类难以预测的,这使得针对它的编程让用户感到沮丧。
- 要求程序员证明匹配不能失败。您可以为程序员引入一种机制来为他们的程序编写证明,并要求他们证明匹配不会失败。这朝着依赖类型的方向发展;这种转变的两个主要成本通常是程序效率的降低,以及用这种语言编写程序需要更多的努力。
语言设计者做出了许多选择(不仅仅是在模式匹配语义中),这些选择在让程序员和编译器编写者的生活更轻松方面是错误的,但允许更多的程序抛出异常或永远不会完成。这是一个这样的地方——数据定义中允许可反驳的模式,即使这会导致崩溃,因为该策略的实现是有用的、简单的和可预测的。
@WillNess I have now added a section on why things like `x@1 = 0` are allowed. Thanks!
回答
因为这些文字是模式,所以您正在使用模式绑定。
let
Haskell 中的绑定是惰性的,因此不执行实际的模式匹配。
但是如果我们强制匹配,它确实失败了:
> :{
let
x@1 = 0
in
1
:}
1 -- no assignment! NB
it :: Num a => a
> :{
let
x@1 = 0
in
x
:}
*** Exception: :87:1-7: Irrefutable pattern failed for pattern x@1
因为1
确实不是 0
。
因此,这不是 GHC实现的错误或功能,而是 Haskell 语言本身的功能。
"let bindings in Haskell are lazy, so no actual pattern matching is performed." is not such explanation? I thought it was.