haskell - la función seq y el rigor

strict

Question

Me he estado preguntando mucho sobre esto, pero no he podido encontrar nada al respecto.

Cuando se usa la función seq , ¿cómo funciona realmente ? En todas partes, solo se explica diciendo que el seq ab evalúa a , descarta el resultado y lo devuelve b .

Pero, ¿qué significa eso realmente ? El siguiente resultado en una evaluación estricta:

foo s t = seq q (bar q t) where
      q = s*t

Lo que quiero decir es q es estrictamente evaluado antes de ser utilizado en la bar ? Y los siguientes serían equivalentes:

foo s t = seq (s*t) (bar (s*t) t)

Me resulta un poco difícil obtener detalles sobre la funcionalidad de esta función.

Answer 1

No estas solo. seq es probablemente una de las funciones de Haskell más difíciles de usar correctamente, por varias razones diferentes. En tu primer ejemplo:

foo s t = seq q (bar q t) where
      q = s*t

q se evalúa antes de evaluar bar qt . Si bar qt nunca se evalúa, q tampoco lo será. Entonces si tienes

main = do
    let val = foo 10 20
    return ()

como val nunca se usa, no se evaluará. Entonces q no será evaluado tampoco. Si en cambio tienes

main = print (foo 10 20)

el resultado de foo 10 20 se evalúa (por print ), por lo que dentro de foo q se evalúa antes del resultado de la bar .

Esta es también la razón por la que esto no funciona:

myseq x = seq x x

Semánticamente, esto significa que las primeras x serán evaluadas antes de que se evalúe la segunda x . Pero si la segunda x nunca se evalúa, tampoco es necesario que la primera sea. Entonces, seq xx es exactamente equivalente a x .

Su segundo ejemplo puede o no ser lo mismo. Aquí, la expresión s*t se evaluará antes de la salida de la bar , pero puede no ser la misma s*t que el primer parámetro de la bar . Si el compilador realiza una eliminación común de sub-expresiones, puede que las dos expresiones comunes sean comunes. Sin embargo, GHC puede ser bastante conservador acerca de dónde hace CSE, por lo que no puede confiar en esto. Si defino bar qt = q*t , realiza el CSE y evalúa s*t antes de usar ese valor en la barra. Puede que no lo haga para expresiones más complejas.

También es posible que desee saber qué se entiende por evaluación estricta . seq evalúa el primer argumento a la forma normal de cabeza débil (WHNF), que para los tipos de datos significa desempaquetar el constructor más externo. Considera esto:

baz xs y = seq xs (map (*y) xs)

xs debe ser una lista, debido al map . Cuando seq evalúa, esencialmente transformará el código en

case xs of
  [] -> map (*y) xs
  (_:_) -> map (*y) xs

Esto significa que determinará si la lista está vacía o no, luego devuelve el segundo argumento. Tenga en cuenta que ninguno de los valores de la lista se evalúa . Entonces puedes hacer esto:

Prelude> seq [undefined] 4
4

pero no esto

Prelude> seq undefined 5
*** Exception: Prelude.undefined

Sea cual sea el tipo de datos que utilice para el primer argumento de seq , evaluar a WHNF irá lo suficientemente lejos como para descubrir el constructor y no más. A menos que el tipo de datos tenga componentes marcados como estrictos con un patrón bang. Entonces todos los campos estrictos también se evaluarán a WHNF.

Editar: (gracias a Daniel Wagner por su sugerencia en los comentarios)

Para las funciones, seq evaluará la expresión hasta que la función "muestre una lambda", lo que significa que está lista para la aplicación. Aquí hay algunos ejemplos que pueden demostrar lo que esto significa:

-- ok, lambda is outermost
Prelude> seq (/x -> undefined) ''a''
''a''

-- not ok.  Because of the inner seq, `undefined` must be evaluated before
-- the lambda is showing
Prelude> seq (seq undefined (/x -> x)) ''b''
*** Exception: Prelude.undefined

Si piensa en un enlace lambda como un constructor de datos (integrado), la función seq en las funciones es perfectamente consistente con su uso en datos.

Además, el "enlace lambda" abarca todos los tipos de definiciones de funciones, ya sea definidas por la notación lambda o como una función normal.

La sección Controversy de la página sek de HaskellWiki tiene un poco sobre algunas de las consecuencias de seq en relación con las funciones.

Answer 2

Puedes pensar en seq como:

seq a b = case a of
            _ -> b

Esto evaluará a de cabeza normal (WHNF) y luego continuará con la evaluación de b .

Editar después de un comentario augusto: este case ... of es el estricto, GHC Core one , que siempre fuerza su argumento.