haskell definition strictness weak-head-normal-form

Haskell: ¿Qué es la forma normal de cabeza débil?



definition strictness (6)

¿Qué significa la forma normal de cabeza débil (WHNF)? ¿Qué significa la forma normal de la cabeza (HNF) y la forma normal (NF)?

El mundo real Haskell afirma:

La función seq familiar evalúa una expresión a lo que llamamos cabeza forma normal (abreviado HNF). Se detiene una vez que llega al constructor más externo (la "cabeza"). Esto es distinto de la forma normal (NF), en la que una expresión se evalúa por completo.

También escuchará a los programadores de Haskell referirse a la forma normal de cabeza débil (WHNF). Para datos normales, la forma normal de la cabeza débil es la misma que la forma normal de la cabeza. La diferencia solo surge para las funciones, y es demasiado compleja para preocuparnos aquí.

He leído algunos recursos y definiciones ( Haskell Wiki y Haskell Mail List y Free Dictionary ) pero no lo entiendo. ¿Alguien puede dar un ejemplo o proporcionar una definición laica?

Supongo que sería similar a:

WHNF = thunk : thunk HNF = 0 : thunk NF = 0 : 1 : 2 : 3 : []

¿Cómo se relacionan seq y ($!) WHNF y HNF?

Actualizar

Todavía estoy confundido. Sé que algunas de las respuestas dicen ignorar HNF. De la lectura de las diversas definiciones, parece que no hay diferencia entre los datos regulares en WHNF y HNF. Sin embargo, parece que hay una diferencia cuando se trata de una función. Si no hubo diferencia, ¿por qué es necesario para el foldl'' ?

Otro punto de confusión es el de Haskell Wiki, que establece que seq reduce a WHNF, y no hará nada con el siguiente ejemplo. Luego dicen que tienen que usar seq para forzar la evaluación. ¿No es eso forzarlo a HNF?

Código de desbordamiento de pila de principiante común:

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

Las personas que entienden la forma normal de la cabeza seq y débil (whnf) pueden entender inmediatamente lo que va mal aquí. (acc + x, len + 1) ya está en whnf, por lo que seq, que reduce un valor a whnf, no hace nada para esto. Este código creará thunks al igual que el ejemplo original de foldl, simplemente estarán dentro de una tupla. La solución es simplemente forzar los componentes de la tupla, por ejemplo,

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

- Haskell Wiki en Stackoverflow

Básicamente, supongamos que tienes algún tipo de thunk, t .

Ahora, si queremos evaluar t a WHNF o NHF, que son las mismas a excepción de las funciones, encontraremos que obtenemos algo como

t1 : t2 donde t1 y t2 son thunks. En este caso, t1 sería su 0 (o, mejor dicho, un thunk a 0 dado que no hay unboxing extra)

seq y $! evalute WHNF. Tenga en cuenta que

f $! x = seq x (f x)

El WHNF no quiere que el cuerpo de lambdas sea evaluado, por lo que

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

seq quiere que su primer argumento esté en WHNF, por lo que

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

evalúa a

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

en lugar de, lo que estaría usando HNF

/d e -> 2 + 5 + d + e + 2

La sección sobre Thunks y la forma normal de cabeza débil en la descripción de la holgazanería de Haskell Wikilibros proporciona una muy buena descripción de WHNF junto con esta descripción útil:

Evaluando el valor (4, [1, 2]) paso a paso. La primera etapa está completamente sin evaluar; todas las formas subsiguientes están en WHNF, y la última también está en forma normal.

Los programas de Haskell son expresiones y se ejecutan realizando una evaluación .

Para evaluar una expresión, reemplace todas las aplicaciones de función por sus definiciones. El orden en el que haces esto no importa mucho, pero sigue siendo importante: comienza con la aplicación más externa y avanza de izquierda a derecha; Esto se llama evaluación perezosa .

Ejemplo:

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

La evaluación se detiene cuando ya no quedan más aplicaciones de función que reemplazar. El resultado está en forma normal (o forma normal reducida , RNF). No importa en qué orden evalúe una expresión, siempre terminará con la misma forma normal (pero solo si la evaluación finaliza).

Hay una descripción ligeramente diferente para la evaluación perezosa. Es decir, dice que debe evaluar todo a la forma normal de cabeza débil solamente. Hay exactamente tres casos para que una expresión esté en WHNF:

  • Un constructor: constructor expression_1 expression_2 ...
  • Una función incorporada con muy pocos argumentos, como (+) 2 o sqrt
  • Una expresión lambda: /x -> expression

En otras palabras, el encabezado de la expresión (es decir, la aplicación de la función más externa) no puede evaluarse más, pero el argumento de la función puede contener expresiones no evaluadas.

Ejemplos de WHNF:

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

