Que signifie la forme normale de la tête faible (WHNF)? Que signifient la forme normale de la tête (HNF) et la forme normale (NF)?

Le monde réel Haskell déclare:

La fonction seq familière évalue une expression à ce que nous appelons la forme normale de tête (en abrégé HNF). Il s'arrête une fois qu'il atteint le constructeur le plus à l'extérieur (la «tête»). Ceci est distinct de la forme normale (NF), dans laquelle une expression est complètement évaluée.

Vous entendrez également les programmeurs Haskell se référer à la forme normale de tête faible (WHNF). Pour les données normales, la forme normale de la tête faible est la même que la forme normale de la tête. La différence ne se pose que pour les fonctions, et est trop abstraite pour nous concerner ici.

J'ai lu quelques ressources et définitions ( Haskell Wiki et Haskell Mail List et Free Dictionary ) mais je ne les comprends pas. Quelqu'un peut-il peut-être donner un exemple ou donner une définition de profane?

Je suppose que ce serait similaire à:

WHNF = thunk : thunk

HNF = 0 : thunk 

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

Comment faire seqet se ($!)rapporter à WHNF et HNF?

Mettre à jour

Je suis toujours confus. Je sais que certaines des réponses disent d'ignorer HNF. À la lecture des différentes définitions, il semble qu'il n'y ait pas de différence entre les données régulières dans WHNF et HNF. Cependant, il semble qu'il y ait une différence en ce qui concerne une fonction. S'il n'y avait pas de différence, pourquoi est-il seqnécessaire foldl'?

Un autre point de confusion provient du Haskell Wiki, qui déclare que seqréduit à WHNF, et ne fera rien à l'exemple suivant. Ensuite, ils disent qu'ils doivent utiliser seqpour forcer l'évaluation. Cela ne l'oblige-t-il pas à HNF?

Code débordant de pile de débutant commun:

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

Les personnes qui comprennent la forme normale seq et tête faible (whnf) peuvent immédiatement comprendre ce qui ne va pas ici. (acc + x, len + 1) est déjà dans whnf, donc seq, qui réduit une valeur à whnf, n'y fait rien. Ce code créera des thunks comme l'exemple de foldl d'origine, ils seront juste à l'intérieur d'un tuple. La solution consiste simplement à forcer les composants du tuple, par exemple

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

- Haskell Wiki sur Stackoverflow

Je vais essayer de donner une explication en termes simples. Comme d'autres l'ont souligné, la forme normale de la tête ne s'applique pas à Haskell, donc je ne l'examinerai pas ici.

Forme normale

Une expression sous forme normale est entièrement évaluée, et aucune sous-expression n'a pu être évaluée plus avant (c'est-à-dire qu'elle ne contient aucun thunks non évalué).

Ces expressions sont toutes sous forme normale:

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

Ces expressions ne sont pas sous forme normale:

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

Forme normale de la tête faible

Une expression sous forme normale de tête faible a été évaluée pour le constructeur de données le plus à l'extérieur ou l'abstraction lambda (la tête ). Les sous-expressions peuvent ou non avoir été évaluées . Par conséquent, chaque expression de forme normale est également sous forme normale de tête faible, bien que l'inverse ne soit pas vrai en général.

Pour déterminer si une expression est sous une forme normale de tête faible, il suffit de regarder la partie la plus externe de l'expression. S'il s'agit d'un constructeur de données ou d'un lambda, il est sous forme normale de tête faible. Si c'est une application de fonction, ce n'est pas le cas.

Ces expressions sont sous forme normale de tête faible:

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

Comme mentionné, toutes les expressions de forme normale répertoriées ci-dessus sont également sous forme normale de tête faible.

Ces expressions ne sont pas en forme normale de tête faible:

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

Débordements de pile

L'évaluation d'une expression à une forme normale de tête faible peut nécessiter que d'autres expressions soient évaluées en premier au WHNF. Par exemple, pour évaluer 1 + (2 + 3)au WHNF, nous devons d'abord évaluer 2 + 3. Si l'évaluation d'une seule expression conduit à un trop grand nombre de ces évaluations imbriquées, le résultat est un débordement de pile.

Cela se produit lorsque vous créez une grande expression qui ne produit aucun constructeur de données ou lambdas tant qu'une grande partie de celle-ci n'a pas été évaluée. Ceux-ci sont souvent causés par ce type d'utilisation de 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

Remarquez comment il doit aller assez profondément avant qu'il ne puisse obtenir l'expression sous une forme normale de tête faible.

Vous vous demandez peut-être pourquoi Haskell ne réduit pas à l'avance les expressions intérieures? C'est à cause de la paresse de Haskell. Puisqu'on ne peut pas supposer en général que chaque sous-expression sera nécessaire, les expressions sont évaluées de l'extérieur dans.

(GHC a un analyseur de rigueur qui détectera certaines situations où une sous-expression est toujours nécessaire et il peut ensuite l'évaluer à l'avance. Ce n'est qu'une optimisation, cependant, et vous ne devriez pas vous en remettre à vous pour vous sauver des débordements).

