Co oznacza postać normalna słaba głowa (WHNF)? Co oznaczają Forma normalna głowy (HNF) i Forma normalna (NF)?

Real World Haskell stwierdza:

Znajoma funkcja seq ocenia wyrażenie do tego, co nazywamy formą głowy normalną (w skrócie HNF). Zatrzymuje się, gdy dotrze do najbardziej zewnętrznego konstruktora („głowy”). Różni się to od postaci normalnej (NF), w której wyrażenie jest całkowicie oceniane.

Usłyszysz także, jak programiści Haskell odnoszą się do normalnej postaci słabej głowy (WHNF). W przypadku normalnych danych słaba postać głowy normalna jest taka sama jak postać głowy normalna. Różnica pojawia się tylko w przypadku funkcji i jest zbyt zawiła, aby nas tutaj martwić.

Przeczytałem kilka zasobów i definicji ( Haskell Wiki i Haskell Mail List oraz bezpłatny słownik ), ale nie rozumiem. Czy ktoś może podać przykład lub podać definicję laika?

Zgaduję, że byłoby to podobne do:

WHNF = thunk : thunk

HNF = 0 : thunk 

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

Jak seqi ($!)odnoszą się do WHNF i HNF?

Aktualizacja

Nadal jestem zdezorientowany. Wiem, że niektóre odpowiedzi mówią, by zignorować HNF. Po przeczytaniu różnych definicji wydaje się, że nie ma różnicy między zwykłymi danymi w WHNF i HNF. Wydaje się jednak, że istnieje różnica w funkcji. Jeśli nie było różnicy, dlaczego jest to seqkonieczne foldl'?

Innym punktem zamieszania jest Wiki Haskell, które stwierdza, że seqogranicza się do WHNF i nie zrobi nic w poniższym przykładzie. Następnie mówią, że muszą użyć, seqaby wymusić ocenę. Czy to nie wymusza na HNF?

Typowy kod przepełnienia stosu początkujących:

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

Ludzie, którzy rozumieją normalną postać sekwoi i słabej głowy (whnf), mogą natychmiast zrozumieć, co się tutaj dzieje. (acc + x, len + 1) jest już w whnf, więc seq, który redukuje wartość do whnf, nic na to nie robi. Ten kod będzie budował thunks, tak jak w oryginalnym przykładzie zwijania, będą one po prostu wewnątrz krotki. Rozwiązaniem jest tylko wymuszenie elementów krotki, np

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

- Wiki Haskell na Stackoverflow

Spróbuję wyjaśnić w prosty sposób. Jak zauważyli inni, głowa w normalnej formie nie dotyczy Haskella, więc nie będę tego tutaj rozważał.

Normalna forma

Wyrażenie w normalnej formie jest w pełni oceniane i żadne podwyrażenie nie może być dalej oceniane (tj. Nie zawiera niezbadanych zespołów).

Wszystkie te wyrażenia są w normalnej formie:

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

Te wyrażenia nie są w normalnej formie:

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

Słaba głowa normalna forma

Wyrażenie w postaci normalnej słabej głowy zostało ocenione do najbardziej zewnętrznego konstruktora danych lub abstrakcji lambda ( głowa ). Podwyrażenia mogły, ale nie musiały być ocenione . Dlatego każde wyrażenie normalnej formy jest również w słabej formie normalnej głowy, chociaż odwrotnie nie ma to miejsca w ogóle.

Aby ustalić, czy wyrażenie ma słabą głowę w normalnej formie, musimy spojrzeć tylko na najbardziej zewnętrzną część wyrażenia. Jeśli jest to konstruktor danych lub lambda, ma on normalną słabą głowę. Jeśli jest to aplikacja funkcyjna, nie jest.

Te wyrażenia są w normalnej formie słabej głowy:

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

Jak wspomniano, wszystkie wyżej wymienione wyrażenia w postaci normalnej są również w słabej postaci normalnej.

Te wyrażenia nie są w normalnej formie słabej głowy:

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

Przepełnienie stosu

Ocena wyrażenia do postaci normalnej słabej głowy może wymagać uprzedniej oceny innych wyrażeń w WHNF. Na przykład, aby ocenić 1 + (2 + 3)WHNF, musimy najpierw ocenić 2 + 3. Jeśli ocena pojedynczego wyrażenia prowadzi do zbyt wielu z tych zagnieżdżonych ocen, wynikiem jest przepełnienie stosu.

Dzieje się tak, gdy budujesz duże wyrażenie, które nie generuje żadnych konstruktorów danych ani lambd, dopóki duża jego część nie zostanie oceniona. Są one często spowodowane przez tego rodzaju użycie 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

Zwróć uwagę, jak musi sięgać dość głęboko, zanim zdoła uzyskać wyraz w normalnej formie słabej głowy.

Możesz się zastanawiać, dlaczego Haskell nie zmniejsza z wyprzedzeniem wewnętrznych wyrażeń? Wynika to z lenistwa Haskella. Ponieważ ogólnie nie można założyć, że każde podwyrażenie będzie potrzebne, wyrażenia są oceniane z zewnątrz w.

(GHC ma analizator dokładności, który wykryje pewne sytuacje, w których podwyrażenie jest zawsze potrzebne, i może następnie ocenić je z wyprzedzeniem. Jest to jednak tylko optymalizacja i nie powinieneś na nim polegać, aby uchronić Cię przed przepełnieniem).

Z drugiej strony tego rodzaju wyrażenie jest całkowicie bezpieczne:

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. 

