Сопутствующие функторы определяют монадные трансформаторы, но где их поднять?

Question

Я заинтригован описанной здесь конструкцией для определения монадного преобразователя из сопряженных функторов. Вот некоторый код, который обобщает основную идею:

{-# LANGUAGE MultiParamTypeClasses #-}

import           Control.Monad

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

class (Functor f, Functor g) => Adjoint f g where
  counit :: f (g a) -> a
  unit   :: a -> g (f a)

instance (Adjoint f g, Monad m) => Monad (Three g f m) where
  return  = Three . fmap return . unit
  m >>= f = Three $ fmap (>>= counit . fmap (getThree . f)) (getThree m)

instance (Adjoint f g, Monad m) => Applicative (Three g f m) where
  pure  = return
  (<*>) = ap

instance (Adjoint f g, Monad m) => Functor (Three g f m) where
  fmap = (<*>) . pure

При условии Adjoint ((,) s) ((->) s), Three ((->) s) ((,) s) кажется эквивалентным StateT s,

Очень круто, но я озадачен парой вещей:

• Как мы можем обновить монадический m a в монадический Three g f m a? Для конкретного случая Three ((->) s) ((,) s)Конечно, очевидно, как это сделать, но, кажется, желательно иметь рецепт, который работает для любого Three g f при условии, что Adjoint f g, Другими словами, похоже, что должен быть аналог lift чье определение требует только unit, counitи return а также >>= входной монады. Но я не могу найти один (я видел определение, используяsequence, но это похоже на обман, так как это требует f быть Traversable).

• В этом отношении, как мы можем обновить g a в Three g f m a (предоставлена Adjoint f g)? Опять же, для конкретного случая Three ((->) s) ((,) s) очевидно, как это сделать, но мне интересно, есть ли аналог gets это требует только unit, counitи return а также >>= входной монады.

Answer 1

lift В ответе Бенджамина Ходжсона это выглядит так:

lift mx = let mgfx = fmap unit mx
              gmfx = distributeR mgfx
          in Three gmfx
-- or
lift = Three . distributeR . fmap unit

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

lift mx = let gfmx = unit mx
              gmfx = fmap sequenceL gfmx
          in Three gmfx
-- or
lift = Three . fmap sequenceL . unit

Откуда Traversable требование для соответствующего Эдварда Кметта MonadTrans экземпляр происходит. Тогда возникает вопрос: а не полагаться ли на это, как вы выразились, на "обман"? Я собираюсь утверждать, что это не так.

Мы можем адаптировать план игры Бенджамина относительно Distributiveи правые смежные и попытаться найти, являются ли левые смежныеTraversable, Взгляд наData.Functor.Adjunction показывает, что у нас есть неплохой набор инструментов для работы:

unabsurdL :: Adjunction f u => f Void -> Void
cozipL :: Adjunction f u => f (Either a b) -> Either (f a) (f b)
splitL :: Adjunction f u => f a -> (a, f ())
unsplitL :: Functor f => a -> f () -> f a

Эдвард услужливо говорит нам, что unabsurdL а также cozipL свидетельствуйте, что "[левый сопряженный должен быть заселен, и [что] левый сопряженный должен быть заселен ровно одним элементом", соответственно. Это, однако, означает, splitL точно соответствует разложению формы и содержания, которое характеризует Traversable функторы. Если добавить к этому тот факт, что splitL а также unsplitL обратные, реализация sequence следует сразу:

sequenceL :: (Adjunction f u, Functor m) => f (m a) -> m (f a)
sequenceL = (\(mx, fu) -> fmap (\x -> unsplitL x fu) mx) . splitL

(Обратите внимание, что не более Functor требуется от m, как и ожидалось для перемещаемых контейнеров, которые содержат ровно одно значение.)

Все, чего не хватает на этом этапе, это проверки того, что обе реализации lift эквивалентны. Это не сложно, только немного трудоемко. Короче говоря, distributeR а также sequenceR Определения здесь могут быть упрощены до:

distributeR = \mgx ->
    leftAdjunct (\fa -> fmap (\gx -> rightAdjunct (const gx) fa) mgx) ()   
sequenceL =
    rightAdjunct (\mx -> leftAdjunct (\fu -> fmap (\x -> fmap (const x) fu) mx) ())

Мы хотим показать, что distributeR . fmap unit = fmap sequenceL . unit, После нескольких раундов упрощения мы получаем:

distributeR . fmap unit = \mgx ->
    leftAdjunct (\fa -> fmap (\gx -> rightAdjunct (const (unit gx)) fa) mgx) ()
fmap sequenceL . unit = \mx ->
    leftAdjunct (\fu -> fmap (\x -> fmap (const x) fu) mx) ()

Мы можем показать, что это действительно одно и то же, выбрав \fu -> fmap (\x -> fmap (const x) fu) mx - аргумент leftAdjunct во второй правой части - и скольжения rightAdjunct unit = counit . fmap unit = id внутрь:

\fu -> fmap (\x -> fmap (const x) fu) mx
\fu -> fmap (\x -> fmap (const x) fu) mx
\fu -> fmap (\x -> (counit . fmap unit . fmap (const x)) fu) mx
\fu -> fmap (\x -> rightAdjunct (unit . const x) fu) mx
\fu -> fmap (\x -> rightAdjunct (const (unit x)) fu) mx
-- Sans variable renaming, the same as
-- \fa -> fmap (\gx -> rightAdjunct (const (unit gx)) fa) mgx

Вывод в том, что Traversable маршрут к вашему MonadTrans так же безопасен, как и Distributive один, и опасения по этому поводу - в том числе упомянутые Control.Monad.Trans.Adjoint документация - больше не должна никого беспокоить.

PS: Стоит отметить, что определение lift Выдвинутые здесь можно записать как:

lift = Three . leftAdjunct sequenceL

То есть, lift является sequenceL отправлено через изоморфизм присоединения. Кроме того, из...

leftAdjunct sequenceL = distributeR . fmap unit

... если мы применим rightAdjunct с обеих сторон мы получаем...

sequenceL = rightAdjunct (distributeR . fmap unit)

... и если мы сочиняем fmap (fmap counit) слева от обеих сторон мы в итоге получим:

distributeR = leftAdjunct (fmap counit . sequenceL)

Так distributeR а также sequenceL являются определяемыми.

Answer 2

Как мы можем обновить монадический m a в монадический Three g f m a?

Хороший вопрос. Время для игры в теннис типа!

-- i'm using Adjuction from the adjunctions package because I'll need the fundeps soon
lift :: Adjunction f g => m a -> Three g f m a
lift mx = Three _

Отверстие набрано g (m (f a)), У нас есть mx :: m a по объему и, конечно, unit :: a -> g (f a) а также fmap :: (a -> b) -> m a -> m b,

lift mx = let mgfx = fmap unit mx
          in Three $ _ mgfx

Теперь это _ :: m (g (f a)) -> g (m (f a)), Это distribute если g является Distributive,

lift mx = let mgfx = fmap unit mx
              gmfx = distributeR mgfx
          in Three gmfx
-- or
lift = Three . distributeR . fmap unit

Так что теперь нам просто нужно доказать, что правая часть присоединения всегда Distributive:

distributeR :: (Functor m, Adjunction f g) => m (g x) -> g (m x)
distributeR mgx = _

Так как нам нужно вернуть g Четкий выбор методов из Adjunction является leftAdjunct :: Adjunction f g => (f a -> b) -> a -> g b, который использует unit создать g (f a) а затем сносит внутреннюю f a от fmap пинг функции.

distributeR mgx = leftAdjunct (\fa -> _) _

Сначала я собираюсь атаковать первую лунку, ожидая, что ее заполнение может рассказать мне кое-что о второй лунке. Первое отверстие имеет тип m a, Единственный способ получить m любого типа является fmap что-нибудь пропинговать mgx,

distributeR mgx = leftAdjunct (\fa -> fmap (\gx -> _) mgx) _

Теперь первая дыра имеет тип a, и у нас есть gx :: g a в рамках. Если бы у нас был f (g a) мы могли бы использовать counit, Но у нас есть f x (где x в настоящее время является неопределенной переменной типа) и g a в рамках.

distributeR mgx = leftAdjunct (\fa -> fmap (\gx -> counit (fa $> gx)) mgx) _

Оказывается, что оставшееся отверстие имеет неоднозначный тип, поэтому мы можем использовать все, что захотим. (Это будет игнорироваться $>.)

distributeR mgx = leftAdjunct (\fa -> fmap (\gx -> counit (fa $> gx)) mgx) ()

---

Этот вывод мог показаться волшебным трюком, но на самом деле вы просто лучше тренируетесь в теннисе. Навык игры заключается в умении смотреть на типы и применять интуицию и факты об объектах, с которыми вы работаете. Посмотрев на типы, я мог сказать, что мне нужно будет обменяться m а также g и обход m был не вариант (потому что m не обязательно Traversable) так что-то вроде distribute собирался быть необходимым.

Помимо догадки мне нужно было реализовать distribute Я руководствовался некоторыми общими знаниями о том, как работают дополнения.

В частности, когда вы говорите о * -> * единственные интересные дополнения (однозначно изоморфны) Reader / Writer примыкание. В частности, это означает, что любое право присоединяется к Hask всегда Representable как свидетельствует tabulateAdjunction а также indexAdjunction, Я также знаю, что все Representable функторы Distributive (на самом деле логически обратное также верно, как описано в Distributive документы, даже если классы не эквивалентны по мощности), в соответствии с distributeRep,

---

В этом отношении, как мы можем обновить g a в Three g f m a (предоставлена Adjoint f g)?

Я оставлю это как упражнение. Я подозреваю, что вам нужно опираться на g ~ ((->) s) опять изоморфизм. Я на самом деле не ожидаю, что это будет верно для всех дополнений, только те, на Hask из которых есть только один.