Je commence juste à lire sur la théorie des catégories, et j'apprécierais beaucoup que quelqu'un puisse expliquer le lien entre CS contravariance/covariance et la théorie des catégories. Quelles seraient certaines catégories d'exemples (c'est-à-dire quels sont leurs objets/morphismes?)? Merci d'avance?quelqu'un pourrait-il expliquer le lien entre type covariance/contravariance et théorie des catégories?
A foncteur contravariant de $ C $ à $ D $ est exactement la même chose comme normale (ie covariant) fonctor de $ C $ à $ D^{op} $, où $ D^{op} $ est le opposite category de $ D $. Il est donc probablement préférable de comprendre d'abord les catégories opposées - alors vous comprendrez automatiquement les foncteurs contravariants!
foncteurs contravariants ne viennent pas si souvent que ça dans CS, bien que je peux penser à deux exceptions:
Vous avez peut-être entendu parler de contravariance dans le contexte de sous-typage. Bien que ce soit techniquement le même terme, la connexion est vraiment, vraiment faible. En programmation orientée objet, les classes forment un ordre partiel; chaque ordre partiel est une catégorie avec des "homonymes binaires" - étant donné deux objets quelconques $ A $ et $ B $, il y a exactement un morphisme $ A \ à B $ iff $ A \ leq B $ (notez la direction; cette orientation légèrement confuse est la norme pour des raisons que je ne vais pas expliquer ici) et aucun morphisme autrement. Les types paramétrés comme, disons, la fonction partielle de Scala [-A, Unit] sont des foncteurs de cette catégorie simple à elle-même ... nous nous concentrons généralement sur ce qu'ils font aux objets: donné une classe X, PartialFunction [X, Unit] est aussi une classe. Mais les foncteurs conservent aussi les morphismes; dans ce cas si nous avions une sous-classe Chien d'Animal, nous aurions un morphisme Dog $ \ à $ Animal, et le foncteur préserverait ce morphisme, nous donnant un morphisme PartialFunction [Animal, Unit] $ \ to $ PartialFunction [Chien, Unit], nous indiquant que PartialFunction [Animal, Unit] est une sous-classe de PartialFunction [Dog, Unit]. Si vous pensez à cela, cela a du sens: supposons que vous ayez besoin d'une fonction qui fonctionne sur les chiens. Une fonction qui fonctionne sur tous les animaux fonctionnerait certainement là! Cela dit, l'utilisation de la théorie des catégories complètes pour parler des ensembles partiellement ordonnés est une surenchère à grande échelle. Moins commun, mais utilise en fait la théorie des catégories: considérons la catégorie Types (Hask) dont les objets sont les types du langage de programmation Haskell et où un morphisme $ \ tau_1 \ to \ tau_2 $ est une fonction du type $ \ tau_1 $ -> $ \ tau_2 $. Il y a aussi une catégorie Jugements (Hask) dont les objets sont des listes de jugements de typage $ \ tau_1 \ vdash \ tau_2 $ et dont les morphismes sont des preuves de tous les jugements d'une liste en utilisant les jugements de l'autre liste comme hypothèses. Il y a un foncteur de types (HASK) à Jugements (HASK) qui prend les types (Hask) -morphism $ f: A \ à B $ à la preuve
B |- Int
----------
......
----------
A |- Int
qui est un $ morphisme (B \ vdash Int) \ (A \ vdash Int) $ - remarquez le changement de direction.Fondamentalement, ce que cela signifie est que si vous avez une fonction qui transforme A en B'a, et une expression de type Int avec une variable libre x de type B, alors vous pouvez l'envelopper avec "let x = fy in. .. "et arriver à une expression encore de type Int mais dont la seule variable libre est de type $ A $, pas $ B $.
Il existe de très belles vidéos sur la contravariance/covariance dans Going deep channel in Microsoft Channel9. Vous pouvez commencer ici:
Très très bien en effet. Merci d'avoir partagé. J'espère qu'ils arriveront avec 4 de N un jour! :) –