La composition de deux foncteurs est un foncteur

Question

Sur une réponse précédente Petr Pudlak a défini le CFunctor pour les foncteurs autres que ceux de la classe Hask a Hask . En le réécrivant un peu à l'aide de familles de types, on obtient les résultats suivants

class CFunctor f where
  type Dom f :: * -> * -> *               -- domain category
  type Cod f :: * -> * -> *               -- codomain category
  cmap :: Dom f a b -> Cod f (f a) (f b)  -- map morphisms across categories

avec des instances qui ressemblent par exemple à

instance CFunctor Maybe where
  type Dom Maybe = (->)                   -- domain is Hask
  type Cod Maybe = (->)                   -- codomain is also Hask 
  cmap f = \m -> case m of
                   Nothing -> Nothing
                   Just x  -> Just (f x)

Dans la théorie des catégories, chaque fois que F : C --> D est un foncteur et G : D --> E est un foncteur, alors la composition GF : C --> E est également un foncteur.

J'aimerais exprimer cela en Haskell. Comme je ne peux pas écrire instance CFunctor (f . g) J'introduis une classe d'enveloppe :

newtype Wrap g f a = Wrap { unWrap :: g (f a) }

En écrivant le CFunctor Si j'arrive jusqu'à

instance (CFunctor f, CFunctor g, Cod f ~ Dom g) => CFunctor (Wrap g f) where
  type Dom (Wrap g f) = Dom f
  type Cod (Wrap g f) = Cod g
  cmap = undefined

mais je n'arrive pas à comprendre ce que l'implémentation de la cmap devrait être. Des conseils ?

PS la raison éventuelle de tout ceci est d'introduire aussi une classe Adjunction avec des méthodes unit y counit puis de dériver automatiquement des instances de monades à partir d'adjonctions. Mais d'abord, je dois montrer au compilateur que la composition de deux foncteurs est aussi un foncteur.

Je suis conscient que je pourrais utiliser cmap.cmap sur un objet de type g (f a) et cela fonctionnerait, mais cela ressemble un peu à de la triche - un foncteur est sûrement juste un foncteur, et le compilateur ne devrait pas avoir à savoir qu'il est en fait la composition de deux autres foncteurs ?

Answer 1

Foncteurs donnés F : C → D y G : D → E , une composition de foncteur G ∘ F : C → E est un mappage d'objets entre les catégories C y E de telle sorte que (G ∘ F)(X) = G(F(X)) et une correspondance entre les morphismes telle que (G ∘ F)(f) = G(F(f)) .

Cela suggère que votre CFunctor doit être définie comme suit :

instance (CFunctor f, CFunctor g, Cod f ~ Dom g) => CFunctor (Wrap g f) where
  type Dom (Wrap g f) = Dom f
  type Cod (Wrap g f) = Cod g
  cmap f = cmap (cmap f)

Cependant, la composition cmap Dom f a b -> Cod g (g (f a)) (g (f b)) y cmap dans ces instances a un type Dom f a b -> Cod g (Wrap g f a) (Wrap g f b) .

Nous pouvons obtenir de g (f a) a Wrap g f et vice versa, mais comme la déclaration d'instance ne fait aucune hypothèse sur la structure de la classe Cod g nous n'avons pas de chance.

Puisque nous savons que le foncteur est un mappage entre catégories, nous pouvons utiliser le fait que Cod g est un Category (du côté de Haskell, cela nécessite un fichier Category (Cod g) ), cela nous donne peu d'opérations avec lesquelles travailler :

cmap f = lift? unWrap >>> cmap (cmap f) >>> lift? Wrap

Cela nécessite toutefois un opérateur de levage pratique lift? qui lève une fonction de Hask à la catégorie Cod g catégorie. Rédaction Cod g como (~>) le type de lift? doit être :

lift? :: (a -> b) -> (a ~> b)

lift? unWrap  :: Wrap g f a ~> g (f a)
cmap (cmap f) :: g (f a)    ~> g (f b)
lift? Wrap    :: g (f b)    ~> Wrap g f b

lift? unWrap >>> cmap (cmap f) >>> lift? Wrap :: Wrap g f a ~> Wrap g f b

Maintenant, il y a au moins deux choix pour cet opérateur de levage :

• Vous pourriez étendre le constrait de Category (Cod g) a Arrow (Cod g) dans ce cas, l'opérateur de levage devient arr ,
• ou, comme le mentionne Sjoerd Visscher dans les commentaires, vous pourriez utiliser le fait que Wrap y unWrap sont sémantiquement id au moment de l'exécution, auquel cas l'utilisation de l'option unsafeCoerce est justifiée.