如何用等式推理合理推导zipWith (+) [1,2] [3,4]的求值步骤？

先给出zipWith的原始定义：

zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
zipWith f = go
  where
    go [] _ = []
    go _ [] = []
    go (x:xs) (y:ys) = f x y : go xs ys

你提到在对zipWith (+) [1,2] [3,4]求值时，原推导步骤3里(+)“凭空出现”不符合等式推理逻辑——问题出在go是定义在zipWith f作用域内的局部函数，它隐式捕获了参数f，不能直接把zipWith (+)替换成无参数绑定的go，正确推导需要明确go对f的引用关系。

正确推导过程 #

zipWith (+) [1,2] [3,4]    -- 1：初始表达式
= (let f = (+) in go) [1,2] [3,4]  -- 2：展开zipWith的定义，显式f的绑定
= let f = (+) in go [1,2] [3,4]    -- 3：应用函数结合律
= let f = (+) in (f 1 3 : go [2] [4])  -- 4：匹配go的第三个模式
= (+) 1 3 : (let f = (+) in go [2] [4])  -- 5：代入let绑定的f
= 4 : (let f = (+) in go [2] [4])  -- 6：计算(+) 1 3
= 4 : (let f = (+) in (f 2 4 : go [] []))  -- 7：再次匹配go的第三个模式
= 4 : ((+) 2 4 : (let f = (+) in go [] []))  -- 8：代入f
= 4 : (6 : [])  -- 9：计算(+) 2 4，匹配go的空列表模式得到[]
= [4,6]  -- 10：整理最终列表

更直观的等价定义辅助推理 #

如果把go改成显式接收f参数的形式（和原定义语义完全等价，只是把隐式捕获的变量显式化），推导会更清晰：

zipWith f = go f
  where
    go _ [] _ = []
    go _ _ [] = []
    go f (x:xs) (y:ys) = f x y : go f xs ys

对应的推导步骤：

zipWith (+) [1,2] [3,4]
= go (+) [1,2] [3,4]
= (+) 1 3 : go (+) [2] [4]
= 4 : ((+) 2 4 : go (+) [] [])
= 4 : (6 : [])
= [4,6]

核心逻辑是：原定义里的go是闭包，它依赖zipWith传入的f，等式推理时必须明确这个绑定关系，不能跳过f的传递直接使用go。

内容的提问来源于stack exchange，提问作者F. Zer