Introduction aux actégories

Les actégories jouent un rôle central dans les optics, notamment les lenses, prisms et traversals. Pour comprendre les actégories, il est essentiel de commencer par la définition d'une catégorie monoidale.

catégorie monoidale

Une catégorie monoidale est une catégorie équipée d'un produit tensoriel, noté ten. Ce produit est un foncteur qui doit être associatif et unitaire, à isomorphisme près. Cela signifie qu'il existe un associateur inversible : alpha :: (a `ten` b) `ten` c -> a `ten` (b `ten` c). De plus, il y a un objet unité et deux unités inversibles : lambda :: (Unit ten) `ten` a -> a et lambda' :: a -> (Unit ten) `ten` a.

modélisation en Haskell

Pour modéliser une catégorie monoidale en Haskell, on peut définir une classe MonoidalCategory qui prend en compte le type du produit tensoriel ten et la contrainte obj sur les objets de la catégorie. La classe MonoidalCategory doit être une instance de Bifunctor pour ten. On peut également définir l'unité de la catégorie monoidale comme un type associé Unit ten.

class (Bifunctor ten) => MonoidalCategory ten where
   type Unit ten :: Type
   alpha :: (a `ten` b) `ten` c -> a `ten` (b `ten` c)
   lambda :: (Unit ten) `ten` a -> a
   lambda' :: a -> (Unit ten) `ten` a

actégories

Une actégorie est une catégorie qui supporte l'action d'une catégorie monoidale. L'action peut être définie comme un foncteur du produit des catégories vers la catégorie d'endofoncteurs. Les conditions de cohérence sont des transformations naturelles inversibles qui relient l'action au produit tensoriel et à son unité.

class (MonoidalCategory obj ten, Bifunctor act) => Actegory obj ten act | act -> ten where
   assoc :: (m `ten` n) `act` a -> m `act` (n `act` a)
   assoc' :: m `act` (n `act` a) -> (m `ten` n) `act` a
   unit :: Unit ten `act` a -> a
   unit' :: a -> Unit ten `act` a

Les actégories qui utilisent la même catégorie monoidale pour leurs actions forment une catégorie, avec des foncteurs monoidaux stricts comme morphismes. Ces foncteurs peuvent être modélisés en Haskell comme des instances de la classe MonFunctor.

class (Actegory obj ten act1, Actegory obj ten act2, Functor f) => MonFunctor obj ten act1 act2 f where
   as :: m `act2` f a -> f (m `act1` a)
   as' :: f (m `act1` a) -> m `act2` f a