哈斯克尔:什么是弱头正常形式? [英] Haskell: What is Weak Head Normal Form?

查看:126
本文介绍了哈斯克尔:什么是弱头正常形式?的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!

问题描述

弱头范式(WHNF)是什么意思? Head Normal form (HNF)和 Normal Form (NF)是什么意思? http://book.realworldhaskell.org/read/concurrent-and-multicore-programming.htmlrel =noreferrer>真实世界Haskell 指出:

< blockquote>

熟悉的seq函数将表达式评估为我们称之为
的正常形式(缩写为HNF)的表达式。它一旦到达最外层的
构造函数(head)就会停止。这与正常形式(NF)截然不同,在
中表达式被完全评估。您还会听到Haskell程序员提到的弱头正常形式
(WHNF)。对于正常数据,弱头正常形式与头部
正常形式相同。差异只出现在函数上,而且
的深度值得我们关注。


我已经阅读了一些资源和定义( Haskell Wiki Haskell Mail List and 免费字典),但我不明白。有人可能会给一个例子或提供一个外行人的定义?

我猜它会类似于:

  WHNF = thunk:thunk 

HNF = 0:thunk

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

seq ($!)与WHNF和HNF有关?

更新



我是仍然困惑。我知道一些答案说忽略HNF。从阅读各种定义看来,WHNF和HNF的常规数据似乎没有区别。但是,它看起来好像在功能方面有所不同。如果没有区别,为什么 foldl'?
$ b必须 seq $ b

另一个混淆之处是来自Haskell Wiki,它指出 seq 简化为WHNF,并且对以下示例不起作用。然后他们说他们必须使用 seq 来强制评估。是不是强迫它到HNF?


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

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

理解seq和弱头正常形式(whnf)
的人可以立即明白这里出了什么问题。 (acc + x,len + 1)已经是
,所以seq,它将一个值减小为whnf,对此没有任何影响。
这段代码将像原来的foldl例子一样构建thunk,
它们只是在一个元组中。解决方案是强制元组的
组件,例如

  myAverage = uncurry(/)。 (acc + x,len + 1))(0,0)
$ / $ c $($,$ len $) c>


- Haskell维基于Stackoverflow

解决方案

我会尽量简单地解释一下。正如其他人指出的,头标准形式不适用于Haskell,所以我不会在这里考虑它。



正常形式



正常形式的表达式会被完全评估,并且任何子表达式都不能被进一步评估(即它不包含未评估的thunk)。

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

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

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

  1 + 2  - 我们可以将其评估为3 
(\ x - > x + 1)2 - 我们可以将函数
he++llo - 我们可以应用(++)
(1 + 1,2 + 2) - 我们可以评估1 + 1和2 + 2



弱头标准形式



标准形式已经被评估为最外层的数据构造函数或lambda抽象( head )。子表达式可能已经评估过或可能未被评估过。因此,每一个正常形式的表达式也是弱头正常形式,尽管相反并不普遍。为了确定一个表达式是否处于弱头法线形式,我们只需要看表达式的最外面的部分。如果它是一个数据构造函数或一个lambda,它就是弱头标准形式。如果它是一个函数应用程序,它不是。

这些表达式以弱头标准形式出现:

 (1 + 1,2 + 2) - 最外面的部分是数据构造函数(,)
\ x - > 2 + 2 - 最外面的部分是lambda抽象
'h':(e++llo) - 最外面的部分是数据构造函数(:)


$ b如前所述,上面列出的所有常规表单表达式都是弱头标准形式。



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

  1 + 2  - 这里最外面的部分是一个应用程序(+)
(\ x - > x + 1)2 - 最外面的部分是(\ x - > x + 1)
he++ llo - 最外面的部分是一个应用程序(++)



堆栈溢出



评估表达式为弱头标准形式可能需要先将其他表达式评估为WHNF。例如,要评估 1 +(2 + 3)到WHNF,我们首先必须评估 2 + 3 。如果评估单个表达式会导致太多这样的嵌套评估,那么结果就是堆栈溢出。



当你建立一个不产生任何内容的大表达式时,会发生这种情况数据构造函数或lambda表达式,直到其大部分被评估为止。这些通常是由 foldl 的使用引起的:

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

请注意,它可以将表达式转化为弱头标准形式。

您可能会想,为什么Haskell不提前减少内部表达式?这是因为Haskell的懒惰。由于不能一般假定每个子表达式都需要,所以表达式会从外部进行评估。



(GHC有一个严格分析器,可以检测出某些情况,其中a子表达式总是需要的,然后它可以提前评估它,但这只是一种优化,你不应该依赖它来避免溢出)。另一方面,这种表达是完全安全的:

 数据List a = Cons a(List a)|无
foldr缺点[1,2,3,4,5,6]
=缺点1(缺点缺点[2,3,4,5,6]) - 缺点是构造函数, 停止。

为了避免在知道所有子表达式必须被评估时构建这些大型表达式,我们希望强制内部部分提前评估。

seq



seq 是一个特殊的函数,用于强制表达式被评估。它的语义是: seq xy 表示每当 y 被评估为弱头标准形式时, x 也被评估为弱头正常形式。



它是 foldl' foldl 的严格版本。

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

每次迭代 foldl'强制累加器到WHNF。因此它避免了建立一个大表达式,因此避免了堆栈溢出。

  foldl'(+)0 [1, (+)1 [2,3,4,5,6] 
