For different possible Monad instances of a type, is the implied Functor instance always the same?

Question

According to the Typeclassopedia and this link a type can only have a single Functor instance (there's a proof in the link). But it is my understanding that it is possible for a given type to have multiple possible Monad instances, is this right? But for a given Monad instance there is a free Functor instance with

fmap f xs  =  xs >>= return . f

From this, I conclude that if I stumble upon a type in which I can define multiple Monad instances in different ways, then the fmap function derived as above must equal for all of them, in other words, if I have two pairs of functions:

bind_1 :: m a -> (a -> m b) -> m b
unit_1 :: a -> m a

bind_2 :: m a -> (a -> m b) -> m b
unit_2 :: a -> m a

for the same type constructor m, than, necessarily:

xs `bind_1` (unit_1 . f) == xs `bind_2` (unit_2 . f)

for all xs :: a and f :: a -> b.

Is this true? Does this hold as a theorem?

Answer 1

Yes. In fact we can make the stronger statement that all function with the type

fmap :: (a -> b) -> (F a -> F b)

such that fmap id = id are equivalent. This actually just falls out of the type of fmap with something called parametricity.

In your case, if >>= and return satisfy the monad laws, then

 mFmap f a  = a >>= return . f
 mFmap id a = a >>= return . id
 mFmap id a = a >>= return
 mFmap id a = a
 mFmap id = id

By the monad law that a >>= return is just a. Using this result, we can appeal to the free theorem we get from parametricity and we have our proof.