什么是弱头范式？

Question

弱头范式 (WHNF) 是什么意思？ Head Normal form (HNF) 和 Normal Form (NF) 是什么意思？

现实世界 Haskell 指出：

熟悉的seq函数将表达式计算为我们想要的值 称为头范式 （缩写为HNF）。一旦到达就停止 最外面的构造函数（“头”）。这与正常情况不同 形式 (NF)，其中表达式被完全求值。

您还会听到 Haskell 程序员提到 弱 头部正常 形式（WHNF）。对于普通数据，弱头范式与 头部正常形态。差异仅出现在功能上，而且差异太大 在这里关心我们是很深奥的。

我已经阅读了一些资源和定义（Haskell Wiki 和 Haskell 邮件列表和免费词典），但我不明白。有人可以举个例子或者提供一个外行定义吗？

我猜它类似于：

WHNF = thunk : thunk

HNF = 0 : thunk 

NF = 0 : 1 : 2 : 3 : []

How do seq and ($!) related to WHNF and HNF?

更新

我还是很困惑。我知道有些答案说忽略 HNF。从阅读各种定义来看，WHNF 和 HNF 中的常规数据似乎没有区别。然而，在功能方面似乎确实存在差异。如果没有区别，为什么 foldl' 需要 seq ？

另一个令人困惑的地方来自 Haskell Wiki，它指出 seq 简化为 WHNF，并且对以下示例没有任何作用。然后他们说必须使用 seq 来强制评估。这不是逼HNF吗？

常见新手堆栈溢出代码：

myAverage = uncurry (/) 。 Foldl' (\(acc, len) x -> (acc+x, len+1)) (0,0)

了解 seq 和弱头范式 (whnf) 的人可以立即明白这里出了什么问题。 (acc+x, len+1) 已经在 whnf 中，因此，seq（在 foldl' 的定义中）将值减少为 whnf，对 这。此代码将像原始的 foldl 示例一样构建 thunk，它们只是位于元组内。解决办法就是强制 元组的组成部分，例如

myAverage = uncurry (/) 。折叠' 
          (\(acc, len) x -> acc `seq` len `seq` (acc+x, len+1)) (0,0)

-Stackoverflow 上的 Haskell Wiki

Answer 1

我将尝试用简单的术语给出解释。正如其他人指出的那样，head 范式不适用于 Haskell，所以我不会在这里考虑它。

正常形式

正常形式的表达式被完全求值，并且不能进一步求值任何子表达式（即它不包含未求值的 thunk）。

这些表达式都是正规形式：

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 抽象（head）。子表达式可能已被计算，也可能未被计算。因此，每个范式表达式也是弱头范式，尽管相反的情况通常不成立。

为了判断一个表达式是否是弱头范式，我们只需要查看表达式的最外层部分。如果它是数据构造函数或 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。例如，要计算 WHNF 的 1 + (2 + 3)，我们首先必须计算 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 不提前减少内部表达式呢？那是因为 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.

Answer 2

Haskell Wikibooks 中关于Thunks 和弱头范式的部分 对懒惰的描述提供了非常好的描述WHNF 以及这个有用的描述：

逐步评估值 (4, [1, 2])。第一阶段是
完全没有被评估；所有后续形式均采用 WHNF 形式，最后一个形式
一个也处于正常状态。

Answer 3

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 ->表达式

换句话说，表达式的头部（即最外层函数应用程序）不能被进一步求值，但函数参数可能包含未求值的表达式。

WHNF 示例：

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

---

注释

1. WHNF 中的“头”不是指列表的头，而是指最外层的函数应用程序。
2. 有时，人们将未评估的表达式称为“thunks”，但我认为这不是理解它的好方法。
3. Head 范式 (HNF) 与 Haskell 无关。它与 WHNF 的不同之处在于 lambda 表达式的主体也在某种程度上进行求值。

Answer 4

http://foldoc.org/Weak+Head+Normal+Form Head 给出了很好的解释和示例范式甚至简化了函数抽象内部表达式的位，而“弱”头范式则停止于函数抽象。

