Quelles sont les paires de foncteurs adjoints correspondant aux monades communes en Haskell ?

Question

En théorie des catégories, une monade peut être construite à partir de deux foncteurs adjoints. En particulier, si C et D sont des catégories et F : C --> D et G : D --> C sont des foncteurs adjoints, dans le sens où il existe une bijection

hom(FX,Y) = hom(X,GY)

pour chaque X sur C et Y sur D alors la composition G o F : C --> C est une monade.

---

Une telle paire de foncteurs adjoints peut être donnée en fixant un type b et en prenant F et G à être

data F b a = F (a,b)
data G b a = G (b -> a)

instance Functor (F b) where
  fmap f (F (a,b)) = F (f a, b)

instance Functor (G b) where
  fmap f (G g) = G (f . g)

et la bijection entre hom-ensembles est donnée (modulo les constructeurs) par la curie :

iso1 :: (F b a -> c) -> a -> G b c
iso1 f = \a -> G $ \b -> f (F (a,b))

iso2 :: (a -> G b c) -> F b a -> c
iso2 g = \(F (a,b)) -> let (G g') = g a in g' b

auquel cas la monade correspondante est

data M b a = M { unM :: b -> (a,b) }

instance Monad (M b) where
    return a    = M (\b -> (a,b))
    (M f) >>= g = M (\r -> let (a,r') = f r in unM (g r') a)

Je ne sais pas quel devrait être le nom de cette monade, si ce n'est qu'elle semble être quelque chose comme une monade de lecture qui transporte un élément d'information réinscriptible ( éditer : dbaupp fait remarquer dans les commentaires qu'il s'agit de la State monade).

Ainsi, le State peut être "décomposée" comme une paire de foncteurs adjoints F et G et nous pourrions écrire

State = G . F

Jusqu'à présent, tout va bien.

---

J'essaie maintenant de trouver comment décomposer d'autres monades communes en paires de foncteurs adjoints, par exemple Maybe , [] , Reader , Writer , Cont - mais je n'arrive pas à comprendre en quoi consistent les paires de foncteurs adjoints dans lesquelles nous pouvons les "décomposer".

Le seul cas simple semble être le Identity qui peut être décomposée en une paire quelconque de foncteurs F et G de telle sorte que F est l'inverse de G (en particulier, vous pourriez simplement prendre F = Identity et G = Identity ).

Quelqu'un peut-il m'éclairer ?

Answer 1

Ce que vous cherchez, c'est Catégorie Kleisli . Elle a été développée à l'origine pour montrer que toute monade peut être construite à partir de deux foncteurs adjoints.

Le problème est que Haskell Functor n'est pas un foncteur générique, c'est un endo-foncteur dans la catégorie Haskell. Nous avons donc besoin de quelque chose de différent (AFAIK) pour représenter les foncteurs entre les autres catégories :

{-# LANGUAGE FunctionalDependencies, KindSignatures #-}
import Control.Arrow
import Control.Category hiding ((.))
import qualified Control.Category as C
import Control.Monad

class (Category c, Category d) => CFunctor f c d | f -> c d where
    cfmap :: c a b -> d (f a) (f b)

Remarquez que si nous prenons -> pour les deux c et d on obtient un endo-foncteur de la catégorie Haskell, qui est juste le type de fmap :

cfmap :: (a -> b) -> (f a -> f b)

Nous avons maintenant une classe de type explicite qui représente les foncteurs entre deux catégories données. c et d et nous pouvons exprimer les deux foncteurs adjoints pour une monade donnée. Celui de gauche fait correspondre un objet a pour juste a et fait correspondre un morphisme f à (return .) f :

-- m is phantom, hence the explicit kind is required
newtype LeftAdj (m :: * -> *) a = LeftAdj { unLeftAdj :: a }
instance Monad m => CFunctor (LeftAdj m) (->) (Kleisli m) where
    cfmap f = Kleisli $ liftM LeftAdj . return . f . unLeftAdj
    -- we could also express it as liftM LeftAdj . (return .) f . unLeftAdj

Le bon correspond à un objet a à l'objet m a et fait correspondre un morphisme g à join . liftM g ou, de manière équivalente, à (=<<) g :

newtype RightAdj m a = RightAdj { unRightAdj :: m a }
instance Monad m => CFunctor (RightAdj m) (Kleisli m) (->) where
    cfmap (Kleisli g) = RightAdj . join . liftM g . unRightAdj
    -- this can be shortened as RightAdj . (=<<) g . unRightAdj

(Si quelqu'un connaît une meilleure façon d'exprimer cela en Haskell, merci de me le faire savoir).

Answer 2

• Maybe provient du foncteur libre dans la catégorie des ensembles pointus et du foncteur oublieux en retour.
• [] vient du foncteur libre dans la catégorie des monoïdes et du foncteur oublieux en retour.

Mais aucune de ces catégories n'est une sous-catégorie de Hask.

Answer 3

Comme vous l'avez observé, chaque paire de foncteurs adjoints donne naissance à une monade. L'inverse est également vrai : chaque monade naît de cette manière. En fait, elle le fait de deux manières canoniques. L'une est la construction de Kleisli décrite par Petr, l'autre est la construction d'Eilenberg-Moore. En effet, Kleisli est la voie initiale et E-M la voie terminale, dans une catégorie appropriée de paires de foncteurs adjoints. Elles ont été découvertes indépendamment en 1965. Si vous voulez plus de détails, je vous recommande vivement le livre Vidéos des chats .