Re: Reason

Si tu acceptes de m'aider (et probablement en aider d'autres) à mieux comprendre ton exposé, je t'en remercie d'avance.

Effectivement, je me rends compte que ce que j'ai écrit doit paraître abscons pour qui n'est pas habitué à ce genre de questions. Je veux bien essayer de clarifier la chose en étant plus didactique, et compléter ainsi la réponse de Def.

On va partir de la logique et de sa notion de concept, la POO cherchant à procéder à une classification des concepts en genres et espèces comme les biologistes le font pour le règne animal.

Toutes les connaissances c'est-à-dire toutes les représentations rapportées consciemment à un objet sont ou bien des intuitions, ou bien des concepts. L'intuition est une représentation singulière, le concept est une représentation générale ou réfléchie.

La connaissance par concept s'appelle la pensée.

Remarques. 1) Le concept est opposé à l'intuition, car c'est une représentation générale ou une représentation de ce qui est commun à plusieurs objets, donc une représentation en tant qu'elle peut être contenue en différents objets.

Kant, Logique.

On peut voir les types comme signifiant des concepts et les termes d'un langage comme des choses rentrant sous un concept. Par exemple, avec le concept de « verre » on peut dire, en en montrant un, « ceci est un verre ». Dans une telle situation, les logiciens disent que l'on subsume la perception que l'on a (l'intuition) sous le concept de « verrre ». Il en est de même lorsque l'on dit que Socrate est un homme. En théorie des types, un tel jugement est appelé un jugement de typage et on l'écrirait Socrate : homme. Comme dans l'exemple suivant :

let i = 1;;
val i : int = 1

Je définit une variable i, et la boucle REPL OCaml me répond : la valeur i est un int.

Jusque là, c'est ce que tu avais bien compris de la notation t : T. Ensuite dans le pensée, nous hiérarchisons nos concepts en genre et espèce : les hommes sont des mammifères, les mammifères sont des animaux, les animaux sont des êtres vivants...

Les concepts sont dits supérieurs s'ils ont sous eux d'autres concepts, qui par rapport à eux sont dit concepts inférieurs.

Remarque. Les concepts n'étant appelé supérieurs et inférieurs que de façon relative, un seul et même concept peut donc, sous différents rapports, être en même temps supérieur et inférieur.

Le concept supérieur dans son rapport avec son concept inférieur s'appelle genre; le concept inférieur dans son rapport à son concept supérieur s'appelle espèce.

Tout comme les concepts inférieurs et supérieurs, ceux de genre et d'espèce se distinguent dans la subordination logique non par leur nature, mais par leur rapport respectif.

Kant, ibid.

Ainsi, par exemple, un triangle est une espèce de polygone et le concept de polygone constitue le genre dans le rapport de subordination logique entres les deux concepts.

Je pense (du moins je l'espère) que ce que je viens d'exposer doit être facilement compréhensible. Les langages orientés objets prétendent, via leur système de classe et d'héritage, réaliser une telle hiérarchie des concepts en genre et espèce. Sauf que, dans les faits, c'est logiquement faux dans la plupart des langages donc faux.

Ce rapport respectif entre concepts, le rapport entre genre et espèce, est justement ce que l'on appelle la relation de sous-typage que l'on note S <: T pour dire que S est un sous-type de T. En revanche, une sous-classe (si l'on entend par là une classe qui hérite d'une autre) n'est pas nécessairement un sous-type. Comme l'a dit Def dans sa réponse, l'héritage c'est proche d'un simple #include, ça évite le copier-coller : c'est pour cela que je parlais de notion syntaxique.

Venons-en maintenant aux règles qui déterminent la relation de sous-typage. Les deux premières que j'ai données sont issues de la syllogistique aristotélicienne : la première figure. Leur notation est empruntée à la formulation par Gentzen du calcul des séquents. On y sépare verticalement les prémisses et la conclusion de la règle de déduction. Ainsi la règle :

S <: U U <: T
---------------
 S <: T

se lit : sous les prémisses que S est un sous-type de U et que U est un sous-type de T, on conclue que S est un sous-type de T. C'est la figure Barbara des syllogismes aristotéliciens.

Pour la première règle, dans la prémisse Gamma |- t : S, le signe |- (qui est un T couché) se lit « thèse de ». Il signifie que, dans le contexte des hypothèses que constitue Gamma, on peut prouver la thèse t : S (que le terme t est de type S). D'un point de vue programmation, on peut voir Gamma comme un contexte, une portée lexicale (scope). Ainsi dans l'exemple suivant :

let i = 1;;
val i : int = 1
let j =
 let i = 2. in
 i +. 3.;;
val j : float = 5.

Dans le contexte global, la REPL infère que i : int. En revanche, dans le contexte de définition de j, elle inférera que i : float. Ainsi la règle :

Gamma |- t : S S <: T
-----------------------
 Gamma |- t : T

peut se lire : dans un contexte où on peut prouver que le terme t est de type S et que S est un sous-type de T, on peut alors prouver, dans le même contexte, que t est de type T.

Voyons un peu maintenant ce qui se passe avec des objets (au sens du paradigme orienté objet), l'héritage et la relation de sous-typage. Les objets peuvent être vus comme des enregistrement extensibles (extension obtenue via l'héritage).

