1. ホーム

[解決済み】Weak Head Normal Formとは何ですか?

2022-03-28 08:42:13

質問

って何? 弱頭正常形 (WHNF)とはどういう意味ですか?また ヘッドノーマル形式 (HNF)と 正規形 (NF)とはどういう意味ですか?

リアルワールドハスケル の状態になります。

おなじみの  seq  関数は、式を評価し と呼ぶ  主正規形  (HNFと略す)。HNFは一旦停止します。 は、一番外側のコンストラクタ("head")です。これは  通常の フォーム  (NF)と呼ばれるもので、式が完全に評価される。

また、Haskellプログラマーが  弱い  ヘッドノーマル 形式(WHNF)です。通常のデータでは、弱い先頭の正規形は となります。この違いは関数の場合のみであり、あまりに重要である。 は、ここでは割愛する。

いくつかの資料や定義を読みました( ハスケルWiki ハスケルメールリスト 無料辞書 ) が、よくわからない。どなたか例を挙げていただくか、素人の定義を教えていただけませんか?

と同じようなものだろうと推測しています。

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  (の定義にある)。  foldl' ) は、値を whnf に還元しますが、これには何もしません。このコードでは、元の  foldl  の例では、タプルの中に入っているだけです。解決策は、単に のコンポーネントは、タプルを構成します。

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

- Haskell Wiki on Stackoverflow

どのように解決するのですか?

わかりやすく解説していこうと思います。他の方も指摘されているように、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

弱頭正常形

weak head normal form の式は、一番外側のデータコンストラクタまたはラムダ抽象化式 ( ヘッド ). 副式 は評価されているかどうか . したがって、すべての正規形の式は弱頭正規形でもあるが、一般にその逆は成り立たない。

ある式が弱頭正規形かどうかを判断するには、式の一番外側を見ればいいのです。データコンストラクタやラムダであれば、弱頭正規形である。関数アプリケーションの場合は、弱頭正規形ではありません。

これらの式は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 (:)

前述のように、上に挙げた正規形の式はすべて弱頭正規形でもある。

これらの式は弱首尾正規形ではありません。

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 . 一つの式を評価する際に、このような入れ子式の評価が多くなると、スタックオーバーフローとなる。

これは、大きな式を構築して、その大部分が評価されるまでデータコンストラクタやラムダが生成されない場合に発生します。これらは、このような 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

この式がweak head normal formになる前に、かなり深く入り込まなければならないことに注意してください。

なぜ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 もweak head normal formとして評価されます。

の定義で使用されている他の場所です。 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.

これを避けるには、タプルコンストラクタを評価すると、強制的に acclen . これを行うには 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.