Understanding the variables in Either

This is from a “write you own Either with Functor instance” exercise. Writing it is pretty painless:

data Either1 a b = Left1 a | Right1 b

instance Functor (Either1 x) where
  fmap _ (Left1 x) = Left1 x
  fmap f (Right1 x) = Right1 (f x)

Out of curiosity I switched a and b in the data constructors and got an error. I know it is wrong but am looking for a deeper unerstanding.

data Either2 a b = Left2 b | Right2 a

instance Functor (Either2 x1) where
  fmap _ (Left2 x2) = Left2 x2
  fmap f (Right2 z) = Right2 (f z)

Error

• Couldn't match type ‘b’ with ‘x1’  
Expected: Either2 x1 b  
Actual: Either2 b b  
‘b’ is a rigid type variable bound by  
the type signature for:  
fmap :: forall a b. (a -> b) -> Either2 x1 a -> Either2 x1 b

Seems I’m missing something

  • I know that Functor on type constructors with multiple arguments only apply the f in fmap f ... to the last argument (or at least I thought so – see the Pair example below).

I think the answer is that x1 in Either2 x1 is a in Either2 a b and a in Right2 a. And since it is already made part of the structure in Functor Either x1 it can’t be modified. But

  1. I’m not sure I’m right
  2. and, re “already made part of the structure” I suspect there is a better/standard way of saying that
  3. I don’t get what the error message is trying to say

This example broke what I though was a rule (“only modify the last argument to the type constructor”). I found many examples of this written exactly as below, so I’m led to think it is correct?

data Pair a = Pair a a

instance Functor Pair where
  fmap :: (a -> b) -> Pair a -> Pair b
  fmap f (Pair a b) = Pair (f a) (f b)
1 Like

So there isn’t really a rule at play here, but there is a consequence of the rules you already know about the type system that makes what you want to do not work. To see why, I’ve annotated the type of fmap:

data Either2 a b = Left2 b | Right2 a

instance Functor (Either2 x1) where
  fmap :: (a -> b) -> Either2 x1 a -> Either2 x1 b
  -- fmap _ (Left2 x2) = Left2 x2
  -- fmap f (Right2 z) = Right2 (f z)

The first thing to do is to convince yourself that fmap must have this type if (Either2 x1) is to be a Functor.

The second thing is to see that this means that the Left side must change, not the Right.

I can expand on either of these points, but let me know which is unclear (or both) :slight_smile:

2 Likes

The first thing …

  • fmap requires kind * -> *
  • Either2 has kind * -> * -> *
  • So you partially apply it Either2 x1
    I’m pretty comfortable with that now

The second thing …

I guess since Either2 is already partially applied with a via the x1, a can’t be changed. If correct, I’m still left with “why not”.

If I think of it in terms of a function then it seems obvious.

  • a -> a -> a (two arguments)
    becomes
  • Integer -> Integer (one argument)
addit :: Num a => a -> a -> a
addit a b = a + b

add1 :: Integer -> Integer
add1 = addit 1

So if I think of that being similar to types then: A type that takes 2 arguments and one is already applied can only take one more. The first is no longer available to change.

But that doesn’t seem to completely hold because x1 isn’t concrete yet so it can be changed. However, I think it will be concrete by the time you can call fmap on Either2 so maybe that is the answer?

Yep, that’s pretty much it exactly re both points. (Either2 x1) can’t vary x1 in the Functor instance because it’s already been applied.

You’re right that x1 is universally quantified, and I see why that’s confusing, but that’s a separate issue. Think of it as fixed by a universal quantifier:

instance forall x1. Functor (Either2 x1) where
  fmap :: (a -> b) -> Either2 x1 a -> Either2 x1 b
  fmap _ (Left2 x2) = Left2 undefined
  fmap f (Right2 z) = Right2  undefined -- (f z)

Or reason about Either2 Bool or any other concrete type for x2.

Someone else can probably explain this more elegantly than me…

1 Like

I think if we rewrite this by not using a and b, you’ll see more easily what’s happening:

data Either1 left right = Left1 left | Right1 right

instance Functor (Either1 left) where
  -- fmap :: (right -> right2) -> Either left right -> Either left right2
  fmap _ (Left1 x) = Left1 x
  fmap f (Right1 x) = Right1 (f x)

If you then give Left the right type variable:

data Either2 left right = Left2 right | Right2 left

instance Functor (Either2 left) where
  -- fmap :: (right -> right2) -> Either left right -> Either left right2
  fmap _ (Left2 x2) = Left2 x2
  fmap f (Right2 z) = Right2 (f z)
  -- what does (f z) do here?
  -- (f :: right -> right2) (z :: left)

The f in your fmap definition will always be f :: right -> right2.
This is per definition, because it’s always the most right/outer type variable of the type definition: e.g. ExceptT e m a will be Functor (ExceptT e m), because the a is the right-most type variable, with fmap :: (a -> b) -> ExceptT e m a -> ExceptT e m b)

But you’re going to only be able to use that f on the value in your Left case, because that’s the one with the right type variable. The Right constructor got the left type variable, so you can’t really do anything with it, except just return it.

1 Like

I’m more comfortable with this now. Thank you both!

1 Like