Existe-t-il une monade qui n'a pas de transformateur de monade correspondant (sauf IO) ?

Question

Jusqu'à présent, chaque monade (qui peut être représentée comme un type de données) que j'ai rencontrée avait un transformateur de monade correspondant, ou pouvait en avoir un. Existe-t-il une monade qui ne peut pas en avoir ? Ou toutes les monades ont-elles un transformateur correspondant ?

Par un transformateur t correspondant à la monade m Je veux dire que t Identity est isomorphe à m . Et bien sûr qu'il satisfait aux lois du transformateur de monades et que t n est une monade pour toute monade n .

J'aimerais voir soit une preuve (idéalement constructive) que chaque monade en a une, soit un exemple d'une monade particulière qui n'en a pas (avec une preuve). Je suis intéressé par des réponses plus orientées vers Haskell, ainsi que par des réponses théoriques (de catégorie).

En guise de question complémentaire, existe-t-il une monade m qui a deux transformateurs distincts t1 y t2 ? C'est-à-dire, t1 Identity est isomorphe à t2 Identity et à m mais il existe une monade n tal que t1 n n'est pas isomorphe à t2 n .

( IO y ST ont une sémantique particulière, je ne les prends donc pas en compte ici et ignorons-les complètement. Concentrons-nous uniquement sur les monades "pures" qui peuvent être construites à l'aide de types de données).

Answer 1

Je suis avec @Rhymoid sur ce point, je crois que toutes les Monads ont deux ( !!) transformateurs. Ma construction est un peu différente, et beaucoup moins complète. J'aimerais être capable de transformer cette esquisse en une preuve, mais je pense qu'il me manque les compétences/intuition et/ou que cela pourrait être assez compliqué.

Grâce à Kleisli, toute monade ( m ) peut être décomposé en deux foncteurs F_k y G_k tal que F_k est l'adjoint gauche de G_k et que m est isomorphe à G_k * F_k (ici * est la composition d'un foncteur). Aussi, à cause de l'adjonction, F_k * G_k forme une comonade.

Je prétends que t_mk défini de telle sorte que t_mk n = G_k * n * F_k est un transformateur de monade. Clairement, t_mk Id = G_k * Id * F_k = G_k * F_k = m . Définition de return pour ce foncteur n'est pas difficile puisque F_k est un foncteur "pointu", et en définissant join devrait être possible puisque extract du comonad F_k * G_k peut être utilisé pour réduire les valeurs de type (t_mk n * t_mk n) a = (G_k * n * F_k * G_k * n * F_k) a à des valeurs de type G_k * n * n * F_k qui est ensuite réduit par join de n .

Nous devons être un peu plus prudents car F_k y G_k ne sont pas des endofoncteurs sur Hask. Ainsi, ils ne sont pas des instances de la norme Functor et ne sont pas directement composables avec la classe de type n comme indiqué ci-dessus. Au lieu de cela, nous devons "projeter" n dans la catégorie Kleisli avant la composition, mais je crois que return de m prévoit que la "projection".

Je crois que l'on peut aussi le faire avec la décomposition de la monade d'Eilenberg-Moore, ce qui donne m = G_em * F_em , tm_em n = G_em * n * F_em et des constructions similaires pour lift , return et join avec une dépendance similaire à l'égard de extract du comonad F_em * G_em .

Answer 2

Voici une réponse qui ressemble à un "je ne suis pas sûr".

Les monades peuvent être considérées comme l'interface des langages impératifs. return est la façon d'injecter une valeur pure dans le langage, et >>= c'est la façon dont on assemble les morceaux de la langue. Les lois sur les monades garantissent que le "remaniement" des morceaux du langage fonctionne comme prévu. Toutes les actions supplémentaires fournies par une monade peuvent être considérées comme ses "opérations".

Les transformateurs de monades sont une façon d'aborder le problème des "effets extensibles". Si nous avons un Transformateur de Monade t qui transforme une Monade m alors on peut dire que le langue m est en cours d'extension avec des opérations supplémentaires disponibles via t . Le site Identity monad est le langage sans effets/opérations, donc l'application de t a Identity vous obtiendrez juste un langage avec seulement les opérations fournies par t .

