什么是严格？

Question

在 Haskell 中，我试图理解严格的概念。我明白了

const x y = x

对第一个参数严格，但对第二个参数不严格。 但是是

 ifFun pred cons alt = if pred then cons else alt

严格？它对第一个论点很严格。我知道 cons 和 alt 的评估取决于 pred 的值。这是否意味着该函数对这些参数不严格？

Answer 1

“严格”是具有精确技术含义的词之一，社区已将其用于表示不那么正式的含义。这是技术定义。

如果f ⊥ = ⊥，函数f是严格。

这里 ⊥ 是未定义计算的标准符号；通常在指称语义中只有一个并且所有未定义的计算彼此无法区分，但在 Haskell 中作为对实用性的让步，我们有许多不同的类型可以区分：异常、无限循环、模式匹配失败等。出于此答案的目的，我们将认为它们都是平等的。

让我们问一下const 是否严格。我们有

const = \x -> \y -> x

因此

const ⊥ = \y -> ⊥ ≠ ⊥

因此const 并不严格。但是，哦，我们在这里失去了一些非常重要的沟通能力！有一种很好的感觉，当应用于未定义的行为时，const 表现不佳。很多人会说“在第 n 个参数中是严格的”，我们会非常理解他们的意思。尚不清楚如何正式定义它们的含义，但稍微像样的第一次尝试是这样的：

如果函数 f 有 m 个参数，那么对于某些 n ≤ m严格的 /em> 当 ∀ a1, ..., am。 f a1 a2 ... a(n-1) ⊥ a(n+1) ... am = ⊥.

（旁白：为什么这不太对？对于许多函数——包括const——我们不能静态知道它有多少个参数。虽然const看起来可能是两个参数函数，const id () () 的类型非常好，并将const 应用于三个参数。）

现在我们可以说类似“const is strict on its first argument”，并让它的意思是我们想要的意思（前提是，如上所述，const 实际上是一个有两个参数的函数），因为∀y。 const ⊥ y = ⊥ 确实成立。

我们现在还拥有解决您关于ifFun 的问题的工具，即：ifFun 的第二个参数是否严格？也就是说，我们能不能把pred 和alt 弄成这样

ifFun pred ⊥ alt ≠ ⊥ -- ?

我认为很明显我们可以这样做，因为：

ifFun False ⊥ () = if False then ⊥ else () = () ≠ ⊥

一个类似的论点表明，ifFun 在这个短语的通俗理解中“对第三个论点不严格”（再次以上面讨论的附带条件为模），但 是“在它的第一个论点上严格”论据”。