我是否使用關於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函數。
這裏是myFilter函數內部的step定義，從上面：

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

另外，我提醒你，p實際上是在我們的例子中odd功能。

好，我們再次在這裏：

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

和

在最內側stepx = 4，並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]。

結束:-)。

我對我的所有動作都適用嗎？
非常感謝:-)。

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是嚴格的。但是，如果你按照我上面概述的方式來思考它，這對我來說是有意義的（無論如何）。

Answer 2

乍一看，您在具體示例中採取的步驟看起來單獨正確。不過，我想指出filter和foldr可以有用地應用於無限列表 - 這應該表明，就Haskell而言，您的步驟順序是不正確的。

Answer 3

只是爲了展開懶惰的評估順序：基本上，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]) 

現在評估step產生3：

1 : 3 : foldr step [] [4] 

評價foldr;

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

而且step一次：

1 : 3 : foldr step [] [] 

最後foldr計算結果爲空列表：

1 : 3 : []