Evaluating `zipWith ( ) [1,2] [3,4]` using equational reasoning-CodePudding

zipWith definition

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

has a local definition bound to the name go.

If I proceed the evaluation of zipWith ( ) [1,2] [3,4]

  zipWith ( ) [1,2] [3,4]    -- 1
= go [1,2] [3,4]             -- 2
= ( ) 1 3 : go [2] [4]       -- 3
= ...

line 3 is not correctly justified. ( ) is available inside go scope, but ( ) function can't appear "out of nowhere" in line 3 using equational reasoning. How can I proceed ?

CodePudding user response：

Thank you so much everyone. I am able to see it. And that's why go isn't available outside zipWith definition. The f in go's third equation would have an actual parameter when zipWith ( ) [1,2] [3,4] is called. Thus,

go (1:[2]) (3:[4]) = ( ) 1 3 : go [2] [4]

would hold.

CodePudding user response：

One way you could reason would be like this:

zipWith ( ) [1,2] [3,4]
= { definition of zipWith }
let go [] _ = []
    go _ [] = []
    go (x:xs) (y:ys) = ( ) x y : go xs ys
in go [1,2] [3,4]
= { definition of go, third case }
let go [] _ = []
    go _ [] = []
    go (x:xs) (y:ys) = ( ) x y : go xs ys
in ( ) 1 3 : go [2] [4]

This way doesn't appear "out of nowhere" -- it appears directly as the creation of a closure after the beta reduction of zipWith applied to .