Происходят ли вообще монадные трансформаторы из присоединений? - PullRequest
16 голосов
/ 23 июня 2019

In Сопоставимые функторы определяют монадные трансформаторы, но где их подъем? , Саймон C показал нам конструкцию ...

newtype Three u f m a = Three { getThree :: u (m (f a)) }

... которая, как там обсуждаются ответы, может быть дано instance Adjunction f u => MonadTrans (Three u f) ( присоединения обеспечивает его как AdjointT).Таким образом, любое присоединение Hask / Hask приводит к монадному преобразователю;в частности, StateT s возникает таким образом из каррирующего соединения между (,) s и (->) s.

Мой следующий вопрос: обобщает ли эта конструкция другие монадные трансформаторы?Есть ли способ получить, скажем, другие трансформаторы из пакета transformers из подходящих присоединений?


Мета замечания: мой ответ здесь изначально был написан для вопроса Саймона С.Я решил включить его в вопрос с самостоятельным ответом, потому что, перечитывая этот вопрос, я заметил, что мой предполагаемый ответ больше связан с обсуждением в комментариях, чем с самим телом вопроса.Два других тесно связанных вопроса, к которым эти вопросы и ответы, вероятно, также являются продолжением: Есть ли монада, у которой нет соответствующего монадного преобразователя (кроме IO)? и Является ли композиция произвольной монады с проходимым всегда монадой?

1 Ответ

14 голосов
/ 23 июня 2019

Три конструкции в этом ответе также доступны в воспроизводимой форме в этом Гисте .

Конструкция Саймона С. ...

newtype Three u f m a = Three { getThree :: u (m (f a)) }

... полагается на f и u, являющиеся присоединенными эндофункторами Хаска. Хотя это работает в случае StateT, есть две связанные проблемы, с которыми мы должны иметь дело, если мы хотим сделать его более общим:

  • Во-первых, нам нужно найти подходящие дополнения для «характерных монад», на которых будут построены трансформаторы; и

  • Во-вторых, если такое присоединение уводит нас от Хаск, нам придется каким-то образом обойти тот факт, что невозможно напрямую использовать монаду Хаск m.

Есть довольно много интересных дополнений, с которыми мы могли бы поэкспериментировать. В частности, есть два дополнения, которые доступны для каждой монады: присоединение Клейсли и присоединение Эйленберга-Мура (для их точного категориального представления см. Эмили Рил, Теория категорий в контексте , раздел 5.2). В категоричном отрывке, который занимает примерно половину этого ответа, я остановлюсь на присоединении Клейсли, просто потому, что в псевдо-Хаскеле удобнее шататься.

(Под псевдо-Хаскеллом я подразумеваю, что в последующем будет широко распространено злоупотребление нотацией. Чтобы упростить глаза, я буду использовать некоторые специальные соглашения: |-> означает отображение между вещами, которые не являются обязательно типы, аналогично : означает что-то, что напоминает сигнатуру типа; ~> означает морфизм не-Хаск; фигурные и угловые скобки выделяют объекты в выбранных категориях не-Хаск; . также означает композицию функторов; и F -| U означает F и U - сопряженные функторы.)

Kleisli присоединение

Если g - это Hask Monad, то между FK g имеется соответствующее присоединение Клейсли FK g -| UK g, которое приводит нас к категории g Kleisli ...

-- Object and morphism mappings.
FK g : a          |-> {a}
       f : a -> b |-> return . f : {a} ~> {b} ~ a -> g b
-- Identity and composition in Kleisli t are return and (<=<)

... и UK g, что возвращает нас к Хаску:

UK g : {a}            |-> g a
       f : {a} -> {b} |-> join . fmap f : g a -> g b  -- that is, (>>= f)

-- The adjunction isomorphism:
kla : (FK g a ~> {b}) -> (a -> UK g {b})
kra : (a -> UK g {b}) -> (FK g a ~> {b})
-- kla and kra mirror leftAdjunct and rightAdjunct from Data.Functor.Adjunction.
-- The underlying Haskell type is a -> g b on both sides, so we can simply have:
kla = id
kra = id

В соответствии с Three у Саймона С, в качестве монады функций будем иметь g, на которой будет построен трансформатор. Трансформатор будет каким-то образом включать в себя эффекты другой монады Hask, m, которую я иногда буду называть «базовой монадой», следуя обычной терминологии Haskell.

