¿Estoy usando el razonamiento de sonido ecuacional sobre una definición de filtro en términos de foldr?

Question

así, esta es la definición de la función de filtro utilizando foldr:

myFilter p xs = foldr step [] xs 
    where step x ys | p x  = x : ys 
        | otherwise = ys 

así por ejemplo digamos que tengo esta función:

myFilter odd [1,2,3,4] 

por lo que será:

foldr step [] [1,2,3,4] 

y esto será

step 1 (foldr step [] [2,3,4]) 

y esto será

step 1 (step 2 (foldr step [] [3,4])) 

y esto será

step 1 (step 2 (step 3 (foldr step [] [4]))) 

y esto será

step 1 (step 2 (step 3 (step 4 (foldr step [] [])))) 

y foldr step [] [] es [] modo:

step 1 (step 2 (step 3 (step 4 []))) 

ahora entraremos en la función step.
aquí es la definición de step dentro de la función myFilter, desde arriba:

step x ys | p x  = x : ys 
      | otherwise = ys 

también, le recuerdo que p es en realidad la función odd en nuestro ejemplo. No

step 1 (step 2 (step 3 (step 4 []))) 

y

x = 4 en el más interno step y 4 es impar, así que volviendo ys, que es []

:

así, una vez más, estamos aquí por lo que ahora tenemos esto:

step 1 (step 2 (step 3 [])) 

ahora, en el más interno step, x = 3 y 3 es impar, por lo que volver x:ys, que es 3 : [], que es [3], y ahora tenemos:

step 1 (step 2 [3]) 

y ahora, en el interior step, x = 2 y 2 no es extraño, por lo que volver ys, que es [3], por lo que ahora vamos a obtener:

step 1 [3] 

y ahora, x = 1 y 1 es impar, por lo que volver x : ys, que es 1 : [3], que es [1,3].

Fin :-).

¿estoy en todos mis movimientos?
muchas gracias :-).

p.s. la definición de myFilter es del libro Real World Haskell, en el capítulo 4.

Answer 1

Esto me parece a mí en la primera lectura.

Lo importante a recordar es que para lograr una evaluación lenta, Haskell realmente verá las cosas de otra manera. En otras palabras, la secuencia real es más como

step 1 (step 2 (step 3 (step 4 []))) 

convierte

step 1 <block1> 

que se convierte en

[1, <block1>] 

continuación, si se intenta tirar del siguiente elemento de esa lista, se evaluará

[1, step 2 <block2>] 

, que se convierte en

[1, <block2>] 

y luego tratar de evaluar

[1, step 3 (step 4 [])] 

convierte en

[1, step 3 <block3>] 

que se convierte en

[1, 3, <block3>] 

etc. Esto me llevó un tiempo entender. Era contradictorio para mí que desde foldr parece evaluarse desde el "adentro hacia afuera" pero foldl se evalúa desde el "exterior en" que foldr sería flojo (lo cual es), mientras que foldl es estricto. Pero si lo piensas de la manera que describí arriba, tiene sentido (para mí, de todos modos).

Answer 2

A primera vista, los pasos que ha seguido en su ejemplo específico parecen correctos individualmente. Sin embargo, me gustaría señalar que tanto filter como foldr se pueden aplicar de manera útil a listas infinitas, lo que debería indicar que el orden de los pasos es incorrecto en lo que respecta a Haskell.

Answer 3

Solo para ampliar el orden de evaluación diferida: básicamente, Haskell siempre evalúa la función primero, sin mirar los argumentos hasta que no tenga que hacerlo.

Si se utiliza el resultado de la llamada a myFilter (por ejemplo impreso), la función se evaluará en el siguiente orden:

myFilter odd [1,2,3,4] 

primer lugar la función de myFilter se evalúa:

foldr step [] [1,2,3,4] 

Ahora foldr es la función más externa y se evalúa:

step 1 (foldr step [] [2,3,4]) 

Ahora step consigue evaluó la producción de un 1, ya 1 es impar:

1 : foldr step [] [2,3,4] 

Ahora el primer elemento de la lista de resultados está disponible y puede ser utilizado por la función de llamada. Si la función de llamada utiliza también elementos de la siguiente evaluación continúa con el foldr:

1 : step 2 (foldr step [] [3,4]) 

La evaluación de step ahora no produce ningún elemento nuevo, ya que 2 es par:

1 : foldr step [] [3,4] 

Así foldr de nuevo:

1 : step 3 (foldr step [] [4]) 

Ahora evaluar step produce 3:

1 : 3 : foldr step [] [4] 

Evaluación de foldr;

1 : 3 : step 4 (foldr step [] []) 

Y step una vez más:

1 : 3 : foldr step [] [] 

Finalmente foldr evalúa a una lista vacía:

1 : 3 : []