Why is the following typecheck performed?

Question

Why is the following typecheck performed?

cancel xy = x distribute fgx = fx (gx) 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 a -> b .

Can anyone explain this to me?

Answer 1

Let all type variables be different:

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

So, just by building the types that we need to combine to prove that checking the distribution of calls:

 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 type equality in Haskell, you can use it in real code if you enable some extensions)

Substitute 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: the type of the argument and the type of the result. Thus, if we have a function type with two arrows, one of them must be inside the argument type or the result type of the other. In a case like r -> s -> r , we use the right associativity -> to leave parentheses that would make it obvious: it really is 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:

 x ~ r y ~ s -> r 

More lookups:

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

So the thing that cancels 1 is ignored is a function of type s -> r , which also returns cancel2. Keeping in mind the implementation of fx (gx) distribute , this makes sense. cancel1 and cancel2 both must be called with the same thing; cancel1 then gets the result of calling cancel2 as the second argument, which it quickly ignores, so it doesn't matter what type of the cancel2 second parameter is, since it never called another argument (any function that takes r since its first parameter would work here) . This is a tricky way to write a function that does nothing: identity.

---

¹ If you are having trouble remembering whether -> right or left associative, you may have heard that all Haskell functions take one argument, and we usually "fake" functions with multiple arguments using functions that return other functions. What happens here and why the arrow function is associated on the right.

Answer 2

cancel is of type a -> b -> a , but the same as a -> (b -> a) , so it has a function type with input a and b -> a .

a -> b matches any type of function; in this case, a corresponds to a and b corresponds to b -> a .

distribute cancel (\abc -> a) checks in the same way. Haskell functions have curry, so there is always only one input type and one return type, but the return type can also be a function.