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

Question

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 ?

Answer 1

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 +.