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

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

11 голосов
/ 17 апреля 2020

Поскольку монаду State можно разложить на Product (слева - Functor) и Reader (Right - представимый).

  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 Ответ

11 голосов
/ 17 апреля 2020

Это не проверка типов, потому что класс Adjunction представляет только небольшое подмножество присоединений, где оба функтора являются endofunctors на 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) Последнее называется присоединением monadi c.

...