Notas

  1. El "encabezado" en WHNF no se refiere al encabezado de una lista, sino a la aplicación de función más externa.
  2. A veces, las personas denominan expresiones no evaluadas "thunks", pero no creo que sea una buena manera de entenderlo.
  3. La forma normal de la cabeza (HNF) es irrelevante para Haskell. Se diferencia de WHNF en que los cuerpos de las expresiones lambda también se evalúan en cierta medida.

Trataré de dar una explicación en términos simples. Como otros han señalado, la forma normal de la cabeza no se aplica a Haskell, por lo que no lo consideraré aquí.

Forma normal

Una expresión en forma normal se evalúa por completo, y ninguna subexpresión podría evaluarse más (es decir, no contiene thunks no evaluados).

Estas expresiones son todas en forma normal:

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

Estas expresiones no están en forma normal:

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

Forma normal de la cabeza débil

Se ha evaluado una expresión en forma normal de cabeza débil para el constructor de datos más externo o la abstracción lambda (la cabeza ). Las sub-expresiones pueden o no haber sido evaluadas . Por lo tanto, toda expresión de forma normal también tiene una forma normal de cabeza débil, aunque en general no ocurre lo contrario.

Para determinar si una expresión tiene una forma normal de cabeza débil, solo tenemos que mirar la parte más externa de la expresión. Si es un constructor de datos o un lambda, tiene una forma normal de cabeza débil. Si es una aplicación de función, no lo es.

Estas expresiones están en forma normal de cabeza débil:

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

Como se mencionó, todas las expresiones de formas normales enumeradas anteriormente también tienen una forma normal de cabeza débil.

Estas expresiones no están en forma normal de cabeza débil:

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

Desbordamientos de pila

La evaluación de una expresión a la forma normal de cabeza débil puede requerir que otras expresiones se evalúen primero a WHNF. Por ejemplo, para evaluar 1 + (2 + 3) a WHNF, primero tenemos que evaluar 2 + 3 . Si la evaluación de una sola expresión conduce a demasiadas de estas evaluaciones anidadas, el resultado es un desbordamiento de pila.

Esto sucede cuando creas una expresión grande que no produce ningún constructor de datos o lambdas hasta que una gran parte de ella haya sido evaluada. Estos son a menudo causados ​​por este tipo de uso 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

Observe cómo debe ir bastante profundo antes de que la expresión se convierta en una forma normal de cabeza débil.

Usted puede preguntarse, ¿por qué Haskell no reduce las expresiones internas antes de tiempo? Eso es debido a la pereza de Haskell. Como no se puede suponer en general que se necesitará cada subexpresión, las expresiones se evalúan desde el exterior hacia adentro.

(GHC tiene un analizador de rigor que detectará algunas situaciones en las que siempre se necesita una subexpresión y luego puede evaluarla antes de tiempo. Sin embargo, esta es solo una optimización y no debe confiar en ella para evitarle desbordamientos).

Este tipo de expresión, por otro lado, es completamente seguro:

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.

Para evitar la construcción de estas expresiones grandes cuando sabemos que todas las subexpresiones tendrán que ser evaluadas, queremos forzar a las partes internas a ser evaluadas con anticipación.

seq

seq es una función especial que se usa para forzar que las expresiones sean evaluadas. Su semántica es que seq xy significa que cada vez que y se evalúa como forma normal de cabeza débil, x también se evalúa como forma normal de cabeza débil.

Es, entre otros lugares, utilizado en la definición de foldl'' , la variante estricta de foldl .

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

Cada iteración de foldl'' obliga al acumulador a WHNF. Por lo tanto, evita construir una expresión grande, y por lo tanto evita desbordar la pila.

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.

Pero como lo menciona el ejemplo en HaskellWiki, esto no te salva en todos los casos, ya que el acumulador solo se evalúa como WHNF. En el ejemplo, el acumulador es una tupla, por lo que solo forzará la evaluación del constructor de tuplas, y no acc o 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.

Para evitar esto, debemos hacer que la evaluación del constructor de tuplas obligue a la evaluación de acc y len . Hacemos esto usando 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.

Una buena explicación con ejemplos se da en http://foldoc.org/Weak+Head+Normal+Form La forma normal de la cabeza simplifica incluso los bits de una expresión dentro de la abstracción de una función, mientras que la forma normal de la cabeza "débil" se detiene en las abstracciones de la función .

Desde la fuente, si tiene:

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

eso es en forma normal de cabeza débil, pero no en forma normal de cabeza ... porque la posible aplicación está bloqueada dentro de una función que aún no se puede evaluar.

La forma normal de la cabeza real sería difícil de implementar de manera eficiente. Requeriría hurgando dentro de las funciones. Entonces, la ventaja de la forma normal de cabeza débil es que aún puede implementar funciones como un tipo opaco, y por lo tanto es más compatible con los lenguajes compilados y la optimización.