Un exemple en dehors d'Ocaml

L'exemple présenté ici est immaginaire. Pour les besoins de l'exposé, nous utilisons la syntaxe Ocaml, mais nous supposons que le typage se fait avec les règles de sous-typage plutôt qu'avec du polymorphisme paramétrique. Ainsi, la défintion de méthode

    method manger (x: aliments) = ...

est interprété ici comme une contrainte de type qui autorise l'argument à être un sous-type de aliments, comme c'est le cas dans les langages objets avec polymorphisme d'inclusion. Cet exemple ne peut pas être écrit en Ocaml!

Nous supposons définies les classes aliments, viande, et legumes, qui satisfont:

$$\begin{array}{lcr} {\tt viande} & \preceq & {\tt aliments} \\ {\tt legumes} & \preceq & {\tt aliments} \\ \end{array}$$

Par ailleurs, nous définissons deux classes

class personne =
 object
    ...
    method manger (x: aliments) = ...
end
 
class vegetarien =
 object
   inherit personne 
   method manger (x: legumes) = ...
end

où nous supposons que la méthode manger ne fait que modifier l'état interne, donc elle renvoie unit. La classe vegetarien est une sous-classe de la classe personne. Est-elle un sous-type de personne? Autrement dit, la relation

$$vegetarien \; \preceq \; personne \hspace{2cm} (1)$$

est-elle vraie? Considérons maintenant la fonction

let chez_MacDo (p:personne) = p#manger(BigMac) où Bigmac:viande

Si (1) est vrai, on peut utiliser à la place de p un objet de type vegetarien, par exemple, Gandhi:vegetarien et avoir:

$${\tt chez\_MacDo (Gandhi)} \Longrightarrow {\tt Gandhi\char93 manger(BigMac)}$$

Or, cet appel est sémantiquement incorrect: on fait manger de la viande à un végétarien; et de plus il est mal typé: la méthode manger d'un végétarien n'accepte pas de viande!

En réalité, la relation (1) n'est pas vérifiée car le type de la méthode manger des végétariens (que nous notons ${\tt manger}_v$) n'est pas un sous-type du type de manger des personnes:

$$Type({\tt manger}_v) \; \not \preceq \; Type({\tt manger}_p) ... ...\quad \Rightarrow \quad \quad vegetarien \not \preceq personne$$

La méthode manger des végétariens ne peut pas être utilisée à la place de la méthode manger des personnes. Il n'est pas sûr de considérer que leurs types sont en relation de sous-typage. Cela entraîne que, bien que vegetarien soit une sous-classe de personne, vegetarien n'est pas sous-type de personne.