Jak faktoryzować monadę kontynuacji w lewy i prawy punkt pośredni?

Ponieważ monada stanu może być podzielona na produkt (lewy - Functor) i czytnik (prawy - reprezentowalny).

1. Czy istnieje sposób na uwzględnienie Monady kontynuacji? Poniżej kodu jest moja próba, która nie sprawdza typu

-- 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

2. Czy istnieje lista powiązań lewicy i praw, które tworzą monady?

3. Czytałem, że biorąc pod uwagę parę przyłączy, tworzą one unikalną Monadę i Comonadę, ale biorąc pod uwagę Monadę, można ją podzielić na wiele czynników. Czy jest na to jakiś przykład?

To nie sprawdza typu, ponieważ klasa Adjunctionreprezentuje tylko niewielki podzbiór adiustacji , w których oba funktory są endofunkcjonariuszami Hask .

Jak się okazuje, nie ma to miejsca w przypadku dodatku (<-:) r -| (<-:) r. Istnieją tutaj dwa subtelnie różne funktory:

• f = (<-:) r, funktor od Hask do Op (Hask) (przeciwna kategoria Hask, czasami również oznaczana Hask ^ op)
• g = (<-:) r, funktor z Op (Hask) do Hask

W szczególności counitpowinna to być naturalna transformacja w kategorii Op (Hask), która odwraca strzałki:

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

W rzeczywistości counitzbiega się z unittym dodatkiem .

Aby odpowiednio to uchwycić, musimy uogólnić FunctorAdjunction klasy i , abyśmy mogli modelować połączenia między różnymi kategoriami:

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

Następnie otrzymujemy ponownie, że Composejest to monada (i comonada, jeśli odwrócimy dodatek):

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

i Cont jest to tylko szczególny przypadek:

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

Aby uzyskać więcej informacji, zobacz także tę treść: https://gist.github.com/Lysxia/beb6f9df9777bbf56fe5b42de04e6c64

Czytałem, że biorąc pod uwagę parę przyłączy tworzą one unikalną Monadę i Comonadę, ale biorąc pod uwagę Monadę, można ją podzielić na wiele czynników. Czy jest na to jakiś przykład?

Faktoryzacja na ogół nie jest wyjątkowa. Po uogólnieniu dopasowań jak wyżej, możesz przynajmniej uwzględnić dowolną monadęM jako połączenie między jej kategorią Kleisli a kategorią podstawową (w tym przypadku 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 (=<<)

Nie wiem, czy monada kontynuacji odpowiada połączeniu między endofunkcjami na Hask.

Zobacz także artykuł nCatLab na temat monad: https://ncatlab.org/nlab/show/monad#RelationToAdjunctionsAndMonadicity

Związek z adiunkcjami i monadycznością

Każde połączenie (L ⊣ R) wywołuje monadę R∘L i comonadę L∘R. Na ogół istnieje więcej niż jedno dopasowanie, które powoduje powstanie danej monady w ten sposób, w rzeczywistości istnieje kategoria dopasowania dla danej monady. Początkowym obiektem w tej kategorii jest połączenie między kategorią monady Kleisli, a przedmiotem końcowym jest to nad algebrami kategorii Eilenberga-Moore'a. (np. Borceux, vol. 2, prop. 4.2.2) Ten ostatni nazywa się łączeniem monadycznym.