Was ist schwache Kopfnormalform?

Ich werde versuchen, eine Erklärung in einfachen Worten zu geben. Wie bereits erwähnt, trifft die normale Kopfform auf Haskell nicht zu, weshalb ich hier nicht darauf eingehen werde.

Normalform

Ein Ausdruck in normaler Form wird vollständig ausgewertet, und kein Unterausdruck kann weiter ausgewertet werden (d. H. Er enthält keine nicht ausgewerteten Thunks).

Diese Ausdrücke sind alle in normaler Form:

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

Diese Ausdrücke sind nicht in normaler 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

Schwacher Kopf normale Form

Ein Ausdruck in schwacher Kopfnormalform wurde für den äußersten Datenkonstruktor oder die Lambda-Abstraktion (Kopf) ausgewertet. Unterausdrücke können ausgewertet worden sein oder nicht. Daher hat jeder Ausdruck in normaler Form auch eine schwache Kopfnormalform, obwohl das Gegenteil im Allgemeinen nicht zutrifft.

Um festzustellen, ob ein Ausdruck eine schwache Kopfnormalform hat, müssen wir nur den äußersten Teil des Ausdrucks betrachten. Wenn es sich um einen Datenkonstruktor oder ein Lambda handelt, weist es eine normale Kopfschwäche auf. Wenn es sich um eine Funktionsanwendung handelt, ist dies nicht der Fall.

Diese Ausdrücke haben eine schwache Kopfnormalform:

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

Wie bereits erwähnt, haben alle oben aufgeführten Normalformausdrücke auch eine Normalform mit schwachem Kopf.

Diese Ausdrücke haben keine schwache Kopfnormalform:

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

Stapel läuft über

Die Auswertung eines Ausdrucks in schwacher Kopfnormalform erfordert möglicherweise, dass andere Ausdrücke zuerst als WHNF ausgewertet werden. Um beispielsweise 1 + (2 + 3) zu WHNF auszuwerten, müssen wir zuerst 2 + 3 Auswerten. Wenn die Auswertung eines einzelnen Ausdrucks zu vielen dieser verschachtelten Auswertungen führt, ist das Ergebnis ein Stapelüberlauf.

Dies passiert, wenn Sie einen großen Ausdruck erstellen, der keine Datenkonstruktoren oder Lambdas erzeugt, bis ein großer Teil davon ausgewertet wurde. Diese werden häufig durch diese Art der Verwendung von foldl verursacht:

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

Beachten Sie, wie tief es gehen muss, bevor es den Ausdruck in die normale Form eines schwachen Kopfes bringen kann.

Sie fragen sich vielleicht, warum Haskell die inneren Ausdrücke nicht vorzeitig reduziert? Das liegt an Haskells Faulheit. Da nicht generell davon ausgegangen werden kann, dass jeder Teilausdruck benötigt wird, werden Ausdrücke von außen nach innen ausgewertet.

(GHC verfügt über einen Strenge-Analysator, der Situationen erkennt, in denen immer ein Teilausdruck benötigt wird, und diesen vorab auswertet. Dies ist jedoch nur eine Optimierung, und Sie sollten sich nicht darauf verlassen, dass Sie vor Überläufen geschützt sind.).

Diese Art von Ausdruck ist dagegen völlig ungefährlich:

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. 

Um zu vermeiden, dass diese großen Ausdrücke erstellt werden, wenn wir wissen, dass alle Unterausdrücke ausgewertet werden müssen, möchten wir erzwingen, dass die inneren Teile vorab ausgewertet werden.

seq

seq ist eine spezielle Funktion, mit der die Auswertung von Ausdrücken erzwungen wird. Die Semantik besagt, dass seq x y Bedeutet, dass jedes Mal, wenn y als Normalform für schwache Köpfe ausgewertet wird, x auch als Normalform für schwache Köpfe ausgewertet wird.

Es wird unter anderem in der Definition von foldl', Der strengen Variante von foldl, verwendet.

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

Jede Iteration von foldl' Zwingt den Akkumulator auf WHNF. Es wird daher vermieden, einen großen Ausdruck aufzubauen, und es wird daher ein Überlaufen des Stapels vermieden.

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.

Wie im Beispiel in HaskellWiki erwähnt, werden Sie dadurch jedoch nicht in allen Fällen gespart, da der Akku nur nach WHNF ausgewertet wird. In diesem Beispiel ist der Akkumulator ein Tupel, sodass nur die Auswertung des Tupel-Konstruktors erzwungen wird und nicht acc oder 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.

Um dies zu vermeiden, müssen wir den Tuple-Konstruktor so einstellen, dass er die Auswertung von acc und len erzwingt. Wir tun dies mit 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.