Cet article est une ébauche concernant l’informatique et les mathématiques.

Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.

En théorie des langages de programmation, la variance d'un type constructeur indique comment celui-ci transforme les relations d'héritage entre les types^[1].

Dans une théorie des types munie de constructeur de type, soit T et S deux types, et C[A] un type constructeur d'argument A. C[.] est soit^[2],[3] :

• covariant : Si S est un sous-type de T alors C[S] est un sous-type de C[T]
• contravariant : Si S est un sous-type de T alors C[T] est un sous-type de C[S]
• invariant : Quelle que soit la relation d'héritage entre T et S, C[T] n'est pas un sous-type de C[S] et C[S] n'est pas un sous-type de C[T].
• bivariant : Quelle que soit la relation d'héritage entre T et S, C[S] est un sous-type de C[T].
• variant : C[.] est covariant, contravariant ou bivariant.

On définit une catégorie ${\displaystyle {\mathcal {C}}}$ dont les objets sont les types et les morphismes sont les relations d'héritage entre les types^[1].

${\displaystyle {\mathcal {C}}}$ est bien une catégorie : tout type est son propre sous-type, donc il existe un morphisme identité associé à chaque objet. De plus, l'associativité est assurée car il existe au plus un morphisme entre deux objets^[1].

Les foncteurs dans ${\displaystyle Fun({\mathcal {C}},{\mathcal {C}})}$ correspondent alors aux types constructeurs, le vocabulaire foncteur covariant et contravariant explique que ce vocabulaire s'applique aux types constructeurs^[1].

• Portail de la programmation informatique