什么是弱头标准型(WHNF) ?Head Normal form (HNF)和Normal form (NF)是什么意思?
Real World Haskell声明:
我们熟悉的seq函数将表达式求值为
呼叫头标准型(简称HNF)。它一旦到达就会停止
最外层的构造函数(“head”)。这与正常情况不同
形式(NF)，其中表达式被完全求值。
您还会听到Haskell程序员提到弱头正常
表单(WHNF)。对于正规数据，弱头正规形式与
头部正常形式。这种差异只出现在函数中，也是如此
这里涉及到我们的深奥。
我读了一些资源和定义(Haskell维基和Haskell邮件列表和免费字典)，但我不明白。谁能举个例子或者给出一个外行的定义?
我猜它会类似于:
WHNF = thunk : thunk
HNF = 0 : thunk
NF = 0 : 1 : 2 : 3 : []
seq和($!)如何与WHNF和HNF相关?
更新
我还是很困惑。我知道有些答案说忽略HNF。从各种定义来看，WHNF和HNF中的常规数据似乎没有区别。然而，当涉及到函数时，似乎确实有区别。如果没有区别，为什么seq是必要的foldl'?
另一个混淆点来自Haskell Wiki，它声明seq简化为WHNF，并且不会对下面的示例执行任何操作。然后他们说他们必须使用seq来强制求值。这不是强迫它去HNF吗?
Common newbie stack overflowing code:
myAverage = uncurry (/) . foldl' (\(acc, len) x -> (acc+x, len+1)) (0,0)
People who understand seq and weak head normal form (whnf) can immediately understand what goes wrong here. (acc+x, len+1) is already in whnf, so the seq (in the definition of foldl'), which reduces a value to whnf, does nothing to this. This code will build up thunks just like the original foldl example, they'll just be inside a tuple. The solution is just to force the
components of the tuple, e.g.
myAverage = uncurry (/) . foldl'
(\(acc, len) x -> acc `seq` len `seq` (acc+x, len+1)) (0,0)
-Haskell Wiki在Stackoverflow上
我知道这是一个老问题，但这里有一个明确的WHNF, HNF和NF的数学定义。在纯lambda演算中:
如果一个项的形式是这样的，那么它就是NF
λx1。λ x2. ...λ xn. (x t1 t2…tm)
其中x是一个变量，t1, t2，…， tm在NF中。
一个术语是HNF，如果它的形式是
λx1。λ x2. ...λ xn. (x e1 e2…em)
其中x是一个变量，e1, e2，…， em是任意的术语。
在WHNF中，如果一个项是任意项e的λ项xe，或者它是这样的形式
X e1 e2…新兴市场
其中x是一个变量，e1, e2，…， em是任意的术语。
现在考虑一种具有构造函数a,b,c…集合na, nb, nc…，这意味着无论何时t1, t2，…， tm在NF中，那么术语a t1 t2…Tm，其中m = na是一个redex，可以计算。例如，Haskell中的加法构造函数+具有arity 2，因为它只在给出两个标准形式的参数时才计算值(在本例中，整数本身可以被视为null构造函数)。
A term is in NF if it is of the form
λ x1. λ x2. ... λ xn. (x t1 t2 ... tm)
where x is either a variable or a constructor of arity n with m < n, and t1, t2, ..., tm are in NF.
A term is in HNF if it is of the form
λ x1. λ x2. ... λ xn. (x e1 e2 ... em)
where x is either a variable or a constructor of arity n, and e1, e2, ... em are arbitrary terms so long as the first n arguments are not all in NF.
A term is in WHNF if it is either a lambda term λ x. e for any term e or if it is of the form
x e1 e2 ... em
where x is either a variable or a constructor of arity n, and e1, e2, ... em are arbitrary terms so long as the first n arguments are not all in NF.
特别地，NF中的任何项都在HNF中，HNF中的任何项都在WHNF中，但不是相反的。
头部正常形式意味着没有头部redex
(λx (y(λ。y + x) b)) b
简化为:R，代表redex(是的，它里面还有另一个redex，但这是不相关的)。这是一个头部redex，因为它是最左边的redex(唯一的redex)，在它之前没有lambda项(变量或lambda表达式(应用或抽象))，只有0到n个抽象者(如果R是一个redex (λx. a)B, R的抽象者是λx)，在这种情况下是0。
因为有一个头部索引，它不在HNF中，因此也不在NF中，因为有一个索引。
WHNF意味着它是一个lambda抽象或在HNF中。上述内容不在HNF中，也不是lambda抽象，而是一个应用程序，因此不在WHNF中。
λx.((λy.y+x)b)b在WHNF中
它是λ抽象，但不是在HNF中因为有一个头部λx。Rb
还原到λx.((b+x)b)。没有redex，所以是正常形式。
考虑λx.(λy.zyx)b)，化简为λx。R，所以不在HNF中。λx.(k(λy.zyx)b)化简为λx。因此它是在HNF中，而不是在NF中。
所有的NF均为HNF和WHNF。所有HNF均为WHNF。
