Как разложить монаду продолжения в левую и правую примыкания?

11

Как монаду состояния можно разложить на Product (слева - функтор) и Reader (справа - представимый).

  1. Есть ли способ разложить монаду продолжения? Ниже код моя попытка, которая не проверяет тип
-- To form a -> (a -> k) -> k
{-# LANGUAGE MultiParamTypeClasses, TypeOperators, InstanceSigs, TypeSynonymInstances #-}
type (<-:) o i = i -> o
-- I Dont think we can have Functor & Representable for this type synonym

class Isomorphism a b where
   from :: a -> b
   to :: b -> a

instance Adjunction ((<-:) e) ((<-:) e) where
   unit :: a -> (a -> e) -> e
   unit a handler = handler a

   counit :: (a -> e) -> e -> a
   counit f e = undefined -- If we have a constraint on Isomorphism a e then we can implement this

  1. Есть ли список Левых и Правых Адъюнктов, которые образуют монады?

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

haskell monads continuations category-theory comonad Паван Кумар
источник

Ответы:

11

Это не проверка типов, потому что класс Adjunctionпредставляет только небольшое подмножество присоединений, где оба функтора являются эндофункторами в Hask .

Оказывается, это не относится к присоединению (<-:) r -| (<-:) r. Здесь есть два тонко разных функтора:

  • f = (<-:) r, функтор от Hask к Op (Hask) (противоположная категория Hask, иногда также обозначаемая Hask ^ op)
  • g = (<-:) rФунктор из Оп (Хаск) в Хаск

В частности, counitдолжно быть естественное преобразование в категории Op (Hask), которая переворачивает стрелки вокруг:

unit   :: a -> g (f a)
counit :: f (g a) <-: a

На самом деле, counitсовпадает с unitэтим в присоединении.

Для того, чтобы захватить это правильно, мы должны обобщить Functorи Adjunctionклассы таким образом , мы можем моделировать примыкания между различными категориями:

class Exofunctor c d f where
  exomap :: c a b -> d (f a) (f b)

class
  (Exofunctor d c f, Exofunctor c d g) =>
  Adjunction
    (c :: k -> k -> Type)
    (d :: h -> h -> Type)
    (f :: h -> k)
    (g :: k -> h) where
  unit :: d a (g (f a))
  counit :: c (f (g a)) a

Затем мы снова получаем Composeмонаду (и комонаду, если мы перевернем присоединение):

newtype Compose f g a = Compose { unCompose :: f (g a) }
adjReturn :: forall c f g a. Adjunction c (->) f g => a -> Compose g f a
adjReturn = Compose . unit @_ @_ @c @(->)

adjJoin :: forall c f g a. Adjunction c (->) f g => Compose g f (Compose g f a) -> Compose g f a
adjJoin = Compose . exomap (counit @_ @_ @c @(->)) . (exomap . exomap @(->) @c) unCompose . unCompose

и Contэто просто частный случай этого:

type Cont r = Compose ((<-:) r) ((<-:) r)

См. Также эту суть для получения дополнительной информации: https://gist.github.com/Lysxia/beb6f9df9777bbf56fe5b42de04e6c64

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

Факторизация, как правило, не уникальна. После того, как вы Mобобщите дополнения, как указано выше, вы можете по меньшей мере учитывать любую монаду как присоединение между ее категорией Клейсли и ее базовой категорией (в данном случае, Hask).

Every monad M defines an adjunction
  F -| G
where

F : (->) -> Kleisli M
  : Type -> Type                -- Types are the objects of both categories (->) and Kleisli m.
                                -- The left adjoint F maps each object to itself.
  : (a -> b) -> (a -> M b)      -- The morphism mapping uses return.

G : Kleisli M -> (->)
  : Type -> Type                -- The right adjoint G maps each object a to m a
  : (a -> M b) -> (M a -> M b)  -- This is (=<<)

Я не знаю, соответствует ли монада продолжения соединению между эндофункторами на Hask.

См. Также статью nCatLab о монадах: https://ncatlab.org/nlab/show/monad#RelationToAdjunctionsAndMonadicity.

Отношение к приставкам и монадичности

Каждое присоединение (L ⊣ R) индуцирует монаду R∘L и комонаду L∘R. В общем случае существует более одного присоединения, которое приводит к данной монаде таким образом, фактически существует категория присоединений для данной монады. Начальный объект в этой категории - это присоединение над категорией монады Клейсли, а конечный объект - над алгеброй Эйленберга-Мура. (например, Borceux, vol. 2, prop. 4.2.2) Последнее называется монадическим присоединением.

Ли Яо Ся
источник