Ainsi, si nous pensons aux monades en termes de modèle "injection, épissage et autres opérations", nous pouvons simplement les reformuler à l'aide du Free Monad Transformer. Même la monade IO pourrait être transformée en un transformateur de cette façon. Le seul problème est que vous voudrez probablement trouver un moyen de retirer cette couche de la pile du transformateur à un moment donné, et la seule façon sensée de le faire est d'avoir IO au bas de la pile pour que vous puissiez simplement effectuer les opérations à cet endroit.

Answer 3

NOTE : il s'agit d'une non-réponse.

---

import Control.Applicative (Const (..))
import Control.Monad (join, liftM)
import Data.Functor.Identity

data Iso a b = Iso { rw :: a -> b, lw :: b -> a }

Pensez à Foo y Bar qui sont essentiellement la composition et la composition inversée :

newtype Foo m n a = Foo { unFoo :: m (n a) }
newtype Bar m n a = Bar { unBar :: n (m a) }

Pour tous les m , Foo m y Bar m sont tous deux des transformateurs correspondant à m .

fooIsTrans :: Monad m => Iso (Foo m Identity a) (m a)
fooIsTrans = Iso (liftM runIdentity . unFoo) (Foo . liftM Identity)

barIsTrans :: Monad m => Iso (Bar m Identity a) (m a)
barIsTrans = Iso (runIdentity . unBar) (Bar . Identity)

Pour certains m , Foo m (Const ()) y Bar m (Const ()) sont distincts.

fooValue :: Iso (Foo Maybe (Const ()) ()) Bool
fooValue = Iso
    (\x -> case x of { Just (Const ()) -> True; Nothing -> False })
    (\b -> case b of { True -> Just (Const ()); False -> Nothing })

barValue :: Iso (Bar Maybe (Const ()) ()) ()
barValue = Iso (getConst . unBar) (Bar . Const)

En supposant que ce qui précède est correct : sí toutes les monades ont un transformateur correspondant, et pas de il n'est pas nécessairement unique (sans tenir compte de la sémantique spéciale).

Answer 4

Auparavant, je pensais avoir trouvé des exemples de monades explicitement définies sans transformateur, mais ces exemples étaient incorrects.

Le transformateur pour Either a (z -> a) est m (Either a (z -> m a) , donde m est une monade étrangère arbitraire. Le transformateur pour (a -> n p) -> n a es (a -> t m p) -> t m a donde t m est le transformateur de la monade n .

1. La monade libre pointue.

Le constructeur de type monade L pour cet exemple est défini par

  type L z a  = Either a (z -> a)

L'intention de cette monade est d'embellir la monade ordinaire du lecteur. z -> a avec un pure valeur ( Left x ). La monade du lecteur ordinaire pure est une fonction constante pure x = _ -> x . Cependant, si l'on nous donne une valeur de type z -> a nous ne serons pas en mesure de déterminer si cette valeur est une fonction constante. Avec L z a le pure est représentée explicitement comme Left x . Les utilisateurs peuvent désormais effectuer une recherche par motif sur L z a et déterminer si une valeur monadique donnée est pure ou a un effet. En dehors de cela, la monade L z fait exactement la même chose que la monade de lecture.

L'instance de la monade :

  instance Monad (L z) where
     return x = Left x
     (Left x) >>= f = f x
     (Right q) >>= f = Right(join merged) where
        join :: (z -> z -> r) -> z -> r
        join f x = f x x -- the standard `join` for Reader monad
        merged :: z -> z -> r
        merged = merge . f . q -- `f . q` is the `fmap` of the Reader monad
        merge :: Either a (z -> a) -> z -> a 
        merge (Left x) _ = x
        merge (Right p) z = p z

Cette monade L z est un cas spécifique d'une construction plus générale, (Monad m) => Monad (L m) donde L m a = Either a (m a) . Cette construction embellit une monade donnée m en ajoutant un pure valeur ( Left x ), de sorte que les utilisateurs peuvent désormais effectuer une recherche de motif sur L m pour décider si la valeur est pure. Dans tous les autres cas, L m représente le même effet de calcul que la monade m .

L'instance de la monade pour L m est presque la même que pour l'exemple ci-dessus, sauf que le fichier join y fmap de la monade m doivent être utilisées, et la fonction d'aide merge est défini par

    merge :: Either a (m a) -> m a
    merge (Left x) = return @m x
    merge (Right p) = p

J'ai vérifié que les lois de la monade tiennent pour L m avec une monade arbitraire m .

Cette construction donne le foncteur pointu libre sur la monade donnée m . Cette construction garantit que le foncteur pointu libre sur un monade est également un monade.

Le transformateur pour la monade libre pointue est défini comme suit :

  type LT m n a = n (Either a (mT n a))

où mT est le transformateur de monade de la monade m (qui doit être connue).

2. Un autre exemple :

type S a = (a -> Bool) -> Maybe a

Cette monade est apparue dans le contexte des "monades de recherche". aquí . Le site papier de Jules Hedges mentionne également la monade de recherche, et plus généralement, les monades de "sélection" de la forme

 type Sq n q a = (a -> n q) -> n a

pour une monade donnée n et un type fixe q . La monade de recherche ci-dessus est un cas particulier de la monade de sélection avec n a = Maybe a y q = () . L'article de Hedges affirme (sans preuve, mais il l'a prouvé plus tard en utilisant Coq) que Sq est un transformateur de monade pour la monade (a -> q) -> a .