Если мы попытаемся сжать m между FK g и UK g, мы столкнемся со вторым вопросом, упомянутым выше: нам понадобится эндофунктор Kleisli- g, а не Hask. Больше нечего делать, кроме как сделать это. Под этим я подразумеваю, что мы можем определить функтор для функторов (точнее, функтор между двумя категориями эндофункторов), который, мы надеемся, превратит m в то, что мы можем использовать. Я назову этот «высший» функтор HK g. Применение этого к m должно дать что-то вроде этого:

-- Keep in mind this is a Kleisli-g endofunctor.
HK g m : {a}                |-> {m a}
         f : {a} ~> {b}     |-> kmap f : {m a} ~> {m b} ~ m a -> g (m b)
-- This is the object mapping, taking functors to functors.
-- The morphism mapping maps natural transformations, a la Control.Monad.Morph:
         t : ∀x. m x -> n x |-> kmorph t : ∀x. {m x} ~> {n x} ~ ∀x. m x -> g (n x)
-- I won't use it explicitly, but it is there if you look for it.

Клейсли на Клейсли

(Примечание: впереди многозначительный категоричный поворот. Если вы спешите, смело переходите к подразделу «Сводка».)

UK g . HK g m . FK g будет эндофунктором Hask, аналогом Three конструкции. Далее мы хотим, чтобы это была монада на Хаске. Мы можем убедиться в этом, настроив HK g m как монаду в категории Kleisli- g. Это означает, что нам нужно выяснить аналоги fmap, return и join на Kleisli- g:

kmap : {a} ~> {b} |-> {m a} ~> {m b}
       (a -> g b)  ->  m a -> g (m b)

kreturn : {a} ~> {m a}
          a -> g (m a)

kjoin : {m (m a)} ~> {m a}
        m (m a) -> g (m a) 

Для kreturn и kjoin, давайте попробуем простейшие вещи, которые могли бы работать:

kreturn :: (Monad g, Monad m) => a -> g (m a)
kreturn = return . return 

kjoin :: (Monad g, Monad m) => m (m a) -> g (m a)
kjoin = return . join

kmap несколько хитрее. fmap @m выдаст m (g a) вместо g (m a), поэтому нам нужен способ вытащить слой g наружу. Как это бывает, есть удобный способ сделать это, но он требует g, чтобы быть a Distributive функтором :

kmap :: (Monad g, Distributive g, Monad m) => (a -> g b)  ->  m a -> g (m b)
kmap f = distribute . fmap f  -- kmap = collect

Законы и условия распределения

Эти предположения, конечно, ничего не значат, если мы не докажем, что они законны:

-- Functor laws for kmap
kmap return = return
kmap g <=< kmap f = kmap (g <=< f)

-- Naturality of kreturn
kmap f <=< kreturn = kreturn <=< f

-- Naturality of kjoin
kjoin <=< kmap (kmap f) = kmap f <=< kjoin

-- Monad laws
kjoin <=< kreturn = return
kjoin <=< kmap kreturn = return
kjoin <=< kmap kjoin = kjoin <=< kjoin

Отработка показывает, что четыре условия для составления монад с распределительным законом достаточны для обеспечения соблюдения законов:

-- dist :: t (g a) -> g (t a)
-- I'm using `dist` instead of `distribute` and `t` instead of `m` here for the
-- sake of notation neutrality. 
dist . fmap (return @g) = return @g                 -- #1
dist . return @t = fmap (return @t)                 -- #2
dist . fmap (join @g) = join @g . fmap dist . dist  -- #3
dist . join @t = fmap (join @t) . dist . fmap dist  -- #4
-- In a nutshell: dist must preserve join and return for both monads.

В нашем случае условие # 1 дает kmap идентичность, kjoin правильная идентичность и kjoin ассоциативность;# 2 дает kreturn естественность;№ 3, функторная композиция;# 4, kjoin естественность (kjoin левая идентичность не зависит ни от одного из четырех условий).Окончательная проверка вменяемости устанавливает, что требуется для выполнения самих условий.В конкретном случае distribute его очень сильные естественные свойства означают, что для любого законного Distributive обязательно выполняются четыре условия, так что нам пора.

Подводя итоги

