Reputation: 14022
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?
Upvotes: 14
Views: 305
Reputation: 53881
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.
Upvotes: 17