Аппликативы составляют, а монады - нет

Если мы сравним типы

(<*>) :: Applicative a => a (s -> t) -> a s -> a t
(>>=) :: Monad m =>       m s -> (s -> m t) -> m t

мы понимаем, что разделяет эти два понятия. Это (s -> m t) в типе (>>=) показывает, что значение в s может определять поведение вычисления в m t. Монады допускают интерференцию между слоями значений и вычислений. Оператор (<*>) не допускает такого вмешательства: вычисления функций и аргументов не зависят от значений. Это действительно кусается. Сравнивать

miffy :: Monad m => m Bool -> m x -> m x -> m x
miffy mb mt mf = do
  b <- mb
  if b then mt else mf

который использует результат некоторого эффекта для выбора между двумя вычислениями (например, запуск ракет и подписание перемирия), тогда как

iffy :: Applicative a => a Bool -> a x -> a x -> a x
iffy ab at af = pure cond <*> ab <*> at <*> af where
  cond b t f = if b then t else f

который использует значение ab для выбора между значениями двух вычислений at и af, выполнив оба, возможно, с трагическим эффектом.

Монадическая версия по существу полагается на дополнительную мощность (>>=) для выбора вычисления из значения, и это может быть важно. Однако поддержка этой силы затрудняет сочинение монад. Если мы попытаемся построить двойную привязку

(>>>>==) :: (Monad m, Monad n) => m (n s) -> (s -> m (n t)) -> m (n t)
mns >>>>== f = mns >>-{-m-} \ ns -> let nmnt = ns >>= (return . f) in ???

мы зашли так далеко, но теперь наши слои перемешаны. У нас есть n (m (n t)), поэтому нам нужно избавиться от внешнего n. Как говорит Александр С, мы можем это сделать, если у нас есть подходящий

swap :: n (m t) -> m (n t)

переставить n внутрь и join его на другой n.

Более слабое двойное применение определить намного легче.

(<<**>>) :: (Applicative a, Applicative b) => a (b (s -> t)) -> a (b s) -> a (b t)
abf <<**>> abs = pure (<*>) <*> abf <*> abs

потому что нет интерференции между слоями.

Соответственно, хорошо понимать, когда вам действительно нужна дополнительная мощность Monads, а когда вы можете избежать жесткой структуры вычислений, которую поддерживает Applicative.

Заметьте, кстати, что, хотя составление монад сложно, это может быть больше, чем вам нужно. Тип m (n v) указывает на вычисление с m-эффектами, затем на вычисление с n-эффектами до v-значения, где m-эффекты заканчиваются до начала n-эффектов (отсюда необходимость в swap). Если вы просто хотите чередовать m-эффекты с n-эффектами, то композиция - это, возможно, слишком много для вас!

Аппликативы составляют, а монады - нет.

Монады действительно составляют, но результатом может быть не монада. Напротив, композиция из двух аппликативов обязательно является аппликативом. Я подозреваю, что намерение первоначального утверждения заключалось в том, что «аппликативность составляет, а монадость - нет». Перефразируя, «Applicative закрыт по составу, а Monad нет».

Если у вас есть аппликативы A1 и A2, тогда тип data A3 a = A3 (A1 (A2 a)) также является аппликативным (вы можете написать такой экземпляр в общем виде).

С другой стороны, если у вас есть монады M1 и M2, тогда тип data M3 a = M3 (M1 (M2 a)) не обязательно является монадой (нет разумной общей реализации для >>= или join для композиции).

Одним из примеров может быть тип [Int -> a] (здесь мы составляем конструктор типа [] с (->) Int, оба из которых являются монадами). Вы легко можете написать

app :: [Int -> (a -> b)] -> [Int -> a] -> [Int -> b]
app f x = (<*>) <$> f <*> x

И это относится к любому аппликативу:

app :: (Applicative f, Applicative f1) => f (f1 (a -> b)) -> f (f1 a) -> f (f1 b)

Но толкового определения

join :: [Int -> [Int -> a]] -> [Int -> a]

Если вы не уверены в этом, рассмотрите это выражение:

join [\x -> replicate x (const ())]

Длина возвращаемого списка должна быть установлена ​​в камне, прежде чем целое число когда-либо будет предоставлено, но правильная длина его зависит от предоставленного целого числа. Таким образом, для этого типа не может существовать правильная join функция.

К сожалению, наша настоящая цель - составление монад - намного сложнее. .. Фактически, мы действительно можем доказать, что в определенном смысле нет способа построить функцию соединения с указанным выше типом, используя только операции двух монад (схему доказательства см. В приложении). Отсюда следует, что единственный способ, которым мы можем надеяться сформировать композицию, - это наличие дополнительных конструкций, связывающих два компонента.

Составление монад, http://web.cecs.pdx.edu/~mpj/pubs/RR-1004.pdf

Достаточно решения l: MN -> NM по распределительному закону

гарантировать монадичность НМ. Для этого вам понадобится агрегат и мульт. Я сосредоточусь на мульт (единица измерения - unit_N unitM)

NMNM - l -> NNMM - mult_N mult_M -> NM

Это не гарантирует, что MN является монадой.

Однако важное наблюдение вступает в игру, когда у вас есть решения по закону распределения.

l1 : ML -> LM
l2 : NL -> LN
l3 : NM -> MN