Вся монада UK g . HK g m . FK g может быть получена из частей, которые у нас уже есть, путем разбиения HK g m на присоединение Клейсли, которое полностью аналогично присоединению Клейсли, с которого мы начинали, за исключением того, что мы начинаем с Klesili -g, а не с Hask:

HK g m = UHK g m . FHK g m

FHK g m : {a}        |-> <{a}>
      f : {a} ~> {b} |-> fmap return . f : <{a}> ~> <{b}> ~ a -> g (m b)
-- kreturn <=< f = fmap (return @m) . f
-- Note that m goes on the inside, so that we end up with a morphism in Kleisli g.

UHK g m : <{a}>          |-> {m a}
      f : <{a}> ~> <{b}> |-> fmap join . distribute . fmap f : {m a} ~> {m b} ~ m a -> g (m b)
-- kjoin <=< kmap f = fmap (join @m) . distribute . fmap f

-- The adjunction isomorphism:
hkla : (FHK g m {a} ~> <{b}>) -> ({a} ~> UHK g m <{b}>)
hkra : ({a} ~> UHK g m <{b}>) -> (FHK g m {a} ~> <{b}>)
-- Just like before, we have:
hkla = id
hkra = id

-- And, for the sake of completeness, a Kleisli composition operator:
-- g <~< f = kjoin <=< kmap g <=< f
(<~<) :: (Monad g, Distributive g, Monad m)
    => (b -> g (m c)) -> (a -> g (m b)) -> (a -> g (m c))
g <~< f = fmap join . join . fmap (distribute . fmap g) . f

Теперь, когда у нас есть два присоединения, мы можем составить их, что приведет к присоединению трансформатора и, наконец, к return и join для трансформатора:

-- The composition of the three morphism mappings in UK g . HK g m . FK g
-- tkmap f = join . fmap (kjoin <=< kmap (kreturn <=< return . f))
tkmap :: (Monad g, Distributive g, Monad m) => (a -> b) -> g (m a) -> g (m b)
tkmap = fmap . fmap

-- Composition of two adjunction units, suitably lifted through the functors.
-- tkreturn = join . fmap (hkla hkid) . kla kid = join . fmap kreturn . return
tkreturn :: (Monad g, Monad m) => a -> g (m a)
tkreturn = return . return

-- Composition of the adjunction counits, suitably lifted through the functors.
-- tkjoin = join . fmap (kjoin <=< kmap (hkra kid <~< (kreturn <=< kra id)))
--    = join . fmap (kjoin <=< kmap (return <~< (kreturn <=< id)))
tkjoin :: (Monad g, Distributive g, Monad m) => g (m (g (m a))) -> g (m a)
tkjoin = fmap join . join . fmap distribute

(Для категориального объяснения состава единиц и количеств см. Эмили Рил, Теория категорий в контексте , предложение 4.4.4.)

Что касается liftkmap (return @g) звучит как разумное определение.Это составляет distribute . fmap return (сравните с lift из ответа Бенджамина Ходжсона на вопрос Саймона С ), что по условию # 1 становится просто:

tklift :: m a -> g (m a)
tklift = return

MonadLiftзаконы, которые означают, что tklift должен быть морфизмом монады, действительно имеют место, с законом join, зависящим от условия дистрибутивности # 1:

tklift . return = tkreturn
tklift . join = tkjoin . tkmap tklift . tklift

В итоге

Присоединение Клейсли позволяетнам построить трансфомер из любой Distributive монады, составив его снаружи любой другой монады.Собрав все это вместе, мы имеем:

-- This is still a Three, even though we only see two Hask endofunctors.
-- Or should we call it FourK?
newtype ThreeK g m a = ThreeK { runThreeK :: g (m a) }

instance (Functor g, Functor m) => Functor (ThreeK g m) where
    fmap f (ThreeK m) = ThreeK $ fmap (fmap f) m

instance (Monad g, Distributive g, Monad m) => Monad (ThreeK g m) where
    return a = ThreeK $ return (return a)
    m >>= f = ThreeK $ fmap join . join . fmap distribute 
        $ runThreeK $ fmap (runThreeK . f) m

instance (Monad g, Distributive g, Monad m) => Applicative (ThreeK g m) where
    pure = return
    (<*>) = ap

instance (Monad g, Distributive g) => MonadTrans (ThreeK g) where
    lift = ThreeK . return

Наиболее существенным примером Distributive является функтор функции.При составлении его на внешней стороне другой монады выдается ReaderT:

