Sous-typage entre fonctions

Soient b et a deux classes telles que $b \preceq a$. La règle de typage entre objets impose que les types des méthodes de b soient des sous-types de celles dans a. Lorsque leurs types sont atomiques (par exemple compte, compteremunere, etc.), il est facile de les comparer par sous-typage: si f dans b est de type compteremunere et dans a elle a le type compte, nous pouvons facilement chercher à établir $type({\tt f}_b) \preceq type({\tt f}_a)$ (où $type({\tt f}_a)$ désigne le type de f dans la classe a), c.a.d., ${\tt comptermeunere} \preceq {\tt compte}$.

En revanche, que se passe-t-il si les méthodes à comparer sont des fonctions? Comment savoir si deux types de fonctions sont en relation de sous-typage? Posons le cas suivant:

class a =
 ...
 method f: t -> q
 ...
end

class b =
 ...
 method f: m -> n
end

Pour établir ${\tt b} \preceq {\tt a}$ il faut vérifier $type({\tt f}_b) \preceq type({\tt f}_a)$, c.a.d., $(m \rightarrow n) \preceq(t \rightarrow q)$. Quand est-ce que ces deux types fonctionnels sont en relation de sous-typage?

Règle (Sous-typage entre fonctions):
Deux types fonctionnels, ( $m \rightarrow n$) et ( $t\rightarrow q$) sont en relation de sous-typage:

$$(m \rightarrow n) \preceq(t \rightarrow q)$$

ssi

• $t \preceq m$ et
• $n \preceq q$.

Justifions cette règle. Nous supposons que les types fonctionnels $(m \rightarrow n)$ et $(t \rightarrow q)$ sont les types de la méthode f des classes b et a plus haut. Pour distinguer les deux méthodes nous les appelons f_a et f_b:

$$\begin{array}{l} f_a : (t \rightarrow q)\\ f_b : (m \rightarrow n) \end{array}$$

Nous faisons également les hypothèses suivantes:

• $b \preceq a$,
• il existe une fonction autre qui prend un argument r : q (voir sa définition plus bas),
• il existe une fonction h (voir définition plus bas) qui envoie le message f à un objet o de type a. Lors de cet envoi, elle fournit un argument x:t à f, alors que cette méthode dans a attend prcisement un argument de type t.

let autre (r: q) = ....
let h(o: a, x: t) = autre(o#f(x));;

D'après ces hypothèses et définitions nous constatons:

• le code o#f(x) est bien typé. En effet, puisque o:a, cet objet possède bien une méthode f, dont l'argument attendu est de type t. Le type déclaré pour x est précisement t,

• le code autre(o#f(x)) est aussi bien typé, car le type résultat de f dans a est q, et que celui-ci est le type attendu pour l'argument de autre.
• ces hypothèses ne retirent rien à la généralité de notre exemple.

Justifions maintenant la règle de typage:

1.

(Justification de $t \preceq m$): Par hypotèse $b \preceq a$, on peut appliquer la fonction h à un objet (o_b : b). L'appel se transforme en

$$h(o_b,x) \Rightarrow {\tt autre}(o_b\char93 f_b(x))$$

dans cet appel, quel est le type de x? Il est déclaré de même type (t) que les arguments de f_a, mais il doit pouvoir être vu comme ayant le type de l'argument de f_b ( c.a.d., comme ayant le type m), donc

$$(type\_argument(f_a) = type(x) = t) \preceq type\_argument(f_b) \Rightarrow t \preceq m$$

Notons que la relation inverse $m \preceq t$ est impossible: f_b ne pourrait pas recevoir un argument de type t. Un appel

$$h(o_b,r) \Rightarrow {\tt autre}(o_b\char93 f_b(r)) \hspace{2mm} \mbox{o\\lq u } \hspace{2mm} r : t$$

serait alors incorrecte.

2.

(Justification de $n \preceq q$): la fonction autre attend un argument de même type ou plus petit que celui résultat d'un appel à f_a. Mais, son argument peut-être du type du résultat de f_b, donc:

$$type\_res(f_b) \preceq type\_res(f_a) \Rightarrow n \preceq q$$

ainsi, les deux appels autre(p) et autre(w) sont correctes, pour p:n et w:q.

On dit que la règle de sous-typage entre fonctions et co-variante pour les types résultat (le type résultat du plus petit des deux types est plus petit (va dans le même sens) que le type résultat du plus grand des deux), alors qu'elle est contre-variante pour les types argument (elle change de sens).