小开

基本上，假设你有某种坦克，t。

现在，如果我们想求t到WHNF或NHF的值，这两个值除了函数外都是一样的，我们会发现我们会得到类似的结果

t1 : t2，其中t1和t2是坦克。在这种情况下，t1将是你的0(或者更确切地说，没有额外开箱的0)

seq和$!计算WHNF。请注意,

f $! x = seq x (f x)

小开

http://foldoc.org/Weak+Head+Normal+Form给出了一个很好的解释，头部标准形式简化了函数抽象中表达式的位，而“弱”头部标准形式止于函数抽象。

从源头看，如果你有:

\ x -> ((\ y -> y+x) 2)

这是弱头部正常形式，但不是头部正常形式……因为可能的应用程序被卡在一个还不能求值的函数中。

实际的头部标准形式将难以有效地实现。这需要在函数内部进行操作。因此，弱头标准形式的优点是，您仍然可以将函数作为不透明类型来实现，因此它与编译语言和优化更加兼容。

小开

WHNF不希望对lambdas的主体进行计算，因此

WHNF = \a -> thunk
HNF = \a -> a + c

seq希望它的第一个参数在WHNF中，因此

let a = \b c d e -> (\f -> b + c + d + e + f) b
b = a 2
in seq b (b 5)

计算结果为

\d e -> (\f -> 2 + 5 + d + e + f) 2

而不是，什么会使用HNF

\d e -> 2 + 5 + d + e + 2

小开

Haskell程序是表达式，它们通过执行评价来运行。

要计算表达式，请将所有函数应用程序替换为它们的定义。这样做的顺序并不重要，但仍然很重要:从最外层的应用程序开始，从左到右;这被称为懒惰的评价。

例子:

   take 1 (1:2:3:[])
=> { apply take }
1 : take (1-1) (2:3:[])
=> { apply (-)  }
1 : take 0 (2:3:[])
=> { apply take }
1 : []

当没有剩余的功能应用程序需要替换时，计算就会停止。结果在标准形式(或简化范式, RNF)中。无论以何种顺序求值表达式，最终都会得到相同的标准形式(但只有在求值结束时)。

对于惰性求值的描述略有不同。也就是说，它说你应该只对弱头正常型求值。表达式在WHNF中有三种情况:

构造函数:constructor expression_1 expression_2 ...
参数太少的内置函数，如(+) 2或sqrt
lambda表达式:\x -> expression

换句话说，表达式的头(即最外层的函数应用程序)不能再求值，但函数参数可以包含未求值的表达式。

WHNF的例子:

3 : take 2 [2,3,4]   -- outermost function is a constructor (:)
(3+1) : [4..]        -- ditto
\x -> 4+5            -- lambda expression

笔记

WHNF中的“头”不是指列表的头，而是指最外层的函数应用程序。
有时，人们称未求值的表达式为“thunk”，但我不认为这是理解它的好方法。
头部标准型 (HNF)与Haskell无关。它与WHNF的不同之处在于，lambda表达式的主体也在某种程度上被求值。

小开

最佳答案

我试着用简单的语言解释一下。正如其他人指出的那样，head范式并不适用于Haskell，所以我在这里不考虑它。

标准形式

正常形式的表达式被完全求值，没有子表达式可以被进一步求值(即它不包含未求值的符号)。

这些表达式都是标准形式:

42
(2, "hello")
\x -> (x + 1)

这些表达式不是正常形式:

1 + 2                 -- we could evaluate this to 3
(\x -> x + 1) 2       -- we could apply the function
"he" ++ "llo"         -- we could apply the (++)
(1 + 1, 2 + 2)        -- we could evaluate 1 + 1 and 2 + 2

弱头正常型

弱头标准形式的表达式已经被求值到最外层的数据构造函数或lambda抽象(头)。子表达式有没有评估过。因此，每个正规形式的表达式也是弱头正规形式，尽管相反的情况并不普遍。

要确定表达式是否为弱头正规形式，我们只需查看表达式的最外层。如果它是一个数据构造函数或，它是弱头正规形式。如果是函数应用，就不是。

这些表达式是弱头范式:

(1 + 1, 2 + 2)       -- the outermost part is the data constructor (,)
\x -> 2 + 2          -- the outermost part is a lambda abstraction
'h' : ("e" ++ "llo") -- the outermost part is the data constructor (:)

如上所述，上面列出的所有正规形式表达式也是弱头正规形式。

这些表达式不是弱头正规形式:

1 + 2                -- the outermost part here is an application of (+)
(\x -> x + 1) 2      -- the outermost part is an application of (\x -> x + 1)
"he" ++ "llo"        -- the outermost part is an application of (++)

堆叠溢位

将一个表达式求为弱头标准式可能需要先将其他表达式求为WHNF。例如，要计算1 + (2 + 3)到WHNF，首先必须计算2 + 3。如果对单个表达式求值会导致太多这样的嵌套求值，则会导致堆栈溢出。

当您构建一个大型表达式时，该表达式直到对其中的大部分进行了计算才会产生任何数据构造函数或lambda，就会发生这种情况。这通常是由foldl的这种用法引起的:

foldl (+) 0 [1, 2, 3, 4, 5, 6]
= foldl (+) (0 + 1) [2, 3, 4, 5, 6]
= foldl (+) ((0 + 1) + 2) [3, 4, 5, 6]
= foldl (+) (((0 + 1) + 2) + 3) [4, 5, 6]
= foldl (+) ((((0 + 1) + 2) + 3) + 4) [5, 6]
= foldl (+) (((((0 + 1) + 2) + 3) + 4) + 5) [6]
= foldl (+) ((((((0 + 1) + 2) + 3) + 4) + 5) + 6) []
= (((((0 + 1) + 2) + 3) + 4) + 5) + 6
= ((((1 + 2) + 3) + 4) + 5) + 6
= (((3 + 3) + 4) + 5) + 6
= ((6 + 4) + 5) + 6
= (10 + 5) + 6
= 15 + 6
= 21

