Why does the following typecheck?

Question

Why does the following typecheck?

cancel x y = x
distribute f g x = f x (g x)
identity = distribute cancel cancel

Clearly cancel :: a -> b -> a, distribute :: (a -> b -> c) -> (a -> b) -> a -> c and identity :: a -> a. Now, distribute cancel :: (a -> b) -> a -> a, but I don't understand why cancel matches with a -> b.

Could anyone explain this to me?

Answer 1

Let's make all the type variables distinct:

identity = distribute cancel1 cancel2
  where distribute :: (a -> b -> c) -> (a -> b) -> a -> c
        cancel1 :: x -> y -> x
        cancel2 :: r -> s -> r

So, simply lining up the types we need to unify to prove that distribute call checks out:

distribute :: (a -> b -> c) -> (a -> b)     -> a -> c
cancel1    ::  x -> y -> x
cancel2    ::                   r -> s -> r

cancel1 is obvious; we have:

a ~ x
b ~ y
c ~ x

(The ~ sign is basically how we write equality of types in Haskell; you can use it in actual code if you turn on some extensions)

Let's substitute those in

distribute :: (x -> y -> x) -> (x -> y)     -> x -> x
cancel1    ::  x -> y -> x
cancel2    ::                   r -> s -> r

For the next bit, we need to remember that the arrow is a binary operator. It takes exactly two parameters: an argument type and a result type.So if we've got a function type with two arrows one of them must be inside the argument type or result type of the other. In a case like r -> s -> r, we're using the right associativity of -> to leave out parentheses that would make it obvious: it's really r -> (s -> r).¹

So then:

distribute :: (x -> y -> x) -> (x ->  y      ) -> x -> x
cancel1    ::  x -> y -> x
cancel2    ::                   r -> (s -> r)

So now we can immediately read off:

x ~ r
y ~ s -> r

More substitution:

distribute :: (r -> (s -> r) -> r) -> (r -> (s -> r)) -> r -> r
cancel1    ::  r -> (s -> r) -> r
cancel2    ::                          r -> (s -> r)

So the thing that cancel1 is ignoring is a function of type s -> r, which is also what cancel2 returns. Remembering the f x (g x) implementation of distribute, this makes sense. cancel1 and cancel2 both have to be called with the same thing; cancel1 then receives the result of calling cancel2 as its second argument, which it promptly ignores, so it doesn't matter what the type of cancel2's second parameter is as it's never actually called on another argument (any function at all that accepts r as its first parameter would have worked here). This is all an elaborate way to write a function that does nothing: identity.

---

¹ If you have trouble remembering whether -> is right or left associative, you may have heard that all Haskell functions take a single argument and we commonly "fake" multiple-argument functions by using functions that return other functions. That's what's going on here, and why the function arrow associates to the right.

Answer 2

cancel has type a -> b -> a, but that's the same as a -> (b -> a), so it's a function type with a input and b -> a output.

a -> b matches any function type whatsoever; in this case, a matches a and b matches b -> a.

distribute cancel (\a b c -> a) checks out similarly. Haskell functions are curried, so there's always just a single input type and a single return type, but the return type can also be a function.