Explanation of currying for zipWith ($)

Question

I have been trying to understand this piece of code but I'm not able to wrap it up clearly:

ghci > :t zipWith
zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
ghci > :t ($)
($) :: (a -> b) -> a -> b
ghci > let c = zipWith ($)
ghci > :t c
c :: [b -> c] -> [b] -> [c]

How does [b -> c] originate up in the above type signature ?

Answer 1

In order for zipWith ($) to typecheck we must unify the type of zipWith's first argument with the type of ($). I'll write them out together and with unique names to make it more clear.

zipWith :: (a        -> b -> c) -> [a]     -> [b] -> [c]
($)     :: ((x -> y) -> x -> y)

Thus, zipWith typechecks if and only if we can assume that a ~ (x -> y), b ~ x and c ~ y. There's nothing stopping this unification from succeeding, so we can substitute these names back into the type for zipWith.

zipWith :: ((x -> y) -> x -> y) -> [x -> y] -> [x] -> [y]
($)     :: ((x -> y) -> x -> y)

And then proceed with application since everything matches up nicely now

zipWith ($) :: [x -> y] -> [x] -> [y]

which is equivalent up to the specific choice of type variable names with the type you saw.

Answer 2

It's just context substitution and no magic there. Look:

ghci > :t zipWith
zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
ghci > :t ($)
($) :: (a' -> b') -> a' -> b'

Now consider zipWith ($). It has type of (a -> b -> c) -> [a] -> [b] -> [c] where first argument is fixed, so we should pattern match (a -> b -> c) (type of a first arg) with (a' -> b') -> a' -> b' (type of $). Thus we have a = (a' -> b'), b = a', c = b'. Substitute is back to the zipWith: [a' -> b'] -> [a'] -> [b'] (first argument is fixed, so he disappear from type) and that's exactly what you got with type variables named differently.

Also, one might consider zipWith semantics: take zipper (first argument), and then zip two lists together. If your zipper is function application ($ is function application, yes!) then when zipping two lists you just invoke elements of the first list with corresponding element of the second list. And function type reflects that.

Answer 3

The actual letters assigned in the type signature are arbitrary and could be anything. You could just as easily write the type of ($) as

(x -> y) -> x -> y

It takes two arguments, a function taking a single argument, and a value to pass into the function.

The first argument to zipWith is a function taking two arguments (a -> b -> c). Given the definition of ($), you choose a as (x -> y) and b as x then c is y, so you get the type of zipWith ($) as

[x -> y] -> [x] -> [y]

Answer 4

Let's rewrite a bit our signature:

($) :: (a -> b) -> a -> b
($) :: a' -> b' -> c'
  where  -- pseudo-Haskell
    a' = a -> b
    b' = a
    c' = b


zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]

And find, that

zipWith ($) :: [a'] -> [b'] -> [c']

zipWith ($) :: [a -> b] -> [a] -> [b]