Estou usando o raciocínio equacional do som sobre uma definição de filtro em termos de dobra?

Question

Bem, esta é a definição da função do filtro usando o dobro:

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

Por exemplo, digamos que eu tenho esta função:

myFilter odd [1,2,3,4]

Então será:

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

E isso será

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

E isso será

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

E isso será

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

E isso será

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

e foldr step [] [] é [] assim:

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

Agora vamos realmente entrar no step função.
Aqui está a definição de step dentro de myFilter função, de cima:

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

Além disso, lembro que você p é realmente o odd função em nosso exemplo.

Bem, novamente, estamos aqui:

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

e

x = 4 no mais interno step, e 4 não é estranho, então voltamos ys, qual é []

Então agora entendemos isso:

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

Agora, no mais interno step, x = 3, e 3 é estranho, então voltamos x:ys, qual é 3 : [], qual é [3], e agora temos:

step 1 (step 2 [3])

E agora, no interior step, x = 2, e 2 não é estranho, então voltamos ys, qual é [3], então agora vamos conseguir:

step 1 [3]

e agora, x = 1, e 1 é estranho, então voltamos x : ys, qual é 1 : [3], qual é [1,3].

O fim :-).

Estou certo em todos os meus movimentos?
Muito obrigado :-).

ps a definição de myFilter é do livro MUNDO REAL HASKELL, no capítulo 4.

Answer 1

Isso me parece certo na primeira leitura.

O importante é lembrar que, para alcançar uma avaliação preguiçosa, Haskell realmente analisará as coisas de outra maneira. Em outras palavras, a sequência real é mais parecida

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

torna-se

step 1 <block1>

que se torna

[1, <block1>]

Então, se você tentar puxar o próximo elemento dessa lista, ele avaliará

[1, step 2 <block2>]

que se torna

[1, <block2>]

e depois tentando avaliar

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

torna-se em

[1, step 3 <block3>]

que se torna

[1, 3, <block3>]

etc. Isso demorei um pouco para entender. Foi contra -intuitivo para mim que desde foldr parece ser avaliado a partir do "dentro para fora", mas foldl é avaliado do "exterior em" que foldr seria preguiçoso (o que é), enquanto foldl é rigoroso. Mas se você pensa sobre isso da maneira que descrevi acima, faz sentido (para mim, de qualquer maneira).

Answer 2

Apenas para expandir a ordem de avaliação preguiçosa: basicamente o Haskell sempre avalia a função primeiro, sem olhar para os argumentos até que seja necessário.

Se o resultado da chamada para myFilter é usado (por exemplo, impresso), a função será avaliada na seguinte ordem:

myFilter odd [1,2,3,4]

Primeiro o myFilter A função é avaliada:

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

Agora foldr é a função mais externa e é avaliada:

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

Agora step é avaliado produzindo um 1, desde 1 é estranho:

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

Agora, o primeiro elemento da lista de resultados está disponível e pode ser usado pela função de chamada. Se a função de chamada também usa os seguintes elementos avaliando com o foldr:

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

A avaliação de step Agora não produz novos elementos, já que 2 é par:

1 : foldr step [] [3,4]

Então foldr novamente:

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

Agora avaliando step produz 3:

1 : 3 : foldr step [] [4]

Avaliação foldr;

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

E step mais uma vez:

1 : 3 : foldr step [] []

Finalmente foldr Avalia para uma lista vazia:

1 : 3 : []

Answer 3

À primeira vista, as etapas que você tomou em seu exemplo específico olham corretas individualmente. No entanto, eu gostaria de ressaltar que ambos filter e foldr pode ser aplicado de maneira útil a Listas infinitas-O que deve indicar que a ordem de suas etapas está incorreta no que diz respeito a Haskell.