请注意，在将表达式转换为弱头部正常形式之前，它必须走得相当深。

你可能会想，为什么Haskell不提前减少内心的表达?那是因为哈斯克尔的懒惰。由于不能一般地假定每个子表达式都需要，所以表达式是由外向内求值的。

(GHC有一个严格性分析器，它可以检测到总是需要子表达式的某些情况，然后它可以提前计算它。然而，这只是一个优化，您不应该依赖它来避免溢出)。

另一方面，这种表达是完全安全的:

data List a = Cons a (List a) | Nil
foldr Cons Nil [1, 2, 3, 4, 5, 6]
= Cons 1 (foldr Cons Nil [2, 3, 4, 5, 6])  -- Cons is a constructor, stop.

为了避免在知道必须对所有子表达式求值时构建这些大表达式，我们希望强制提前对内部部分求值。

`seq`

seq是一个特殊的函数，用于强制表达式求值。它的语义是，seq x y意味着每当y被求为弱头标准形式时，x也被求为弱头标准形式。

它在foldl' (foldl的严格变体)的定义中使用。

foldl' f a []     = a
foldl' f a (x:xs) = let a' = f a x in a' `seq` foldl' f a' xs

foldl'的每次迭代都强制累加器为WHNF。因此，它可以避免构建一个大表达式，从而避免堆栈溢出。

foldl' (+) 0 [1, 2, 3, 4, 5, 6]
= foldl' (+) 1 [2, 3, 4, 5, 6]
= foldl' (+) 3 [3, 4, 5, 6]
= foldl' (+) 6 [4, 5, 6]
= foldl' (+) 10 [5, 6]
= foldl' (+) 15 [6]
= foldl' (+) 21 []
= 21                           -- 21 is a data constructor, stop.

但正如HaskellWiki上的例子所提到的，这并不是在所有情况下都可以节省您的时间，因为累加器只计算到WHNF。在下面的例子中，累加器是一个元组，因此它只强制求元组构造函数的值，而不是acc或len。

f (acc, len) x = (acc + x, len + 1)


foldl' f (0, 0) [1, 2, 3]
= foldl' f (0 + 1, 0 + 1) [2, 3]
= foldl' f ((0 + 1) + 2, (0 + 1) + 1) [3]
= foldl' f (((0 + 1) + 2) + 3, ((0 + 1) + 1) + 1) []
= (((0 + 1) + 2) + 3, ((0 + 1) + 1) + 1)  -- tuple constructor, stop.

为了避免这种情况，必须使求值元组构造函数强制求值acc和len。我们通过使用seq来做到这一点。

f' (acc, len) x = let acc' = acc + x
len' = len + 1
in  acc' `seq` len' `seq` (acc', len')


foldl' f' (0, 0) [1, 2, 3]
= foldl' f' (1, 1) [2, 3]
= foldl' f' (3, 2) [3]
= foldl' f' (6, 3) []
= (6, 3)                    -- tuple constructor, stop.

小开

Haskell Wikibooks 懒惰的描述中关于坦克和弱头正常形态的部分提供了非常好的WHNF描述，以及以下有用的描述:

逐步评估值(4，[1,2])。第一阶段完全没有评估;所有随后的形式都是WHNF形式，最后一种形式也是normal形式。

逐步评估值(4，[1,2])。第一阶段是完全未鉴定的;所有随后的形式都在WHNF中，而最后一个也是正形式

小开

在图约简的实现中，对HNF的惰性求值迫使您处理lambda演算的名称捕获问题，而对WHNF的惰性求值则可以避免这个问题。

Simon Peyton Jones在函数式编程语言的实现第11章中解释了这一点。

小开

我知道这是一个老问题，但这里有一个明确的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是任意项。
如果一个词是任意词e的lambda词λ x. e，或者它的形式为
```
x e1 e2 ... em
```
其中x是变量，e1, e2, ..., em是任意项。

现在考虑一个集合na, nb, nc...的带有构造函数的编程语言 a,b,c...，这意味着只要t1, t2, ..., tm在NF中，那么术语a t1 t2 ... tm，其中m = na是一个索引，可以被求值。例如，Haskell中的加法构造函数+具有2，因为当给出两个标准形式的参数时(在这种情况下，整数本身可以被视为零构造函数)，它只有评估。

形式为NF的项
```
λ x1. λ x2. ... λ xn. (x t1 t2 ... tm)
```
其中x要么是一个变量，要么是n和m < n的构造函数，而t1, t2, ..., tm在NF中。
一个项的形式为HNF
```
λ x1. λ x2. ... λ xn. (x e1 e2 ... em)
```
其中x是n的变量或构造函数，而e1, e2, ... em是任意术语只要第一个n参数是not all in NF。
如果一个词是任意词e的lambda词λ x. e，或者它的形式为
```
x e1 e2 ... em
```
其中x是n的变量或构造函数，而e1, e2, ... em是任意术语只要第一个n参数是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中

它是一个lambda抽象，但不是在HNF中，因为有一个头λx.Rb

化简为λx.((b+x)b)。没有redex，所以是正常形式。

考虑λx.((λy.zyx)b)，它简化为λx.R，所以它不在HNF中。λx.(k(λy.zyx)b)简化为λx.kR，因此它是HNF而不是NF。

所有的NF均为HNF和WHNF。所有HNF均为WHNF。

什么是弱头正常形式?

更新

标准形式

弱头正常型

堆叠溢位

`seq`