Почему монады не закрыты по составу? - PullRequest
11 голосов
/ 07 марта 2019

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

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

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

Functor:

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

Ожидаемый тип: Compose f g b

Фактический тип: f (g (Создать f g b))

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

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

Ответы [ 2 ]

18 голосов
/ 07 марта 2019

Я думаю, что это проще всего понять, посмотрев на оператор 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 :: 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).
  • Некоторые монады не имеют такого закона распределения.
  • Некоторые монады могут составлять сдруг друга, но не каждая пара монад может составлять.
1 голос
/ 14 апреля 2019

Монады не составляют - см. Здесь: https://www.slideshare.net/pjschwarz/monads-do-not-compose

first slide

enter image description here

...