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

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

  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
person Pawan Kumar    schedule 17.04.2020    source источник

Ответы (1)


arrow_upward
18
arrow_downward

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

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

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

В частности, 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) Последнее называется монадическим присоединением.

person Li-yao Xia    schedule 17.04.2020