Appel de fonctions avec sous-typage

Un des interêts du polymorphisme est de pouvoir utiliser les fonctions avec différents types d'arguments. Sous quelles conditions un appel de fonction est bien typé en présence du polymorphisme d'inclusion? La fonction qui teste si un point est à l'origine dans un plan, prend en argument un point mais peut recevoir un point coloré (vu comme un point). Le type de l'argument effectif peut être sous-type de celui l'argument formel. La règle de typage associée est:

Règle (Appel de fonction avec $\preceq$):

Si

• $f : \sigma \rightarrow\tau$
• $a : \sigma'$
• $\sigma' \preceq\sigma$

alors $(f \ a)$ est bien typé et a le type $\tau$

Justifions cette règle. Si $\sigma'$ est un sous-type de $\sigma$ alors toutes les opérations définies sur $\sigma$ sont aussi définies sur $\sigma'$. Ainsi, f qui attend un argument de type $\sigma$ peut en recevoir un de type $\sigma'$: on pourra appliquer en toute sécurité à celui-ci, toute opération définie sur l'argument attendu.