什么是严格？

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有米的参数,那么它是在第n个参数严格一些ñ ≤ 米 ∀A1的时候,......,我.f a1 a2 ... a(n-1)⊥a(n + 1)... am =⊥.

(旁白:为什么这不是很正确？对于许多函数 - 包括const- 我们无法静态地知道它有多少个参数.虽然const看起来它可能是一个双参数函数,但const id () ()输入完全正确并且适用const于三个论点.)

现在我们可以说" const对它的第一个参数是严格的"并且它意味着我们想要它意味着什么(如上所述,const实际上是一个双参数函数),因为∀ y.const ? y = ?的确如此.

我们现在也有工具来解决你的问题ifFun,即:ifFun第二个论点是严格的吗？也就是说,我们可以编造pred并alt使得

ifFun pred ? alt ? ? -- ?

我认为很明显我们可以这样做,因为:

ifFun False ? () = if False then ? else () = () ? ?

类似的论点显示,ifFun是"不严格在其第三个参数"在此短语的通俗的理解(再次模上面讨论的附带条件),但是 "严格上的第一个参数".