Cependant, la monade (a -> q) -> a a un autre transformateur de monade (m a -> q) -> m a du type "composé à l'extérieur". Ceci est lié à la propriété de " rigidité " explorée dans la question Cette propriété d'un foncteur est-elle plus forte que celle d'une monade ? A savoir , (a -> q) -> a est une monade rigide, et toutes les monades rigides ont des transformateurs de monade du type "composed-outside".

3. En général, les monades transformées ne possèdent pas elles-mêmes automatiquement un transformateur de monade. C'est-à-dire qu'une fois que nous prenons une monade étrangère m et appliquer un transformateur de monade t à celui-ci, nous obtenons une nouvelle monade t m et cette monade n'a pas de transformateur : étant donné une nouvelle monade étrangère n nous ne savons pas comment transformer n avec la monade t m . Si l'on connaît le transformateur mT pour la monade m on peut d'abord transformer n con mT et ensuite transformer le résultat avec t . Mais si nous n'avons pas de transformateur pour la monade m nous sommes bloqués : il n'y a pas de construction qui crée un transformateur pour la monade t m à partir de la connaissance de t seul et fonctionne pour les monades étrangères arbitraires m .

Cependant, en pratique, toutes les monades explicitement définies ont des transformateurs explicitement définis, de sorte que ce problème ne se pose pas.

4. La réponse de @JamesCandy suggère que pour toute monade (y compris IO ? !), on peut écrire une expression de type (générale mais compliquée) qui représente le transformateur de monade correspondant. En d'autres termes, vous devez d'abord coder votre type de monade à l'aide de Church, ce qui fait ressembler le type à une monade de continuation, puis définir son transformateur de monade comme pour la monade de continuation. Mais je pense que c'est incorrect - cela ne donne pas une recette pour produire un transformateur de monade en général.

Prendre l'encodage Church d'un type a signifie écrire le type

 type ca = forall r. (a -> r) -> r

Ce type ca est complètement isomorphe à a par le lemme de Yoneda. Jusqu'à présent, nous n'avons rien obtenu d'autre que de rendre le type beaucoup plus compliqué en introduisant un paramètre de type quantifié. forall r .

Encodons maintenant une monade de base par l'Église L :

 type CL a = forall r. (L a -> r) -> r

Encore une fois, nous n'avons rien obtenu jusqu'à présent, car CL a est entièrement équivalent à L a .

Maintenant, imaginez une seconde que CL a une monade de continuation (ce qu'elle n'est pas !), et écrire le transformateur de monade comme s'il s'agissait d'un transformateur de monade de continuation, en remplaçant le type de résultat r par le biais de m r :

 type TCL m a = forall r. (L a -> m r) -> m r

On prétend qu'il s'agit du "transformateur de monade codé par l'Eglise" pour L . Mais cela semble être incorrect. Nous devons vérifier les propriétés :

• TCL m est une monade légale pour toute monade étrangère m et pour toute monade de base L
• m a -> TCL m a est un morphisme monadique licite