= fold1'(+)3 [3,4,5,6]
= fold1' 6]
= foldl'(+)6 [4,5,6]
= foldl'(+)10 [5,6]
= foldl'(+)15 [6]
= foldl'(+)21 []
= 21 - 21是一个数据构造函数,stop。

但是正如HaskellWiki提到的例子,这并不能在所有情况下保存你,因为累加器是只评估为WHNF。在这个例子中,累加器是一个元组,所以它只会强制评估元组构造函数,而不是 acc len

pre code $ f(acc,len)x =(acc + x,len + 1)
$ b (0,0)[1,2,3]
= foldl'f(0 + 1,0 + 1)[2,3]
= foldl'f ((0 + 1)+2)+3,((0 + 1)+ 1)[3]
= []
=(((0 + 1)+ 2)+ 3,((0 + 1)+ 1)+ 1) - 元组构造函数stop。

为了避免这种情况,我们必须使得评估元组构造器对 acc len 。我们通过使用 seq 来做到这一点。

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

(1,1)[2,3]
= fold1'f'(3,2)[1,2,3]
= foldl'f' 3]
= foldl'f'(6,3)[]
=(6,3) - 元组构造函数,stop。


What does Weak Head Normal Form (WHNF) mean? What does Head Normal form (HNF) and Normal Form (NF) mean?

Real World Haskell states:

The familiar seq function evaluates an expression to what we call head normal form (abbreviated HNF). It stops once it reaches the outermost constructor (the "head"). This is distinct from normal form (NF), in which an expression is completely evaluated.

You will also hear Haskell programmers refer to weak head normal form (WHNF). For normal data, weak head normal form is the same as head normal form. The difference only arises for functions, and is too abstruse to concern us here.

I have read a few resources and definitions (Haskell Wiki and Haskell Mail List and Free Dictionary) but I don't get it. Can someone perhaps give an example or provide a layman definition?

I am guessing it would be similar to:

WHNF = thunk : thunk

HNF = 0 : thunk 

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

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

Update

I am still confused. I know some of the answers say to ignore HNF. From reading the various definitions it seems that there is no difference between regular data in WHNF and HNF. However, it does seem like there is a difference when it comes to a function. If there was no difference, why is seq necessary for foldl'?

Another point of confusion is from the Haskell Wiki, which states that seq reduces to WHNF, and will do nothing to the following example. Then they say that they have to use seq to force the evaluation. Is that not forcing it to 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 seq, 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 on Stackoverflow

解决方案

I'll try to give an explanation in simple terms. As others have pointed out, head normal form does not apply to Haskell, so I will not consider it here.

Normal form

An expression in normal form is fully evaluated, and no sub-expression could be evaluated any further (i.e. it contains no un-evaluated thunks).

These expressions are all in normal form:

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

These expressions are not in normal form:

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

Weak head normal form

An expression in weak head normal form has been evaluated to the outermost data constructor or lambda abstraction (the head). Sub-expressions may or may not have been evaluated. Therefore, every normal form expression is also in weak head normal form, though the opposite does not hold in general.

To determine whether an expression is in weak head normal form, we only have to look at the outermost part of the expression. If it's a data constructor or a lambda, it's in weak head normal form. If it's a function application, it's not.

These expressions are in weak head normal form:

(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 (:)

As mentioned, all the normal form expressions listed above are also in weak head normal form.

These expressions are not in weak head normal form:

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 (++)

Stack overflows

Evaluating an expression to weak head normal form may require that other expressions be evaluated to WHNF first. For example, to evaluate 1 + (2 + 3) to WHNF, we first have to evaluate 2 + 3. If evaluating a single expression leads to too many of these nested evaluations, the result is a stack overflow.

This happens when you build up a large expression that does not produce any data constructors or lambdas until a large part of it has been evaluated. These are often caused by this kind of usage of 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

Notice how it has to go quite deep before it can get the expression into weak head normal form.

You may wonder, why does not Haskell reduce the inner expressions ahead of time? That is because of Haskell's laziness. Since it cannot be assumed in general that every subexpression will be needed, expressions are evaluated from the outside in.

(GHC has a strictness analyzer that will detect some situations where a subexpression is always needed and it can then evaluate it ahead of time. This is only an optimization, however, and you should not rely on it to save you from overflows).

This kind of expression, on the other hand, is completely safe:

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. 

To avoid building these large expressions when we know all the subexpressions will have to be evaluated, we want to force the inner parts to be evaluated ahead of time.

seq

seq is a special function that is used to force expressions to be evaluated. Its semantics are that seq x y means that whenever y is evaluated to weak head normal form, x is also evaluated to weak head normal form.

It is among other places used in the definition of foldl', the strict variant of foldl.

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

Each iteration of foldl' forces the accumulator to WHNF. It therefore avoids building up a large expression, and it therefore avoids overflowing the stack.

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.

But as the example on HaskellWiki mentions, this does not save you in all cases, as the accumulator is only evaluated to WHNF. In the example, the accumulator is a tuple, so it will only force evaluation of the tuple constructor, and not acc or 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.

To avoid this, we must make it so that evaluating the tuple constructor forces evaluation of acc and len. We do this by using 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.

这篇关于哈斯克尔:什么是弱头正常形式?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!

查看全文
登录 关闭
扫码关注1秒登录
发送“验证码”获取 | 15天全站免登陆