Для различных возможных экземпляров Monad типа всегда подразумевается экземпляр Functor?

Question

Согласно Typeclassopedia и этой ссылке тип может иметь только один Functor экземпляр (есть ссылка в ссылке). Но я понимаю, что для данного типа возможно иметь несколько возможных Monad случаи, это правильно? Но для данного Monad экземпляр есть бесплатный Functor экземпляр с

fmap f xs  =  xs >>= return . f

Из этого я заключаю, что если я наткнусь на тип, в котором я могу определить несколько Monad экземпляры по-разному, то fmap Функция, полученная, как указано выше, должна равняться для всех них, другими словами, если у меня есть две пары функций:

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

для однотипного конструктора m, чем, обязательно:

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

для всех xs :: a а также f :: a -> b,

Это правда? Это имеет место как теорема?

Answer 1

Да. На самом деле мы можем сделать более сильное утверждение, что все функции с типом

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

такой, что fmap id = id эквивалентны. Это на самом деле просто выпадает из типа fmap с тем, что называется параметричностью.

В вашем случае, если >>= а также return удовлетворить законы монады, то

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

По закону монады, что a >>= return просто a, Используя этот результат, мы можем обратиться к свободной теореме, которую мы получаем из параметричности, и у нас есть доказательство.