Aby uniknąć budowania tych dużych wyrażeń, gdy wiemy, że wszystkie podwyrażenia będą musiały zostać ocenione, chcemy zmusić wewnętrzne części do oceny przed czasem.

seq

seqto specjalna funkcja używana do wymuszania oceny wyrażeń. Jego semantyka seq x yoznacza, że ​​ilekroć yjest oceniana jako słaba głowa w normalnej formie, xjest również oceniana w postaci słabej głowa w normalnej formie.

Jest to między innymi miejsca stosowane w definicji foldl'ścisłego wariantu foldl.

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

Każda iteracja foldl'zmusza akumulator do WHNF. W ten sposób unika się tworzenia dużego wyrażenia, a zatem unika się przepełnienia stosu.

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.

Ale jak wspomina przykład w HaskellWiki, nie oszczędza cię to we wszystkich przypadkach, ponieważ akumulator jest oceniany tylko do WHNF. W tym przykładzie akumulator jest krotką, więc wymusi jedynie ocenę konstruktora krotki, a nie acclub 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.

Aby tego uniknąć, musimy sprawić, aby ocena konstruktora krotek wymusiła ocenę acci len. Robimy to za pomocą 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.

Część opisująca lenistwo w Haskell Wikibooks w sekcji Normalne formy Thunks and Weak Head Normal zapewnia bardzo dobry opis WHNF wraz z tym pomocnym przedstawieniem:

Szacowanie wartości (4, [1, 2]) krok po kroku. Pierwszy etap jest całkowicie nieoceniony; wszystkie kolejne formy są w WHNF, a ostatnia jest również w normalnej formie.

Programy Haskell są wyrażeniami i są uruchamiane przez wykonanie oceny .

Aby ocenić wyrażenie, zastąp wszystkie aplikacje funkcyjne ich definicjami. Kolejność, w jakiej to robisz, nie ma większego znaczenia, ale nadal jest ważna: zacznij od aplikacji zewnętrznej i przejdź od lewej do prawej; nazywa się to leniwą oceną .

Przykład:

   take 1 (1:2:3:[])
=> { apply take }
   1 : take (1-1) (2:3:[])
=> { apply (-)  }
   1 : take 0 (2:3:[])
=> { apply take }
   1 : []

Ocena zostaje zatrzymana, gdy nie ma już więcej aplikacji funkcyjnych do zastąpienia. Wynik ma postać normalną (lub zmniejszoną postać normalną , RNF). Bez względu na to, w jakiej kolejności oceniasz wyrażenie, zawsze będziesz mieć taką samą normalną formę (ale tylko wtedy, gdy ocena się zakończy).

Istnieje nieco inny opis leniwej oceny. Mianowicie mówi, że wszystko należy oceniać tylko do słabej głowy w normalnej formie . Istnieją dokładnie trzy przypadki wyrażenia w WHNF:

• Konstruktor: constructor expression_1 expression_2 ...
• Wbudowana funkcja ze zbyt małą liczbą argumentów, takich jak (+) 2lubsqrt
• Wyrażenie lambda: \x -> expression

Innymi słowy, głowa wyrażenia (tj. Najbardziej zewnętrzna aplikacja funkcji) nie może być dalej oceniana, ale argument funkcji może zawierać nieocenione wyrażenia.

Przykłady WHNF:

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

Notatki

1. „Head” w WHNF nie odnosi się do nagłówka listy, ale do aplikacji funkcji peryferyjnej.
2. Czasami ludzie nazywają nieocenione wyrażenia „zgrzytami”, ale nie sądzę, żeby to był dobry sposób na ich zrozumienie.
3. Hask normalna postać (HNF) nie ma znaczenia. Różni się od WHNF tym, że ciała wyrażeń lambda są również do pewnego stopnia oceniane.

Dobre wyjaśnienie z przykładami podano na stronie http://foldoc.org/Weak+Head+Normal+Form Forma normalna głowy upraszcza nawet fragmenty wyrażenia wewnątrz abstrakcji funkcji, podczas gdy „słaba” forma normalna głowy zatrzymuje się przy abstrakcjach funkcji .

Ze źródła, jeśli masz:

\ x -> ((\ y -> y+x) 2)

to jest w normalnej formie słabej głowy, ale nie w normalnej formie głowy ... ponieważ możliwa aplikacja utknęła w funkcji, której nie można jeszcze ocenić.

Rzeczywista normalna forma głowy byłaby trudna do skutecznego wdrożenia. Wymagałoby to szukania wewnątrz funkcji. Zaletą słabej głowy normalnej formy jest to, że nadal można implementować funkcje jako nieprzezroczyste, a zatem jest ona bardziej kompatybilna z kompilowanymi językami i optymalizacją.

WHNF nie chce oceniać ciała lambdów, więc

WHNF = \a -> thunk
HNF = \a -> a + c

seq chce, aby jego pierwszy argument był w WHNF, więc

let a = \b c d e -> (\f -> b + c + d + e + f) b
    b = a 2
in seq b (b 5)

ocenia na

\d e -> (\f -> 2 + 5 + d + e + f) 2

zamiast tego, co będzie używać HNF

\d e -> 2 + 5 + d + e + 2

Zasadniczo, załóżmy, że masz jakieś thunk, t.

Teraz, jeśli chcemy ocenić tWHNF lub NHF, które są takie same, z wyjątkiem funkcji, stwierdzilibyśmy, że otrzymujemy coś takiego

t1 : t2gdzie t1i t2są gromady. W tym przypadku t1byłby to twój 0(a raczej 0niezły bzdurny brak dodatkowego rozpakowania)

seqi $!ewaluować WHNF. Zauważ, że

f $! x = seq x (f x)