La deuxième propriété est valable, mais je crois que la première ne l'est pas, - en d'autres termes, TCL m n'est pas une monade pour une monade arbitraire m . Peut-être que certaines monades m l'admettent, mais d'autres ne le font pas. Je n'ai pas été capable de trouver une instance générale de monade pour TCL m correspondant à une monade de base arbitraire L .

Une autre façon d'argumenter que TCL m n'est pas en général une monade est de noter que forall r. (a -> m r) -> m r est en effet une monade pour tout constructeur de type m . On désigne cette monade par CM . Maintenant, TCL m a = CM (L a) . Si TCL m était une monade, cela impliquerait que CM peut être composé avec n'importe quelle monade L et donne une monade légale CM (L a) . Cependant, il est très peu probable qu'une monade non triviale CM (en particulier, une qui n'est pas équivalente à Reader ) se composera avec toutes les monades L . Les monades ne se composent généralement pas sans contraintes supplémentaires strictes.

Un exemple spécifique où cela ne fonctionne pas est celui des monades de lecture. Considérons L a = r -> a y m a = s -> a donde r y s sont des types fixes. Maintenant, nous aimerions considérer le "transformateur de monades codées par l'Église". forall t. (L a -> m t) -> m t . Nous pouvons simplifier cette expression de type en utilisant le lemme de Yoneda,

 forall t. (x -> t) -> Q t  = Q x

(pour tout foncteur Q ) et on obtient

 forall t. (L a -> s -> t) -> s -> t
 = forall t. ((L a, s) -> t) -> s -> t
 = s -> (L a, s)
 = s -> (r -> a, s)

C'est donc l'expression de type pour TCL m a dans ce cas. Si TCL était un transformateur de monades, alors P a = s -> (r -> a, s) serait une monade. Mais on peut vérifier explicitement que cette P n'est en fait pas une monade (on ne peut pas implémenter return y bind qui satisfont aux lois).

Même si cela fonctionnait (c'est-à-dire en supposant que j'ai fait une erreur en prétendant que TCL m n'est en général pas une monade ), cette construction présente certains inconvénients :

• Il n'est pas functoriel (c'est-à-dire non covariant) par rapport à la monade étrangère m Nous ne pouvons donc pas interpréter une monade libre transformée en une autre monade, ni fusionner deux transformateurs de monades, comme expliqué ici. Existe-t-il un moyen fondé sur des principes de composer deux transformateurs de monade s'ils sont de type différent, mais que leur monade sous-jacente est du même type ?
• La présence d'un forall r rend le type assez compliqué à raisonner et peut entraîner une dégradation des performances (voir l'article "L'encodage Church considéré comme nuisible") et des débordements de pile (puisque l'encodage Church n'est généralement pas sûr pour la pile).
• Le transformateur de monade codé par Church pour une monade de base d'identité ( L = Id ) ne donne pas la monade étrangère non modifiée : T m a = forall r. (a -> m r) -> m r et ce n'est pas la même chose que m a . En fait, il est assez difficile de déterminer quelle est cette monade, étant donné une monade m .

Un exemple qui montre pourquoi forall r rend le raisonnement compliqué, considérons la monade étrangère m a = Maybe a et essayer de comprendre ce que le type forall r. (a -> Maybe r) -> Maybe r signifie en fait. Je n'ai pas été en mesure de simplifier ce type ou de trouver une bonne explication sur ce qu'il fait, c'est-à-dire quel type d'"effet" il représente (puisqu'il s'agit d'une monade, elle doit représenter un certain type d'"effet") et comment on pourrait utiliser un tel type.

• Le transformateur de monade codé par Church n'est pas équivalent aux transformateurs de monade standard bien connus tels que ReaderT , WriterT , EitherT , StateT et ainsi de suite.

Il n'est pas clair combien d'autres transformateurs de monades existent et dans quels cas on utiliserait un transformateur ou un autre.

5. L'une des questions du post est de trouver un exemple explicite d'une monade. m qui a deux transformateurs t1 y t2 de telle sorte que pour toute monade étrangère n les monades t1 n y t2 n ne sont pas équivalentes.

Je crois que le Search fournit un tel exemple.

 type Search a = (a -> p) -> a

où p est un type fixe.