newtype KReaderT r m a = KReaderT { runKReaderT :: r -> m a }
    deriving (Functor, Applicative, Monad) via ThreeK ((->) r) m
    deriving MonadTrans via ThreeK ((->) r)

* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *

*Присоединение Мура

В приведенном выше выводе мы уложили базовое присоединение монады Клесли поверх присоединения монады объектов.Мы могли бы сделать это наоборот и начать с присоединения базовой монады.Важное изменение, которое произойдет, произойдет при определении kmap.Поскольку базовой монадой, в принципе, может быть любая монада, мы бы не хотели накладывать на нее ограничение Distributive, чтобы ее можно было вытянуть наружу, как мы это сделали с g в приведенном выше выводе.Лучше всего подойдет для нашего игрового плана двойное требование Traversable от монады функций, чтобы его можно было вставить внутрь с помощью sequenceA.Это приведет к появлению трансформатора, который будет составлять монаду feture изнутри, а не снаружи.Я назвал это ThreeEM, потому что оно также может быть получено с помощью дополнений Эйленберга-Мура (вместо Клейсли) и сложения их с базовой монадой на вершине, как в Three Симона С.Этот факт, вероятно, имеет отношение к двойственности между присоединениями Эйленберга-Мура и Клесили.

newtype ThreeEM t m a = ThreeEM { runThreeEM :: m (t a) }

instance (Functor t, Functor m) => Functor (ThreeEM t m) where
    fmap f (ThreeEM m) = ThreeEM $ fmap (fmap f) m

instance (Monad t, Traversable t, Monad m) => Monad (ThreeEM t m) where
    return a = ThreeEM $ return (return a)
    m >>= f = ThreeEM $ fmap join . join . fmap sequenceA 
      $ runThreeEM $ fmap (runThreeEM . f) m

instance (Monad t, Traversable t, Monad m) => Applicative (ThreeEM t m) where
    pure = return
    (<*>) = ap

-- In terms of of the Kleisli construction: as the bottom adjunction is now the
-- base monad one, we can use plain old fmap @m instead of kmap to promote return. 
instance (Monad t, Traversable t) => MonadTrans (ThreeEM t) where
    lift = ThreeEM . fmap return

Обычные трансформаторы, которые возникают таким образом, включают MaybeT и ExceptT.

В этой конструкции есть одна потенциальная ловушка.sequenceA должен следовать условиям дистрибутивности, чтобы экземпляры были законными.Однако его ограничение Applicative делает его свойства естественности намного слабее, чем у distribute, и поэтому условия не все выполняются бесплатно:

  • Условие № 1 выполняетдержись: это является следствием законов об идентичности и натуральности Traversable.

  • Условие № 2 также выполняется: sequenceA сохраняет естественные преобразования на проходимом функторе, пока эти преобразования сохраняют toList. Если мы рассматриваем return как естественное преобразование из Identity, это немедленно сохраняет регистр.

  • Условие № 3, однако, не гарантируется. Это будет иметь место, если join @m, взятый как естественное преобразование из Compose m m, сохранится (<*>), но это может быть не так. Если sequenceA на самом деле последовательность эффектов (то есть, если traversable может содержать более одного значения), любые различия, вытекающие из порядка, в котором join и (<*>) выполняются в базовой монаде, приведет к нарушению условия , Это, кстати, является частью пресловутой проблемы «ListT сделано неправильно»: ListT в трансформаторах, построенных в соответствии с этой конструкцией, является законным, только если используется с коммутативными базовыми монадами.

  • Наконец, условие # 4 выполняется, только если join @t, взятый как естественное преобразование из Compose t t, сохраняет toList (то есть, если оно не удаляет, не дублирует или не переставляет элементы). Одним из следствий этого является то, что эта конструкция не будет работать для монад объектов, у которых join «принимает диагональ» вложенной структуры (как это обычно имеет место для монад, которые также являются экземплярами Distributive), даже если мы попытаемся переписать условие № 3, ограничиваясь коммутативными базовыми монадами.

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

Другие возможности

Конструкции, описанные к настоящему времени, требуют, чтобы монада признаков была Distributive или Traversable, соответственно. Общая стратегия, однако, совсем не специфична для присоединений Клейсли и Эйленберга-Мура, поэтому вполне возможно попробовать ее, используя другие дополнения. Тот факт, что присоединение карри приводит к StateT через Three / AdjointT Саймона С, даже если State не является ни Distributive, ни Traversable, может указывать на то, что такие попытки могут быть плодотворными. Однако я не настроен оптимистично.

