haskell - 我是否使用合理的等式推理来根据 foldr 定义过滤器？

Question

好吧，这是使用 foldr 的过滤器函数的定义:

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

所以例如假设我有这个功能:

myFilter odd [1,2,3,4]

所以它将是:

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

这将是

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

这将是

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

这将是

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

这将是

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

和 foldr step [] []是 []所以:

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

现在我们将真正进入 step功能。
这是 step的定义里面 myFilter功能，从上面:

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

另外，我提醒你 p实际上是 odd在我们的例子中起作用。

好吧，我们又来了:

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

和
x = 4在最里面 step , 和 4不奇怪，所以我们返回 ys ，即 []
所以现在我们得到了这个:

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

现在，在最内心的 step , x = 3 , 和 3是奇数，所以我们返回 x:ys ，即 3 : [] ，即 [3] ，现在我们得到:

step 1 (step 2 [3])

现在，在内部 step , x = 2 , 和 2并不奇怪，所以我们返回 ys ，即 [3] ，所以现在我们将得到:

step 1 [3]

现在， x = 1 , 和 1是奇数，所以我们返回 x : ys ，即 1 : [3] ，即 [1,3] .

结束 :-)。

我的所有 Action 都正确吗？
多谢 :-)。

p.s. myFilter的定义来自书 Real World Haskell ，在第 4 章。

Answer 1

初读时这对我来说是正确的。

不过要记住的重要一点是，为了实现惰性求值，Haskell 实际上会以另一种方式看待事物。换句话说，真实的序列更像

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

变成

step 1 <block1>

变成

[1, <block1>]

然后，如果您尝试从该列表中提取下一个元素，它将评估

[1, step 2 <block2>]

变成

[1, <block2>]

然后尝试评估

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

变成

[1, step 3 <block3>]

变成

[1, 3, <block3>]

等等。我花了一段时间才明白。从 foldr 开始，这对我来说是违反直觉的。似乎是从“由内而外”评估的，但 foldl从 foldr 的“外在”进行评估会很懒(确实如此)，而 foldl是严格的。但是，如果您按照我上面概述的方式来思考它，那是有道理的(无论如何，对我来说)。