Les transformateurs sont

 type SearchT1 n a = (a -> n p) -> n a
 type SearchT2 n a = (n a -> p) -> n a

J'ai vérifié que les deux SearchT1 n y SearchT2 n sont des monades licites pour toute monade n . Nous avons des ascenseurs n a -> SearchT1 n a y n a -> SearchT2 n a qui fonctionnent en retournant des fonctions constantes (il suffit de retourner n a tel que donné, en ignorant l'argument). Nous avons SearchT1 Identity y SearchT2 Identity évidemment équivalent à Search .

La grande différence entre SearchT1 y SearchT2 c'est que SearchT1 n'est pas functoriel dans n alors que SearchT2 est. Cela peut avoir des implications pour "l'exécution" ("l'interprétation") de la monade transformée, puisque normalement nous voudrions pouvoir lever un interpréteur n a -> n' a en un "coureur" SearchT n a -> SearchT n' a . Cela n'est possible qu'avec SearchT2 .

Une déficience similaire est présente dans les transformateurs de monades standard pour la monade de continuation et la monade de codensité : ils ne sont pas fonctoriels dans la monade étrangère.

Answer 5

Cette réponse est une ébauche de preuve pour une réponse positive aux deux questions. (L'isomorphisme n'est que partiellement prouvé, et la deuxième réponse doit être plus rigoureuse. Je ne suis pas non plus certain de ce qui suit r ou ma terminologie en général).

---

import Control.Monad.Trans.Cont
import Data.Functor.Identity

Pour toute monade donnée m il existe un certain r tal que ContT (m r) est un transformateur correspondant à la monade m . (Cette r est éventuellement fixé par l'exécution de la monade de continuation).

• Pour chaque a il existe un isomorphisme entre m r y ContT (m r) Identity r .
• ContT (m r) satisfait aux lois de transformation des monades (supposées de instance MonadTrans (ContT x) ).
• Pour chaque n , ContT (m r) n est une monade (supposée de instance Monad (ContT x m) ).

Nous pouvons prouver que ContT (m r) Identity r y m r sont isomorphes ; il suffit de montrer que les deux fonctions suivantes sont inverses l'une de l'autre :

up :: Monad m => m a -> ContT (m r) Identity a
up = \xs -> ContT (Identity . (xs >>=) . (runIdentity .))

down :: Monad m => ContT (m r) Identity r -> m r
down = runIdentity . ($ Identity . return) . runContT

Nous pouvons prouver que down . up = id :

down . up
 -- by definition of down and up
 = runIdentity . ($ Identity . return) . runContT . (\xs -> ContT (Identity . (xs >>=) . (runIdentity .)))
 -- by definition of composition, almost
 = runIdentity . ($ Identity . return) . runContT . ContT . (\xs -> Identity . (xs >>=) . (runIdentity .))
 -- newtypes
 = runIdentity . ($ Identity . return) . (\xs -> Identity . (xs >>=) . (runIdentity .))
 -- application after eta-abstraction
 = runIdentity . (\xs -> Identity . (xs >>=) . (runIdentity .) $ (Identity . return))
 -- application
 = runIdentity . (\xs -> Identity . (xs >>= runIdentity . Identity . return))
 -- newtypes
 = runIdentity . (\xs -> Identity $ (xs >>= return))
 -- monad: right-associativity
 = runIdentity . (\xs -> Identity xs)
 -- eta-reduction
 = runIdentity . Identity
 -- newtypes
 = id

(Il reste à prouver que up . down = id ; je reste bloqué, malheureusement, donc il y a peut-être quelque chose qui ne va pas).

Par conséquent, toutes les monades ont un transformateur correspondant .

---

Une preuve pour toutes les monades ont au moins deux transformateurs correspondants distincts pourrait être donné en utilisant une légère modification de ContT :

data SideT r m a = SideT (() -> m ()) ((a -> m r) -> m r)

Notez que le type () -> Identity () est isomorphe à () alors que () -> Maybe () est isomorphe à Bool (en ne considérant que les fonctions référentiellement transparentes et totales).

En tant que tel, ContT (m r) Identity y SideT (m r) Identity sont isomorphes, tandis que ContT (m r) Maybe y SideT (m r) Maybe ne le sont pas.