Аппликативные сочинения, монады нет
Аппликативные сочинения, монады нет.
Что означает приведенное выше утверждение? А когда один предпочтительнее другого?
7 ответов
Если мы сравним типы
(<*>) :: 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
потому что нет никаких помех между слоями.
Соответственно, хорошо осознавать, когда вам действительно нужна дополнительная сила Monadс, и когда вы можете сойти с жесткой вычислительной структурой, которая 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 для композиции).
Одним из примеров может быть тип [String -> a] (здесь мы составляем конструктор типа [] с (->) Stringоба монады). Вы можете легко написать
app :: [String -> (a -> b)] -> [String -> a] -> [String -> b]
app f x = (<*>) <$> f <*> x
И это обобщает на любой аппликативный:
app :: (Applicative f, Applicative f1) => f (f1 (a -> b)) -> f (f1 a) -> f (f1 b)
Но нет разумного определения
join :: [String -> [String -> a]] -> [String -> a]
К сожалению, наша настоящая цель, составление монад, гораздо сложнее. Фактически, мы можем фактически доказать, что в определенном смысле нет способа построить функцию соединения с вышеприведенным типом, используя только операции двух монад (см. Приложение для краткого изложения доказательства). Отсюда следует, что единственный способ, которым мы могли бы надеяться сформировать композицию, - это наличие некоторых дополнительных конструкций, связывающих эти два компонента.
Составление монад, 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) или N(LM) -> (LM)N
У нас достаточно структур, чтобы сделать эти карты. Однако, как отмечает Евгения Ченг, нам необходимо шестиугольное условие (равносильное представлению уравнения Янга-Бакстера), чтобы гарантировать монадность любой конструкции. Фактически, с гексагональным условием две разные монады совпадают.
Из любых двух аппликативных функторов можно составить еще один аппликативный функтор. Но с монадами это не работает. Сочетание двух монад - это не всегда монада. Например, композиция из
State а также
List монады (в любом порядке) - это не монада.
Более того, невозможно соединить две монады вообще ни по композиции, ни по какому-либо другому методу. Не существует известного алгоритма или процедуры, объединяющей любые две монады в более крупную законную монаду, чтобы вы могли ввести
M ~> T а также
N ~> T морфизмами монад и удовлетворяют разумным законам невырожденности (например, чтобы гарантировать, что это не просто тип единицы, который отбрасывает все эффекты от и).
Можно определить подходящие для конкретных и, например,
M = Maybe а также
N = State sи так далее. Но неизвестно, как определить
Tэто будет работать параметрически в монадах и. Ни композиция функторов, ни более сложные конструкции не работают должным образом.
Один из способов объединения монад и, во-первых, определение сопутствующего продукта.
C a = Either (M a) (N a). Это будет функтор, но не монада. Затем строят свободную монаду (
Free C) на функторе
C. Результатом является монада, которая может представлять эффекты и сочетать их. Однако это гораздо более крупная монада, которая также может представлять другие эффекты; это намного больше, чем просто комбинация эффектов и. Кроме того, свободную монаду нужно будет «запустить» или «интерпретировать», чтобы извлечь какие-либо результаты (а законы монад гарантируются только после «выполнения»). Будет штраф во время выполнения, а также размер памяти, потому что свободная монада потенциально будет создавать очень большие структуры в памяти, прежде чем она будет "запущена". Если эти недостатки несущественны, то можно использовать бесплатную монаду.
Другой способ объединения монад - взять преобразователь одной монады и применить его к другой монаде. Но не существует алгоритмического способа взять определение монады (например, тип и код в Haskell) и создать тип и код соответствующего преобразователя.
Существует по крайней мере 4 различных класса монад, преобразователи которых построены совершенно разными, но регулярными способами (составленная внутри, составленная снаружи, монада на основе присоединения, монада продукта). Несколько других монад не принадлежат ни к одному из этих «обычных» классов, и в них преобразователи каким-то образом определены «ad hoc».
Законы распределения существуют только для составных монад. Ошибочно думать, что любые две монады
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