I have the following two similar function definitions:
left f (Left x) = Left (f x)
left _ (Right x) = Right x
left' f (Left x) = Left (f x)
left' _ r@(Right _) = r
When I check the type signatures of the two functions, I am confused by the following types:
ghci> :t left
left :: (t -> a) -> Either t b -> Either a b
ghci> :t left'
left' :: (a -> a) -> Either a b -> Either a b
I suppose left and left' should be of the same type signature, but the haskell's type inference gives me a suprise.
I can't figure out why the type signatures of left and left' are different. Can anybody give me some information? Thanks!
In the second line of left':
left' _ r@(Right _) = r
-- ^^^^^^^^^^^ ^
Since you use an as-pattern, you require the input type to be equal to the return type, since clearly they're the exact same value. left''s type is then restricted to something of the form a -> b -> b.
This restriction then propogates backwards to in turn restrict the function's type – hopefully you can see how; it's not too difficult.
However, in the second line of left, you construct a new value
left _ (Right x) = Right x
-- ^^^^^^^
The type of this new value has not been restricted, and thus the same problem doesn't occur; it can be something of the form a -> b -> c, which is what you want.
For this reason, the type of left' is more restricted than the type of left, which is what causes their types to be unequal.
To illustrate this concept more concretely, I will describe to you more precisely how this restriction propogates backwards.
We know that left''s signature is of the form (a -> b) -> Either a q -> Either b q. However, line 2 dictates that Either a q = Either b q, which means that a = b, so the type now becomes (a -> a) -> Either a q -> Either a q.