Why the difference in type-inference over the as-pattern in two similar function definitions?

26
votes

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!

2
haskelltype-signature
It looks like the first one might be a bit more flexible since t could conceivably equal a. – ChaosPandion
@ChaosPandion yes it is, but that's the mystery (to me as well when I've looked at it!) - it's saying the function input f must have the same input and output type, but there is nothing obvious in the function definition which would so constrain f. In fact the only line which differs in the two definitions doesn't reference f at all! – Robin Zigmond
same thing happens with the definition of fmap for Const btw. the value is repackaged in a different Right/Const constructor (which is polymorphic in the other type). – Will Ness
What is this "as-pattern" that you speak of? – Peter Mortensen
@PeterMortensen An "as-pattern" is a pattern that uses the @ symbol to assign a value to an identifier while also pattern matching on that value. Here that's r@(Right _) – 4castle

2 Answers

25
votes

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.

19
votes

The issue here is that there are some "hidden" types which make the difference. The type inference engine can infer those in the first case, but can't in the second case.

When we use 

Right :: forall a b. b -> Either a b

we actually need to choose what types a and b are. Fortunately, type inference makes this choice for us in most cases. Type b is easy to choose: it is the type of the value inside the argument of Right. Type a instead can be anything -- the inference engine has to rely on the context to "force" some choice for a. For instance, note that all of these type check:

test0 :: Either Int Bool
test0 = Right True

test1 :: Either String Bool
test1 = Right True

test2 :: Either [(Char, Int)] Bool
test2 = Right True

Now, in your first function

left :: (t -> a) -> Either t b -> Either a b
left f (Left x) = Left (f x)
left _ (Right x) = Right x

The first matched Right x is actually Right x :: Either t b, where the implicit type arguments are chosen to be t and b. This makes x to have type b. With this information, the type inference tries to determine the type for the second Right x. There, it can see that it should be of the form Either ?? b since x :: b, but, as it happened for our test examples above, we could use anything for ??. So the type inference engine chooses another type variable a (a type which might be t, but could also be something else).

Instead, in the second function

left' :: (t -> t) -> Either t b -> Either t b
left' f (Left x) = Left (f x)
left' _ r@(Right _) = r

we give a name (r) to the Right _ pattern. As above, that is inferred to have type Either t b. However, now we use the name r on the right of the =, so type inference does not have to infer anything there, and can (in fact, must) simply reuse the type it has already inferred for r. This makes the output type to be the same Either t b as the one for the input, and in turn this forces f to be of type t -> t.

If this is confusing, you could try to completely avoid type inference and provide an explicit choice for the types using the syntax Right @T @U to choose the function U -> Either T U. (You'll need to turn on the ScopedTypeVariables, TypeApplications extensions for this, though.) Then we can write:

left :: forall t a b. (t -> a) -> Either t b -> Either a b
left f (Left x) = Left @a @b (f x)
left _ (Right x) = Right @a @b x
                      -- ^^ -- we don't have to pick @t here!

We can also have

left :: forall t b. (t -> t) -> Either t b -> Either t b
left f (Left x) = Left @t @b (f x)
left _ (Right x) = Right @t @b x

and it would work just fine. GHC prefers the first type since it is more general, allowing a to be anything (including t, but also including other types).

There's no type application to specify in the second definition, since it reuses the same value r on the right hand side as on the left:

left' :: forall t b. (t -> t) -> Either t b -> Either t b
left' f (Left x) = Left @t @b (f x)
left' _ r@(Right x) = r
                   -- ^^ -- can't pick @a here! it's the same as on the LHS