Why does adding an as-pattern to a working function cause compilation errors?

Question

Here's the standard Functor instance for Either a:

instance Functor (Either a) where
        fmap _ (Left x) = Left x
        fmap f (Right y) = Right (f y)

adding in an as-pattern causes compilation errors when loading into GHCi:

instance Functor (Either a) where
        fmap _ z@(Left x) = z          -- <-- here's the as-pattern
        fmap f (Right y) = Right (f y)

Couldn't match expected type `b' against inferred type `a1'
  `b' is a rigid type variable bound by
      the type signature for `fmap' at <no location info>
  `a1' is a rigid type variable bound by
       the type signature for `fmap' at <no location info>
  Expected type: Either a b
  Inferred type: Either a a1
In the expression: z
In the definition of `fmap': fmap _ (z@(Left x)) = z

Why doesn't this work?

`Either x a` and `Either x b` both have elements named `L x`, so `fmap f (L x) = L x` works. But `a@(L x)`, on the left means that `a` is identified with something of type `Either x a`. But what is needed on the right is something of type `Either x b` — applicative, Aug 21 '12 at 16:38

score 11 · Answer 1 · answered Aug 21 '12 at 13:57

11

fmap has signature (a -> b) -> f a -> f b, i.e. it has to allow for a and b to be different. In your implementation, a and b can only be the same, because it returns the same thing that was passed as an argument. So GHC complains.

answered Aug 21 '12 at 13:57

Cat Plus Plus

125,936
27
200
224

From a beginner's point of view, the standard instance also `returns the same thing that was passed as an argument`. The difference is somewhat subtle -- at least to me. – Matt Fenwick Aug 21 '12 at 14:08
9

@MattFenwick The subtle thing is that the `Left` on the left and the `Left` on the right aren't the same thing; the one on the right is more polymorphic! You might like to try writing `data Phantom a = Phantom` and comparing the types of `f a@Phantom = a` and `g Phantom = Phantom`. – Daniel Wagner Aug 21 '12 at 14:20

Matt Fenwick · Answer 2 · 2012-08-21T14:05:58.787

My best guess is that this fails because z represents different types on each side of the equation:

the overall type is fmap :: (a -> b) -> Either t a -> Either t b
on the left side, z :: Either t a
on the right side, z :: Either t b

It seems that Left x is allowed to have multiple different types in the same equation, but z is not.

This implementation also fails, apparently for the same reason:

instance Functor (Either a) where
        fmap f (Right y) = Right (f y)
        fmap _ z = z          

Couldn't match expected type `b' against inferred type `a1'
  `b' is a rigid type variable bound by
      the type signature for `fmap' at <no location info>
  `a1' is a rigid type variable bound by
       the type signature for `fmap' at <no location info>
  Expected type: Either a b
  Inferred type: Either a a1
In the expression: z
In the definition of `fmap': fmap _ z = z

Nothing surprising since the type of `z` is fixed to be `Either t a`. On the other hand `Left :: forall a b. a -> Either a b` and because of that `Left x :: forall b. Either t b`, which allows you to pick any `b` you want. — Vitus, Aug 21 '12 at 14:08
@Vitus good point, I'm so used to Haskell's implicit forall's and type inferencing that those differences are usually invisible to me ... — Matt Fenwick, Aug 21 '12 at 14:10

score 2 · Answer 3 · answered Aug 21 '12 at 19:24

If you specialize the signature of fmap to Either l, you get:

fmap :: (a -> b) -> Either l a -> Either l b

This means that the Left r that you are pattern-matching on the left-hand side of your case statement must have type Either l a. However, you can't return it as is, because you have to return an Either l b. This requires re-wrapping the left-hand value in a new Left so that the compiler can infer that it is returning a newly minted Either that might have a different type for the Right value.

score 2 · Answer 4 · answered Aug 22 '12 at 01:52

For the Either a instance, fmap has the following type:

(i -> j) -> Either a i -> Either a j

In this equation:

fmap _ (Left x) = Left x

the second argument is known to be of type Either a i and to have matched the pattern Left x. We take the x out, and apply Left to it to get the result of fmap.

The trick is that the Left on the left side of the equation is not the same thing as the Left on the right side! On the LHS Left is this constructor:

Left :: a -> Either a i

Whereas on the RHS the Left is this constructor:

Left :: a -> Either a j

The RHS Left used in the pattern wouldn't have matched the type of fmap's second argument Either a i, and the LHS Left doesn't construct values of the type needed as fmap's result Either a j.

So there's no way to use the same Left for both things, semantically speaking; you have to construct a new Left x :: Either a j containing the x found in the Left x :: Either a i. Operationally, the Haskell implementation may or may not represent those two terms identically, and may or may not be able to share a single in-memory representation of two values with different types, and may or may not be clever enough to optimise away the construction of a new value that would be represented identically to another value it already has on hand. But those implementation issues are distinct from what the program means, and the type-checker's role is purely concerned with meaning.

Why does adding an as-pattern to a working function cause compilation errors?

4 Answers4