таким образом, LM, LN и MN - монады. Возникает вопрос, является ли LMN монадой (либо по

(MN)L -> L(MN) or by N(LM) -> (LM)N

У нас достаточно структуры, чтобы делать эти карты. Однако, как отмечает Евгения Ченг, нам нужно гексагональное условие (которое эквивалентно представлению Янга-Бакстера уравнение), чтобы гарантировать монадичность любой конструкции. Фактически, при условии гексагональности две разные монады совпадают.

Из любых двух аппликативных функторов можно составить еще один аппликативный функтор. Но с монадами это не работает. Сочетание двух монад - это не всегда монада. Например, композиция из монад State и List (в любом порядке) не является монадой.

Более того, невозможно соединить две монады вообще ни композиционно, ни каким-либо другим способом. Не существует известного алгоритма или процедуры, объединяющей любые две монады M, N в более крупную законную монаду T, чтобы вы могли вводить M ~> T и N ~> T морфизмами монад и удовлетворять разумным законам невырожденности (например, чтобы гарантировать, что T не просто тип юнита, который отбрасывает все эффекты от M и N).

Можно определить подходящий T для конкретных M и N, например M = Maybe, N = State s и так далее. Но неизвестно, как определить T, который работал бы параметрически в монадах M и N. Ни композиция функторов, ни более сложные конструкции не работают должным образом.

Один из способов комбинирования монад M и N - сначала определить совместный продукт C a = Either (M a) (N a). Этот C будет функтором, но, в общем, не монадой. Затем строят свободную монаду (Free C) на функторе C. В результате получилась монада, способная представлять комбинированные эффекты M и N. Однако это гораздо более крупная монада, которая также может представлять другие эффекты; это намного больше, чем просто комбинация эффектов M и N. Кроме того, свободную монаду нужно будет запустить или интерпретировать, чтобы извлечь какие-либо результаты (а законы монад гарантируются только после запуска). Будет штраф во время выполнения, а также штраф за размер памяти, потому что свободная монада потенциально будет создавать очень большие структуры в памяти перед запуском. Если эти недостатки несущественны, то можно использовать бесплатную монаду.

Другой способ объединения монад - взять преобразователь одной монады и применить его к другой монаде. Но не существует алгоритмического способа взять определение монады (например, тип и код в Haskell) и создать тип и код соответствующего преобразователя.

Существует по крайней мере 4 различных класса монад, преобразователи которых построены совершенно разными, но регулярными способами (составленные внутри, составленные снаружи, монада на основе присоединения, монада произведения). Несколько других монад не принадлежат ни к одному из этих обычных классов и имеют преобразователи, определенные каким-то образом специально.

Законы распределения существуют только для составных монад. Ошибочно думать, что любые две монады M, N, для которых можно определить некоторую функцию M (N a) -> N (M a), будут составлены. Помимо определения функции с этим типом сигнатуры, нужно доказать, что выполняются определенные законы. Во многих случаях эти законы не выполняются.

Есть даже некоторые монады, у которых есть два неэквивалентных преобразователя; один определяется обычным образом, а другой - специально. Простым примером является монада идентичности Id a = a; у него есть обычный трансформатор IdT m = m (составной) и нерегулярный специальный: IdT2 m a = forall r. (a -> m r) -> m r (монада кодовой плотности на m).

Более сложный пример - монада селектора: Sel q a = (a -> q) -> a. Здесь q - фиксированный тип, а a - главный параметр типа монады Sel q. Эта монада имеет два преобразователя: SelT1 m a = (m a -> q) -> m a (внутренний) и SelT2 m a = (a -> m q) -> m a (специальный).

Полная информация представлена ​​в главе 14 книги «Наука функционального программирования». https://github.com/winitzki/sofp или https://leanpub.com/sofp/.

Вот код, создающий композицию монад с помощью закона распределения. Обратите внимание, что существуют законы распределения от любой монады к монадам Maybe, Either, Writer и []. С другой стороны, вы не найдете таких (общих) законов распределения на Reader и State. Для этого вам понадобятся монадные трансформаторы.

 {-# LANGUAGE FlexibleInstances #-}
 
 module ComposeMonads where
 import Control.Monad
 import Control.Monad.Writer.Lazy
 
 newtype Compose m1 m2 a = Compose { run :: m1 (m2 a) }
 
 instance (Functor f1, Functor f2) => Functor (Compose f1 f2) where
   fmap f = Compose . fmap (fmap f) . run
 
 class (Monad m1, Monad m2) => DistributiveLaw m1 m2 where
   dist :: m2 (m1 a) -> m1 (m2 a)
 
 instance (Monad m1,Monad m2, DistributiveLaw m1 m2)
           => Applicative (Compose m1 m2) where
     pure = return
     (<*>) = ap
 
 instance (Monad m1, Monad m2, DistributiveLaw m1 m2)
           => Monad (Compose m1 m2) where
   return = Compose . return . return
   Compose m1m2a >>= g =
     Compose $ do m2a <- m1m2a -- in monad m1
                  m2m2b <- dist $ do a <- m2a  -- in monad m2
                                     let Compose m1m2b = g a
                                     return m1m2b
                                  -- do ... ::  m2 (m1 (m2 b))
                           -- dist ... :: m1 (m2 (m2 b))          
                  return $ join m2m2b -- in monad m2
 
 instance Monad m => DistributiveLaw m Maybe where
   dist Nothing = return Nothing
   dist (Just m) = fmap Just m
 
 instance Monad m => DistributiveLaw m (Either s) where
   dist (Left s) = return $ Left s
   dist (Right m) = fmap Right m
 
 instance Monad m => DistributiveLaw m [] where
   dist = sequence
 
 instance (Monad m, Monoid w) => DistributiveLaw m (Writer w) where
   dist m = let (m1,w) = runWriter m
            in do a <- m1
                  return $ writer (a,w)
 
 liftOuter :: (Monad m1, Monad m2, DistributiveLaw m1 m2) =>
                    m1 a -> Compose m1 m2 a
 liftOuter = Compose . fmap return
 
 liftInner :: (Monad m1, Monad m2, DistributiveLaw m1 m2) =>
                    m2 a -> Compose m1 m2 a
 liftInner = Compose . return