Sous-typage entre objets

Soit t le type d'un objet: $t = <m_1:\tau_1; m_2: \tau_2; ... m_n: \tau_n>$. Nous notons la relation `` t' est un sous-type de t'' par: $t' \preceq t$. Dans cette partie nous étudions la forme que doit avoir tout type t' sous-type de t.

D'après la défition du sous-typage, si t' est sous-type de t, alors tout objet de type t' peut prendre la place d'un objet de type t sans occasionner d'erreur de typage. Cela veut dire, en particulier, que si nous supposons:

• o : t

• o' : t',

• et $m_i : \tau_i$ est une méthode de t, alors

• si o#mi est un envoi de message bien typé dans un certain contexte, alors

• o'#mi doit être bien typé dans le même contexte.

Par conséquent, t' doit être tel que:

• t' doit avoir au moins toutes les méthodes de t, mais peut éventuellement en avoir plus,
• les types des méthodes communes sont en relation de sous-typage: si $m_i : \tau_i'$ dans t' et $m_i : \tau_i$ dans t, alors $\tau'_i \preceq\tau_i$.

Exemple 1:

Soient p:point et cp:colorpoint. Le code p#getx = 0 est bien typé. Pour que le code

(cp : colorpoint :> point)#getx = 0

soit bien typé, colorpoint doit posséder la méthode getx avec un type qui doit être sous-type du type de la même méthode dans point. Comme getx a le même type dans les deux classes, et comme un type est toujours sous-type de lui-même, on peut conclure que colorpoint est sous-type de point.

Exemple 2:

Considérons la classe des cercles dont le centre est définit par une instance polymorphe des points. Nous commencons par rappeler les classes des points et des points colorés:

class point init =
 object
   val mutable x = init
   method getx = x
   method move d = x<-x+d
   method print = print_int x
end;;

class colorpoint x cinit  =
 object
   inherit point x as super
   val mutable c = cinit 
   method color = c
   method setcolor c' = c<-c'
   method print = print_string "("; 
                  super#print; print_string (" , "^c);
                  print_string ")"
end;;

let p1 = new point 1;;

let cp1 = new colorpoint 1 "Rouge";;

La classe circle place son centre par rapport à un point, et la classe colorcircle par rapport à un point coloré:

# class ['a] circle (c : 'a) =
   object 
     constraint 'a = #point
     val mutable center = c
     method center = center
     method move = center#move
   end;;

class ['a] circle :
  'a ->
  object
    constraint 'a = #point
    val mutable center : 'a
    method center : 'a
    method move : int -> unit
  end

# class ['a] colorcircle c =
  object
     constraint 'a = #colorpoint
     inherit ['a] circle c
     method color = center#color
  end;;

class ['a] colorcircle :
  'a ->
  object
    constraint 'a = #colorpoint
    val mutable center : 'a
    method center : 'a
    method color : string
    method move : int -> unit
  end


(* Un cercle centre sur un point *)

# let cirp = new circle p1;;
val cirp : point circle = <obj>

(* Un cercle centre sur un point colore *)

# let circp = new colorcircle  cp1;;
val circp : colorpoint colorcircle = <obj>

# circp#color;;
- : string = "Rouge"

Le typage réussi de la fonction erase_color montre que colorpoint colorcircle est un sous-type de point circle.

# let erase_color c  = (c : colorpoint colorcircle :> point circle);;
val erase_color : colorpoint colorcircle -> point circle = <fun>

(* En effet *)

# let coerced_ccircle = erase_color circp;;
val coerced_ccircle : point circle = <obj>

#  coerced_ccircle#color;;
This expression has type point circle
It has no method color

De manière générale, la relation entre t et t' est formalisée par la règle de typage suivante:

Règle (Sous-typage entre objets):

Soient

• $t = <m_1: \tau_1; \ldots; m_n: \tau_n>$
• $t' = <m_1: \tau'_1; \ldots; m_n: \tau'_n; \rho>$ où $\rho$ est une suite de méthodes

t' est un sous-type de t (noté $t' \preceq t$)

si $\tau'_i \preceq\tau_i$ pour tout i dans [1..n].

En Ocaml (et dans la plupart des langages avec sous-typage), l'ordre des méthodes n'a pas d'importance dans la comparaison de deux types d'objets. Pour simplifier l'exposé, notre règle est moins générale: elle n'admet pas de permutations dans l'ordre des méthodes.