Variance (informatique)

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].