Haskell:什么是弱头正常形式？

Question

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

真实世界Haskell说:

熟悉的seq函数将表达式计算为我们称之为head normal form(缩写为HNF)的表达式.它一旦到达最外面的构造函数("头部")就会停止.这与正常形式(NF)不同,其中表达式被完全评估.

您还将听到Haskell程序员引用弱头正常形式(WHNF).对于正常数据,弱头正常形式与头部正常形式相同.差异只出现在功能上,而且我们在这里无关紧要.

我已经阅读了一些资源和定义(Haskell Wiki和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吗？

常见的新手堆栈溢出代码:

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

了解seq和弱头正常形式(whnf)的人可以立即明白这里出了什么问题.(acc + x,len + 1)已经在whnf中,所以seq将值减少到whnf,对此无效.这段代码将像原始的foldl示例一样构建thunks,它们只是在元组内部.解决方案只是强制元组的组件,例如

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.如果评估单个表达式导致这些嵌套评估过多,则结果是堆栈溢出.

当您构建一个不会生成任何数据构造函数或lambdas的大型表达式,直到对其进行大部分计算时,就会发生这种情况.这些通常是由以下类型的使用引起的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中关于Thunks和Weak Head Normal Form的部分Wikibooks 对懒惰的描述提供了对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 -> 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)

这是弱头正常形式,但不是头部正常形式...因为可能的应用程序被卡在一个无法评估的函数内部.

实际的头部正常形式难以有效实施.它需要在函数内部进行调整.因此,弱头法线形式的优点是您仍然可以将函数实现为opaque类型,因此它与编译语言和优化更兼容.

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

基本上,假设你有某种形式,t.

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

t1 : t2在哪里t1和t2是thunk.在这种情况下,t1将是你的0(或者更确切地说,0没有额外拆箱的thunk )

seq并$!评估WHNF.注意

f $! x = seq x (f x)