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
(Обратите внимание, что от m требуется не более Functor, как ожидается для перемещаемых контейнеров, которые содержат ровно одно значение.)
Все, что здесь отсутствует, - это проверка эквивалентности обеих реализаций 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, больше никого не должны беспокоить.
P.S .: Стоит отметить, что приведенное здесь определение 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 взаимоопределимы.
person
duplode
schedule
17.03.2018
(>>=)реализация может быть упрощена доm >>= f = Three $ fmap (>>= counit . fmap (getThree . f)) (getThree m)- person duplode schedule 17.03.2018