haskell - 什么是弱头范式？

Question

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

真实世界的 Haskell状态：

熟悉的 seq 函数将表达式计算为我们所说 的头部范式 （缩写为 HNF）。一旦到达最外层的构造函数（“头部”），它就会停止。这与 标准形式 (NF) 不同，在标准形式中，表达式被完全评估。

您还会听到 Haskell 程序员提到 弱 头范式 (WHNF)。对于法线数据，弱头范式与头范式相同。区别只出现在功能上，而且太深奥了，我们在这里不关心。

我已经阅读了一些资源和定义（Haskell Wiki和Haskell Mail List和Free Dictionary），但我不明白。有人可以举个例子或提供一个外行定义吗？

我猜它会类似于：

WHNF = thunk : thunk

HNF = 0 : thunk 

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

WHNFseq和($!)HNF 有什么关系？

更新

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

另一个混淆点来自 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，对此没有任何作用。这段代码将像原始示例一样构建 thunk  foldl ，它们只是在一个元组中。解决方案只是强制元组的组件，例如

myAverage = uncurry (/) . foldl' 
          (\(acc, len) x -> acc `seq` len `seq` (acc+x, len+1)) (0,0)

- Stackoverflow 上的 Haskell Wiki

Answer 1

我将尝试用简单的术语来解释。正如其他人所指出的，头部范式不适用于 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 抽象（头）。子表达式可能已经被评估，也可能没有被评估。因此，每个范式表达式也是弱头范式，尽管反之一般不成立。

要确定一个表达式是否是弱头范式，我们只需要查看表达式的最外层部分。如果它是数据构造函数或 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 不提前减少内部表达式呢？那是因为 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。在下面的示例中，累加器是一个元组，因此它只会强制评估元组构造函数，而不是accor 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.

为了避免这种情况，我们必须使评估元组构造函数强制评估accand 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和 Weak Head Normal Form的部分提供了对 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 ...
• 参数太少的内置函数，例如(+) 2orsqrt
• 一个 lambda 表达式：\x -> expression

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

WHNF 的示例：

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

---

笔记

1. WHNF 中的“头”不是指列表的头，而是指最外层的函数应用程序。
2. 有时，人们称未评估的表达式为“thunk”，但我认为这不是理解它的好方法。
3. 头范式（HNF）与 Haskell 无关。它与 WHNF 的不同之处在于 lambda 表达式的主体也在一定程度上被评估。

Answer 4

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

从源头看，如果您有：

\ 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，.

现在，如果我们想要评估tWHNF 或 NHF，除了函数之外它们是相同的，我们会发现我们得到类似

t1 : t2wheret1和t2are thunks。在这种情况下，t1将是您的0（或者更确切地说，0没有额外的拆箱）

seq并$!评估 WHNF。注意

f $! x = seq x (f x)

Answer 7

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

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

Answer 8

我意识到这是一个老问题，但这是 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是任意项。

• λ x. e如果一个术语是任何术语的 lambda 术语，e或者它的形式为

  x e1 e2 ... em
  

  其中x是一个变量并且e1, e2, ..., em是任意项。

---

现在考虑一种具有arity构造函数的编程语言 ，这意味着只要在 NF 中，术语where就是 redex 并且可以被评估。例如，Haskell 中的加法构造函数具有 arity ，因为它仅在给定两个正常形式的参数时才进行评估（在这种情况下为整数，它们本身可以被视为空构造函数）。a,b,c...na, nb, nc...t1, t2, ..., tma t1 t2 ... tmm = na+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是变量或 arity 的构造函数n，并且e1, e2, ... em是任意项，只要第一个n参数不全部在 NF 中。

• λ x. e如果一个术语是任何术语的 lambda 术语，e或者它的形式为

  x e1 e2 ... em
  

  其中x是变量或 arity 的构造函数n，并且e1, e2, ... em是任意项，只要第一个n参数不全部在 NF 中。

---

特别是，NF 中的任何项都属于 HNF，HNF 中的任何项都属于 WHNF，但反过来则不然。

Answer 9

头部正常形式意味着没有头部还原

(λ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。

因为有一个 head 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。