Prenons par exemple ces deux types OCaml :

type pt2d = { x : float; y : float };;
type pt3d = { x : float; y : float; z : float };;
let p = {x = 1.; y = 3.};;
val p : pt2d = {x = 1.; y = 3.}
let p' = {x = 1.; y = 3.; z = 4.};;
val p' : pt3d = {x = 1.; y = 3.; z = 4.}

Bien que le type des pt3d contiennent les champs x et y, on ne peut pas, en OCaml, utiliser p' là où le système attend un objet de type pt2d.

let move dx (p : pt2d ) = {p with x = p.x +. dx};;
val move : float -> pt2d -> pt2d = <fun>
move 0.1 (p' :> pt2d);;
Error: Type pt3d is not a subtype of pt2d

Les enregistrements OCaml ne possèdent pas cette relation de sous-typage <:. Pour cela, il faut passer par les enregistrements extensibles que sont les objets.

let op = object method x = 1. method y = 3. end;;
val op : < x : float; y : float > = <obj>
let op' = object method x = 1. method y = 3. method z = 4. end;;
val op' : < x : float; y : float; z : float > = <obj>
type obj_pt2D = <x : float; y : float>;;
let move dx (p : obj_pt2D) : obj_pt2D = object method x = p#x +.dx method y = p#y end;;
val move : float -> obj_pt2D -> obj_pt2D = <fun>
move 0.1 op;;
- : obj_pt2D = <obj>
move 0.1 (op' :> obj_pt2D);;
- : obj_pt2D = <obj>

On peut noter au passage que la coercition entre types doit être explicite (il n'y a pas de cast implicite en OCaml) et qu'elle est notée comme la « symétrique » de la relation de sous-typage : :>.

Les règles qui dictent la relation de sous-typages entre enregistrements sont données dans la section records du chapitre de l'ouvrage de Benjamin C. Pierce. En gros, pour être un sous-type, il faut avoir au moins les mêmes champs (ici x et y) et que les types de ces champs soient des sous-types des champs correspondant (ici ce sont les même, à savoir float).

C'est ici qu'il peut y avoir des soucis entre héritage et sous-typage. Pour l'instant nos méthodes n'étaient pas des fonctions. Lorsque l'on a une classe qui possèdent des fonctions comme méthodes, au moment de l'héritage il faut contrôler le sous-typage entre ces fonctions. D'où la règle de sous-typage entre fonctions et les problématiques de contravariance et de convariance.

Commençons avec deux classes simples à la mode fonctionnel : des points à une ou deux dimensions avec des méthodes pour les déplacer.

class point x_init = object
val x = x_init
method get_x = x
method move_x dx = {< x = x +. dx >}
end;;
class point : 
 float ->
 object('a)
 val x : float
 method get_x : float
 method move_x : float -> 'a
 end
class point2d x_init y_init = object
inherit point x_init
val y = y_init
method get_y = y
method move_y dy = {< y = y +. dy >}
end;;
class point2d : 
 float ->
 float ->
 object ('a)
 val x : float
 val y : float
 method get_x : float
 method get_y : float
 method move_x : float -> 'a
 method move_y : float -> 'a
 end

Ici les méthodes move_x (ou move_y) font référence au types de l'objet ('a) : elle retourne un objet de même type que l'objet sur lesquelles on les utilise. Comme ce type apparaît en position covariante (sortie), l'héritage est aussi un sous-typage.

let move_x dx (p : point) = p#move_x dx;;
val move_x : float -> point -> point = <fun>
let op = new point 1.;;
val op : point = <obj>
let op' = new point2d 1. 2.;;
val op' : point2d = <obj>
move_x 0.1 op;;
- : point = <obj>
move_x 0.1 (op' :> point);;
- : point = <obj>

Maintenant, au lieu de considérer des points, considérons des vecteurs à une ou deux dimensions disposant d'une méthode pour les ajouter entre eux (opérateur binaire).

class virtual vect = object ( _ : 'a)
method virtual get_x : float
method virtual add : 'a -> 'a
end;;
class virtual vect :
 object('a)
 method virtual add : 'a -> 'a 
 method virtual get_x : float
 end

Ici la méthode add n'ont seulement renvoie un objet du type de la classe (position covariante) mais en prend également un en entrée (position contravariante). Ici l'héritage ne sera pas identique au sous-typage.

class vect1d x_init = object
inherit vect
val x = x_init
method get_x = x
method add v = {< x = x +. v#get_x >}
end;;
class vect1d :
 float -> 
 object ('a)
 val x : float
 method add : 'a -> 'a
 method get_x : float
 end
class vect2d x_init y_init = object
inherit vect1d x_init
val y = y_init
method get_y = y
method add v = {< x = x +. v#get_x ; y = y +. v#get_y >}
end;;
class vect2d : 
 float -> 
 float ->
 object ('a)
 val x : float
 val y : float
 method add : 'a -> 'a
 method get_x : float
 method get_y : float
 end
((new vect2d 1. 2.) :> vect1d);;
Error:
 Type vect2d = < add : vect2d -> vect2d; get_x : float;
 get_y : float > is not a subtype of
 vect1d = < add : vect1d -> vect1d; get_x : float >
 Type vect1d = < add : vect1d -> vect1d; get_x : float > is
 not a subtype of vect2d = < add : vect2d -> vect2d; get_x : float; get_y : float >

Pour que le type vect2d soit un sous-type du type vect1d, il faudrait que sa méthode add : vect2d -> vect2d soit un sous-type de la méthode add : vect1d -> vect1d du type vect1d. Ce qui, d'après la règle de sous-typage des fonctions, nécessiterait que vect2d soit à la fois un sous-type et un sur-type de vetc1d, ce qui est impossible.

Pour rappel, la règle en question était :

T1 <: S1 S2 <: T2
---------------------
S1 -> S2 <: T1 -> T2

autrement dit, avec les prémisses que T1 est un sous-type de S1 et que S2 est un sous-type de T2, on en conclue que le type des fonctions de S1 vers S2 (noté S1 -> S2) est un sous-type de celui des fonctions de T1 vers T2. La règle se comprend intuitivement ainsi : si j'ai une fonction qui prend un S1, je peux bien lui donner également un T1 étant donné que T1 <: S1 (si j'ai besoin d'un animal, prendre un homme convient aussi); et si je renvoie un S2 alors a fortiori je renvoie aussi un T2 (si je renvoie un chat, je renvoie aussi un félin).

Dans le cas de la méthode add de la classe vect2d, on voit bien le problème : pour fonctionner elle a besoin d'un attribut y sur son entrée, ce que ne peut lui fournir un objet de la classe vect1d.

J'espère avoir été plus clair sur la distinction entre héritage et sous-typage. Si ce n'est pas le cas, et que tu as encore des questions, n'hésite pas. Pour plus d'information, voir aussi la page du manuel OCaml sur les objets.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.