我是否使用合理的等式推理来根据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 1 (step 2 (step 3 (step 4 [])))

现在我们将真正进入 step 函数。
这是 myFilter 函数中 step 的定义，来自上面：

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

另外，我提醒你，p 实际上是 odd<我们示例中的 /code> 函数。

好吧，我们又在这里：

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

并且

x = 4 在最里面的 step 中，并且 4 并不奇怪，所以我们返回 < code>ys，即 []

所以现在我们得到：

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

现在，在最里面的 step 中，x = 3 ，而 3 是奇数，因此我们返回 x:ys，即 3 : []，即 [3]< /code>，现在我们得到：

step 1 (step 2 [3])

现在，在内部步骤中，x = 2，并且2并不奇怪，所以我们返回 ys，即 [3]，所以现在我们将得到：

step 1 [3]

现在，x = 1 和 1< /code> 是奇数，因此我们返回 x : ys，即 1 : [3]，即 [1,3]。

结束:-)。

我的所有举动都正确吗？
多谢 ：-）。

ps 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 是严格的。但如果你按照我上面概述的方式思考它，那就有道理了（无论如何对我来说）。

Answer 2

只是为了扩展惰性计算顺序：基本上 Haskell 总是首先计算函数，直到必要时才查看参数。

如果使用 myFilter 调用的结果（例如打印），则将按以下顺序计算该函数：

myFilter odd [1,2,3,4]

首先计算 myFilter 函数：

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

现在 foldr 是最外面的函数并被求值：

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

现在 step 被求值，生成 1，因为 1 是奇数：

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

现在结果列表的第一个元素可用并且可由调用函数使用。如果调用函数还使用以下元素，则评估继续
使用 foldr：

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

对 step 的评估现在不会产生任何新元素，因为 2 是偶数：

1 : foldr step [] [3,4]

所以再次 foldr：

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

现在评估 < code>step 产生 3：

1 : 3 : foldr step [] [4]

评估 foldr；

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

再次step：

1 : 3 : foldr step [] []

最后foldr计算结果为空列表：

1 : 3 : []

Answer 3

乍一看，您在特定示例中采取的步骤单独看来是正确的。但是，我想指出 filter 和 foldr 都可以有效地应用于无限列表 - 这应该表明顺序就 Haskell 而言，你的步骤是不正确的。