Почему монады не закрыты по составу? - программирование
Подтвердить что ты не робот

Почему монады не закрыты по составу?

Когда я изучал главу " Composing Types из книги "Haskell", мне дали задание написать экземпляры Functor и Applicative для следующего типа.

newtype Compose f g a = Compose { getCompose :: f (g a) }

Я написал следующие определения

Функтор:

fmap f (Compose fga) = Compose $ (fmap . fmap) f fga

Прикладное:

(Compose f) <*> (Compose a) = Compose $ (<*>) <$> f <*> a

Я узнал, что составление двух Функторов или Аппликативов дает Функтор и Аппликатив соответственно.

Автор также объяснил, что невозможно составить две монады одинаково. Поэтому мы используем монадные трансформаторы. Я просто не хочу читать Монадные Трансформеры, если не понимаю, почему Монады не сочиняют.

До сих пор я пытался написать функцию bind следующим образом:

Монада:

(>>=) :: Compose f g a -> (a -> Compose f g b) -> Compose f g b
(Compose fga) >>= h = (fmap.fmap) h fga

и, конечно, получил эту ошибку от GHC

Ожидаемый тип: составить FGB

Фактический тип: f (g (Compose fgb))

Если я смогу как-нибудь лишить fg, композиция даст нам монаду, верно? (Я все еще не мог понять, как раздеть это все же)

Я попытался прочитать ответы на другие вопросы о переполнении стека, как это, но все ответы более теоретические или математические. Я до сих пор не понял, почему монады не сочиняют. Может кто-нибудь объяснить мне без использования математики?

4b9b3361

ОТВЕТЫ

Ответ 1

Я думаю, что это проще всего понять, посмотрев на оператор join:

join :: Monad m => m (m a) -> m a

join является альтернативой >>= для определения Monad, и ее немного легче рассуждать. (Но теперь у вас есть упражнение: покажите, как реализовать >>= из join и как реализовать join из >>=!)

Давайте попробуем сделать операцию join для Composed f g и посмотрим, что пойдет не так. Наш ввод по сути является значением типа f (g (f (g a))), и мы хотим получить значение типа f (g a). Мы также знаем, что у нас есть join для f и g по отдельности, поэтому, если бы мы могли получить значение типа f (f (g (g a))), то мы могли бы нажать его с fmap join . join, чтобы получить f (g a), который мы хотели.

Теперь f (f (g (g a))) не так далеко от f (g (f (g a))). Все, что нам действительно нужно, это такая функция: distribute :: g (f a) -> f (g a). Тогда мы могли бы реализовать join так:

join = Compose . fmap join . join . fmap (distribute . fmap getCompose) . getCompose

Примечание: есть некоторые законы, которые мы хотели бы выполнить distribute, чтобы убедиться, что получаемый нами join законен.

Итак, это показывает, как мы можем составить две монады, если у нас есть закон распределения distribute :: (Monad f, Monad g) => g (f a) -> f (g a). Теперь, это может быть правдой, что каждая пара монад имеет закон распределения. Может быть, нам просто нужно серьезно задуматься о том, как записать один?

К сожалению, есть пары монад, у которых нет закона распределения. Таким образом, мы можем ответить на ваш первоначальный вопрос, создав две монады, которые определенно не могут превратить g (f a) в f (g a). Эти две монады будут свидетельствовать о том, что монады вообще не сочиняются.

Я утверждаю, что у g = IO и f = Maybe нет закона о распределении

-- Impossible!
distribute :: IO (Maybe a) -> Maybe (IO a)

Давайте подумаем, почему такая вещь невозможна. Входом для этой функции является действие ввода-вывода, которое выходит в реальный мир и в конечном итоге производит Nothing или Just x. Выход этой функции - либо Nothing, либо Just действие ввода-вывода, которое при запуске в конечном итоге приводит к x. Чтобы создать Maybe (IO a), нам нужно заглянуть в будущее и предсказать, что будет делать действие IO (Maybe a)!

В итоге:

  • Монады могут сочинять, только если существует закон распределения g (f a) -> f (g a).
  • Некоторые монады не имеют такого закона распределения.
  • Некоторые монады могут сочинять друг с другом, но не каждая пара монад может сочинять.