从源头来看，如果您有：

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

那是弱头部正常形式，但不是头部正常形式......因为可能的应用程序被困在尚无法评估的函数内部。

实际的头部范式很难有效地实现。这需要探索函数内部。因此，弱头范式的优点是您仍然可以将函数实现为不透明类型，因此它与编译语言和优化更兼容。

Answer 5

WHNF 不希望计算 lambda 的主体，因此

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

Answer 6

基本上，假设您有某种 thunk，t。

现在，如果我们想要将 t 计算为 WHNF 或 NHF（除了函数之外，它们是相同的），我们会发现我们得到类似

t1 : t2 的内容，其中 t1 和 t2 是 thunk。在这种情况下，t1 将是您的 0（或者更确切地说，在没有额外拆箱的情况下，对 0 进行重击）

seq 和 $! 计算 WHNF。注意

f $! x = seq x (f x)

Answer 7

我意识到这是一个老问题，但这里有 WHNF、HNF 和 NF 的明确数学定义。在纯 lambda 演算中：

• 如果一项的形式为 NF，则该项为 NF

  <前><代码>λ x1。 λx2。 ... λ xn。 (x t1 t2 ... tm)

  其中 x 是变量，t1, t2, ..., tm 位于 NF 中。

• 。

  如果项的形式为 HNF，则该项属于 HNF

  <前><代码>λ x1。 λx2。 ... λ xn。 (x e1 e2 ... em)

  其中 x 是变量，e1, e2, ..., em 是任意项。

• 。

  如果一项是 lambda 项 λ x，则该项属于 WHNF。 e 表示任何术语 e 或者如果它的形式为

  x e1 e2 ... em
  

  其中 x 是变量，e1, e2, ..., em 是任意项。

---

现在考虑一种编程语言，其构造函数 a,b,c... 数量为 na, nb, nc...< /code>，这意味着只要 t1, t2, ..., tm 位于 NF 中，则术语 a t1 t2 ... tm 其中 m = na 是一个 redex，可以是评价。例如，Haskell 中的加法构造函数 + 具有元数 2，因为它仅在以正常形式给出两个参数时才进行计算（在本例中） case 整数，它们本身可以被视为无效构造函数）。

• 如果项的形式为 NF，则该项属于 NF

  <前><代码>λ x1。 λx2。 ... λ xn。 (x t1 t2 ... tm)

  其中 x 是一个变量或一个 arity n 的构造函数，其中 m m n 。 n 和 t1, t2, ..., tm 属于 NF。

  


• 如果项的形式为 HNF，则该项属于 HNF

  <前><代码>λ x1。 λx2。 ... λ xn。 (x e1 e2 ... em)

  其中 x 是一个变量或一个 arity n 的构造函数，而 e1, e2, ... em 是任意项 < em>只要前 n 个参数并非全部都在 NF 中。

• 如果满足以下条件，则项在 WHNF 中：它是 lambda 项 λ x。 e 表示任何术语 e 或者如果它的形式为

  x e1 e2 ... em
  

  其中 x 是一个变量或一个 arity n 的构造函数，而 e1, e2, ... em 是任意项 < em>只要前 n 个参数并非全部都在 NF 中。

---

特别是，NF 中的任何术语都是 HNF 中的，并且 HNF 中的任何术语都是属于 WHNF，但反之则不然。

Answer 8

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

Simon Peyton Jones 的《函数式编程语言的实现》第 11 章。

Answer 9

Head 范式意味着没有 head redex

(λx.((λy.y+x)b))b

简化为：R，用于 redex（是的，其中还有另一个 redex，但这无关紧要）。这是一个 head redex，因为它是最左边的 redex（唯一的 redex），并且它之前没有 lambda 项（变量或 lambda 表达式（应用程序或抽象）），只有 0 到 n 个抽象器（如果 R 是 redex (λx.A)B R 的抽象器是 λx)，在本例中为 0。

因为有一个头 redex，所以它不在 HNF 中，因此也不是在 NF 中，因为有一个 redex。

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。