Для разных возможных экземпляров Monad типа подразумевается, что экземпляр Functor всегда одинаковый?
В соответствии с 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.
Это правда? Означает ли это, что это теорема?
Ответы
Ответ 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. Используя этот результат, мы можем обратиться к свободной теореме, полученной из параметричности, и имеем наше доказательство.
