Comment factoriser la monade de continuation en joints gauche et droit?

En tant qu'État, la monade peut être factorisée en produit (gauche - fonction) et lecteur (droite - représentable).

1. Existe-t-il un moyen de factoriser la Monade de Continuation? Ci-dessous le code est ma tentative, qui ne vérifiera pas le type

-- 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. Existe-t-il une liste des Adjoints Gauche et Droits qui forment des monades?

3. J'ai lu que, étant donné une paire d'adjoints, ils forment une monade et une comonade uniques mais, étant donné une monade, elle peut être factorisée en plusieurs facteurs. Y a-t-il un exemple de cela?

Cela ne vérifie pas le type car la classe Adjunctionne représente qu'un petit sous-ensemble d'adjonctions, où les deux foncteurs sont des endofoncteurs sur Hask .

Il s'avère que ce n'est pas le cas pour l'adjonction (<-:) r -| (<-:) r. Il existe ici deux foncteurs subtilement différents:

• f = (<-:) r, le foncteur de Hask à Op (Hask) (la catégorie opposée de Hask, parfois aussi appelée Hask ^ op)
• g = (<-:) r, le foncteur d'Op (Hask) à Hask

En particulier, le counitdevrait être une transformation naturelle dans la catégorie Op (Hask), qui inverse les flèches:

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

En fait, counitcoïncide avec unitdans cette adjonction.

Pour capturer cela correctement, nous devons généraliser les classes Functoret Adjunctionafin de pouvoir modéliser les adjonctions entre différentes catégories:

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

Ensuite, nous obtenons à nouveau qui Composeest une monade (et une comonade si nous inversons l'adjonction):

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

et Contn'est qu'un cas particulier de cela:

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

Voir également cet essentiel pour plus de détails: https://gist.github.com/Lysxia/beb6f9df9777bbf56fe5b42de04e6c64

J'ai lu que, étant donné une paire d'adjoints, ils forment une monade et une comonade uniques, mais étant donné une monade, elle peut être factorisée en plusieurs facteurs. Y a-t-il un exemple de cela?

La factorisation n'est généralement pas unique. Une fois que vous avez généralisé les adjonctions comme ci-dessus, vous pouvez au moins factoriser n'importe quelle monade Mcomme une adjonction entre sa catégorie Kleisli et sa catégorie de base (dans ce cas, 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 (=<<)

Je ne sais pas si la monade de continuation correspond à une adjonction entre endofuncteurs sur Hask.

Voir également l'article nCatLab sur les monades: https://ncatlab.org/nlab/show/monad#RelationToAdjunctionsAndMonadicity

Relation avec les adjonctions et la monadicité

Chaque adjonction (L ⊣ R) induit une monade R∘L et une comonade L∘R. Il y a en général plus d'une adjonction qui donne ainsi naissance à une monade donnée, en fait il y a une catégorie d'adjonctions pour une monade donnée. L'objet initial dans cette catégorie est l'adjonction sur la catégorie Kleisli de la monade et l'objet terminal est celui sur la catégorie d'algèbres Eilenberg-Moore. (par exemple Borceux, vol. 2, prop. 4.2.2) Ce dernier est appelé l'adjonction monadique.