Ce type d'expression, en revanche, est totalement sûr:

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. 

Pour éviter de construire ces grandes expressions lorsque nous savons que toutes les sous-expressions devront être évaluées, nous voulons forcer les parties internes à être évaluées à l'avance.

seq

seqest une fonction spéciale qui est utilisée pour forcer les expressions à être évaluées. Sa sémantique seq x ysignifie que chaque fois qu'il yest évalué à une forme normale de tête faible, il xest également évalué à une forme normale de tête faible.

C'est entre autres endroits utilisés dans la définition de foldl', la variante stricte de foldl.

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

Chaque itération de foldl'force l'accumulateur à WHNF. Il évite donc de construire une grande expression, et il évite donc de déborder de la pile.

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.

Mais comme le mentionne l'exemple sur HaskellWiki, cela ne vous sauve pas dans tous les cas, car l'accumulateur n'est évalué qu'en WHNF. Dans l'exemple, l'accumulateur est un tuple, il ne forcera donc que l'évaluation du constructeur de tuple, et non accou 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.

Pour éviter cela, nous devons faire en sorte que l'évaluation du constructeur de tuple force l'évaluation de accet len. Nous le faisons en utilisant 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.

La section sur la forme normale de Thunks and Weak Head dans la description de la paresse de Haskell Wikibooks fournit une très bonne description de WHNF avec cette représentation utile:

Évaluation pas à pas de la valeur (4, [1, 2]). La première étape est complètement non évaluée; toutes les formes suivantes sont en WHNF, et la dernière est également en forme normale.

Les programmes Haskell sont des expressions et ils sont exécutés en effectuant une évaluation .

Pour évaluer une expression, remplacez toutes les applications de fonction par leurs définitions. L'ordre dans lequel vous faites cela n'a pas beaucoup d'importance, mais il est toujours important: commencez par l'application la plus externe et continuez de gauche à droite; c'est ce qu'on appelle l' évaluation paresseuse .

Exemple:

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

L'évaluation s'arrête lorsqu'il n'y a plus d'applications de fonction à remplacer. Le résultat est sous forme normale (ou sous forme normale réduite , RNF). Quel que soit l'ordre dans lequel vous évaluez une expression, vous vous retrouverez toujours avec la même forme normale (mais seulement si l'évaluation se termine).

Il existe une description légèrement différente pour l'évaluation paresseuse. À savoir, il dit que vous devez tout évaluer uniquement sous forme normale de tête faible . Il y a précisément trois cas pour qu'une expression soit dans WHNF:

• Un constructeur: constructor expression_1 expression_2 ...
• Une fonction intégrée avec trop peu d'arguments, comme (+) 2ousqrt
• Une expression lambda: \x -> expression

En d'autres termes, la tête de l'expression (c'est-à-dire l'application de fonction la plus externe) ne peut plus être évaluée, mais l'argument de fonction peut contenir des expressions non évaluées.

Exemples de WHNF:

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

Remarques

1. La "tête" dans WHNF ne fait pas référence à la tête d'une liste, mais à l'application de fonction la plus externe.
2. Parfois, les gens appellent les expressions non évaluées "thunks", mais je ne pense pas que ce soit une bonne façon de le comprendre.
3. La forme normale de la tête (HNF) n'est pas pertinente pour Haskell. Il diffère de WHNF en ce que les corps des expressions lambda sont également évalués dans une certaine mesure.

Une bonne explication avec des exemples est donnée à http://foldoc.org/Weak+Head+Normal+Form La forme normale de tête simplifie même les bits d'une expression à l'intérieur d'une abstraction de fonction, tandis que la forme normale de tête "faible" s'arrête aux abstractions de fonction .

De la source, si vous avez:

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

qui est sous forme normale de tête faible, mais pas sous forme normale de tête ... car l'application possible est coincée à l'intérieur d'une fonction qui ne peut pas encore être évaluée.

La forme normale de la tête réelle serait difficile à mettre en œuvre efficacement. Il faudrait fouiller à l'intérieur des fonctions. Ainsi, l'avantage de la forme normale de la tête faible est que vous pouvez toujours implémenter des fonctions comme un type opaque, et donc qu'il est plus compatible avec les langages compilés et l'optimisation.

Le WHNF ne veut pas que le corps des lambdas soit évalué, donc

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

seq veut que son premier argument soit dans WHNF, donc

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

évalue à

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

au lieu de, ce qui utiliserait HNF

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

En gros, supposons que vous avez une sorte de thunk t.

Maintenant, si nous voulons évaluer tWHNF ou NHF, qui sont les mêmes sauf pour les fonctions, nous trouverions que nous obtenons quelque chose comme

t1 : t2où t1et t2sont les thunks. Dans ce cas, ce t1serait votre 0(ou plutôt un thunk à 0ne pas donner de déballage supplémentaire)

seqet $!évaluer WHNF. Notez que

f $! x = seq x (f x)