В связанном обсуждении в другом месте Бенджамин Ходжсон предполагает, что все присоединения, вызывающие монаду, ведут к одному и тому же трансформатору. Это звучит очень правдоподобно, учитывая, что все такие присоединения через уникальные функторы связаны как с добавками Клейсли, так и с Эйленбергом-Муром (см. Теория категорий в контексте , предложение 5.2.12). Показательный пример: если мы попытаемся List с конструкцией ThreeK, но с использованием свободного / забывчивого присоединения к категории моноидов вместо Kleisli- [], мы получим преобразователь m [] ThreeEM / Конструкция "функция на внутренней стороне" дала бы нам, вплоть до "ListT, сделанного неправильно, проблему" необходимости join быть аппликативным гомоморфизмом.

А как же State и его третье присоединение, производящее трансформатор, тогда? Хотя я не проработал это подробно, я подозреваю, что более уместно думать о distribute и sequenceA, как они используются в конструкциях здесь, как о принадлежащих правой и левой смежных областях, соответственно, а не как о вся особенность монады. В случае distribute это будет означать выход за пределы сигнатуры типа Haskell ...

distribute :: (Distribute g, Functor m) => m (g a) -> g (m a)

... чтобы увидеть естественное преобразование между функторами Kleisli- g -to-Hask:

distribute  : m . UK g |-> UK g . HK g m

Если я прав в этом, можно будет перевернуть этот ответ и переосмыслить конструкцию Three / AdjointT в терминах присоединения Клейсли к монаде объектов. Если это так, State совсем не говорит нам о других монадах функций, которые не являются ни Distributive, ни Traversable.

ListT сделано правильно

Стоит также отметить, что не все трансформаторы возникают из-за смешивания монадических эффектов с составом соединений, как мы видели здесь. В трансформаторы , ContT и [SelectT не следуют шаблону; однако я бы сказал, что они слишком дурацкие, чтобы обсуждать их в этом контексте («не функтор в категории монад», , как указывают документы ). Лучший пример представлен различными реализациями "ListT сделано правильно" , которые позволяют избежать проблем незаконности, связанных с sequenceA (а также потери потоковой передачи), путём смешивания эффектов базовой монады это не требует последовательности их в привязке трансформатора. Вот эскиз реализации, в иллюстративных целях:

-- A recursion-schemes style base functor for lists.
data ListF a b = Nil | Cons a b
    deriving (Eq, Ord, Show, Functor)

-- A list type might be recovered by recursively filling the functorial
-- position in ListF.
newtype DemoList a = DemoList { getDemoList :: ListF a (DemoList a) }

-- To get the transformer, we compose the base monad on the outside of ListF.
newtype ListT m a = ListT { runListT :: m (ListF a (ListT m a)) }
    deriving (Functor, Applicative, Alternative) via WrappedMonad (ListT m)

-- Appending through the monadic layers. Note that mplus only runs the effect
-- of the first ListF layer; everything eslse can be consumed lazily.
instance Monad m => MonadPlus (ListT m) where
    mzero = ListT $ return Nil
    u `mplus` v = ListT $ runListT u >>= \case
        Nil -> runListT v
        Cons a u' -> return (Cons a (u' `mplus` v))

-- The effects are kept apart, and can be consumed as they are needed.
instance Monad m => Monad (ListT m) where
    return a = ListT $ pure (Cons a mzero)
    u >>= f = ListT $ runListT u >>= \case
        Nil -> return Nil
        Cons a v -> runListT $ f a `mplus` (v >>= f)

instance MonadTrans ListT where
    lift m = ListT $ (\a -> Cons a mzero) <$> m

В этом ListT базовые эффекты монады отсутствуют ни внутри, ни снаружи списка. Скорее, они прикреплены болтами к корешку списка и сделаны материальными благодаря определению типа в терминах ListF.

Связанные преобразователи, которые построены подобным образом, включают в себя трансформатор свободной монады FreeT, а также основные монадные трансформаторы из эффективных потоковых библиотек (не случайно, что «ListT сделан правильно» "ссылка, которую я включил выше, указывает на документацию трубы ).

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

...