Correspondances logiques et ensemblistes - Application à la généricité

L'association à un type est explicite lorsqu'il est nécessaire de préciser dans chaque déclaration le type du nom, comme en Java. Elle est implicite lorsque le type est inféré de l'expression définissant le nom. Par exemple, la déclaration en Java *String m = "une String"* devient *var m = "une String"* dans le langage scala, qui admet une inférence partielle des types ou encore *let m = "une String"* dans le langage Ocaml, qui admet une inférence complète des types. L'inférence de type présente deux avantages principaux.

• Les déclarations sont plus concises, moins verbeuses, ce qui est généralement apprécié par les programmeurs économes de leur temps.
• Elle augmente les possibilités d'usage de la variable, en calculant le type le plus général. Par exemple, la fonction identité sur les entiers, int id(int x){return x;} en Java, s'écrit en Ocaml let id(x) = x, de type inféré celui d'une fonction de T dans T, pour tout type T : cette dernière peut donc s'utiliser quel que soit le type de l'argument. Il est possible d'obtenir une telle fonction en Java à condition de recourir explicitement à la généricité, comme on va le voir.

L'association entre un nom et un type peut être statique ou dynamique.

Lorsqu'elle est statique, elle est déterminée avant l'exécution du programme et ne change pas pendant l'exécution du programme. Le typage est dit statique : c'est le cas pour les langages C++, Java, Scala et Ocaml.

Au contraire, dans le cas d'un typage dynamique, l'association peut varier pendant l'exécution, suivant la valeur prise par le nom : le type est donc inféré pendant l'exécution. C'est le cas du langage Ruby, comme le montre l'exemple suivant où la variable m reçoit successivement les types String et Fixnum correspondant aux chaînes de caractères et aux (petits) entiers respectivement.

m = "une String"
m = 5

Le typage a pour but premier d'éviter les erreurs de typage lors de l'exécution. Ces erreurs sont pernicieuses car bien souvent, elles restent silencieuses : elles ne "plantent" pas la machine exécutant le programme. Précisément, dans un langage typé, toute opération pouvant s'exécuter est typée : une règle précise le type de ses arguments et le type de son résultat. Par exemple, l'addition accepte deux entiers pour produire un entier, deux réels pour produire un réel, mais n'accepte pas un entier et une chaîne de caractères. L'ensemble de ces règles forme le système de types. Lorsqu'à l'exécution, une règle de typage est violée, par exemple lorsqu'on additionne un entier à une chaîne de caractères, l'opération peut cependant se réaliser et donner un résultat insensé : pour la machine, une chaîne de caractères ressemble à un entier, car elle est représentée de la même façon, par une suite de bits (chiffres binaires, zéro ou un).

On dit que le système de types est sûr (ou que le langage est fortement typé) lorsque toute erreur de typage est détectée. Cette détection peut se produire avant l'exécution : le programme est alors contrôlé de manière à s'assurer qu'il vérifiera pendant l'exécution toutes les règles de typage. Ce contrôle correspond typiquement à une exécution symbolique du programme, où les calculs sur les valeurs sont remplacés par des calculs sur les types. Lorsque le programme passe le contrôle de typage, il est dit bien typé. Alternativement, cette détection peut se produire lors de l'exécution. La machine contrôle avant chaque opération la règle de typage associée et interrompt l'exécution si la règle de typage est violée. Il lui est donc nécessaire d'inférer le type des arguments à partir de leur valeur : la solution, simple, est d'annoter la valeur par son type. Avec un langage typé statiquement, on utilise généralement le contrôle statique, avant l'exécution : c'est le cas de Java. Avec un langage typé dynamiquement, comme Ruby, on utilise nécessairement le contrôle dynamique, au cours de l'exécution.

Le typage dynamique et celui statique diffèrent avant tout par cette variation dans le contrôle. Le typage statique permet de détecter le plus tôt possible les erreurs de typage, mais suppose que les types soient connus avant l'exécution. Cette détection anticipée peut être une limitation lorsqu'elle impose une discipline de typage trop stricte, rendant impossible le développement de programmes pourtant corrects en réduisant l'expressivité du langage.

De manière générale, il est souhaitable d'utiliser le typage statique partout où il est possible, et le typage dynamique lorsqu'il est nécessaire. En effet, le typage statique entraîne les avantages suivants :

• une meilleure documentation, s'appuyant sur les types,
• une exécution plus efficace, les contrôles de typage étant réalisés avant l'exécution et les valeurs n'étant pas annotées par leur type lors de l'exécution,
• une optimisation automatisée du code, utilisant les informations données par les types,
• un meilleur outillage pour l'édition du code, permettant au développeur de profiter des informations de typage.

Quant au typage dynamique, il permet surtout d'adapter les programmes à des variations ou des évolutions imprévues des types.

Un compromis intéressant est d'utiliser le typage graduel. Il permet d'assouplir le typage statique en recourant au typage dynamique si nécessaire.

Exemple : TypeScript ou Javascript avec des types graduels

L'ensemble des types d'un langage de programmation peut se définir inductivement, typiquement par une grammaire en utilisant une notation de Backus-Naur.

On peut interpréter une proposition logique par l'ensemble de ses preuves.

A ou B : Somme({p | p preuve de A}, {p | preuve de B}) (somme disjointe)  
A et B : {(p, q) | p preuve de A et q preuve de B} (produit cartésien)

On utilise alors une correspondance entre les preuves et les programmes d'une part, entre les propositions et les types d'autre part. C'est la correspondance dite de Curry-Howard (du nom de deux logiciens, cf. Wikipedia), qui s'appuie sur la théorie de la démonstration en logique.

Avec cette correspondance, la preuve démontre la proposition si et seulement si le programme habite (a pour type) le type. On observe que la structure d'une preuve reflète la structure de la proposition qu'elle démontre. Avec cette correspondance logique, la structure des programmes reflète ainsi la structure des types. Par exemple, pour prouver une conjonction A et B, on doit disposer d'une preuve p de A et d'une preuve q de B, donc d'un couple (p, q) de preuves. Autrement dit, la conjonction logique se traduit par un produit cartésien. Voici une description plus complète de cette correspondance. Elle s'applique non seulement à la conjonction et à la disjonction mais aussi à l'implication.

Cette correspondance est parfaitement adaptée aux langages fonctionnels, et est d'ailleurs souvent très proche de l'identité (une preuve étant alors un programme, et une proposition un type): elle permet de donner une interprétation logique aux constructeurs de types et de termes d'un langage fonctionnel.

Exemple dans un langage fonctionnel (le langage inclus dans l'assistant à la preuve COQ)

A B : Set.
a : A.
b : B.

(* Produit cartésien *)
(* 1. Couple *)
(a, b) : A * B.
(* 2. Projections *)
fst (a, b) : A.
snd (a, b) : B.

(* Somme disjointe *)
(* 1. Plongements *)
(inl B a) : A + B.
(inr A b) : A + B.
(* 2. Filtrage *)
Definition f(C : Set)(g : A -> C)(d : B -> C)(x : A + B) : C :=
match x with 
    inl y => g y
  | inr z => d z
end.

(* Type flèche *)
(* 1. Abstraction *)
(fun (x : A) => b) : A -> B.
(* 2. Application *)
f : A -> B.
(f a) : B.

Complément (un peu digressif) : Il est en revanche plus compliqué de définir une correspondance pour la négation. C'est cependant possible en partant de la définition de (non A) par (A -> Faux) et en utilisant ce type pour représenter les piles d'exécution. Les constructeurs associés qui sont des opérateurs de contrôle permettent alors d'implémenter un mécanisme d'exceptions. On peut alors distinguer

• les expressions qui produisent des valeurs (les termes habituels),
• les expressions qui consomment des valeurs (les piles),
• les calculs, qui résultent de la mise en relation d'une pile et d'un terme (d'où la dualité des calculs).

Un des nouveaux opérateurs associés à la négation réalise une inversion du contrôle : il permet à un terme de capturer la pile courante et ainsi de rendre possible son remplacement par une pile de son choix.

On peut interpréter un ensemble en extension, par la collection de ses éléments.

{v | v appartient à A union B} = Union({v | v appartient à A}, {v | v appartient à B})
{v | v appartient à A inter B} = Intersection({v | v appartient à A}, {v | v appartient à B})

(Union et Intersection représentent ici les opérations habituelles sur les ensembles).

On utilise alors une correspondance entre les éléments et les programmes d'une part, entre les ensembles et les types d'autre part. Cette correspondance peut s'interpréter logiquement également : modèles logiques et programmes d'un côté, propositions logique et types de l'autre. Elle repose sur la théorie des modèles en logique et non pas sur la théorie de la démonstration comme celle de Curry-Howard. Pour simplifier, on utilisera la correspondance avec les ensembles.

Avec cette correspondance, l'élément appartient à l'ensemble si et seulement si le programme habite (a pour type) le type. On observe que la structure d'un élément ne reflète pas la structure de l'ensemble auquel il appartient. Avec cette correspondance ensembliste, la structure des programmes ne reflète donc plus la structure des types. En conséquence, il est plus difficile de vérifier le type d'un programme. C'est une différence fondamentale avec le point de vue logique.

Cette correspondance permet enfin d'interpréter

• la relation de sous-typage par l'inclusion,
• le type le plus général (comme Object en Java) par l'univers (l'ensemble contenant tous les autres ensembles),
• le complémentaire par le complémentaire dans l'univers.

A sous-type de B : A inclus dans B
Object : Univers 
Complémentaire A : Univers - A

Complément (un peu digressif) : L'implication A -> B peut se définir par (non A) ou B. On s'éloigne ici de l'interprétation fonctionnelle de l'implication vue précédemment en suivant le point de vue logique.

Très souvent, un langage de programmation utilise les deux points de vue simultanément.

Passons en revue les différentes constructions, en prenant les deux points de vue.

Approche logique

type ::= ... | T | existe T^+ tel que P.type | pour tout T^+ tel que P.type
   P ::= ... (propriété)

• variable de type : T

• quantification existentielle comme disjonction infinie

  existe T tel que P. type(T) : type(A1) ou type(A2) ou ...
  (A1, A2, ... parcourant tous les types vérifiant P)
  

• quantification universelle comme conjonction infinie

  pour tout T tel que P. type(T) : type(A1) et type(A2) et ...
  (A1, A2, ... parcourant tous les types vérifiant P)
  

Approche ensembliste

type ::= ... | T | Union T tel que P.type | Inter T tel que P.type

• variable de type : T

• union dépendant de T comme union infinie

  Union T tel que P. type(T) : type(A1) union type(A2) union ...
  (A1, A2, ... parcourant tous les types vérifiant P)
  

• intersection dépendant de T comme intersection infinie

  Inter T tel que P. type(T) : type(A1) inter type(A2) inter ...
  (A1, A2, ... parcourant tous les types vérifiant P)
  

Les propriétés utilisées pour relativiser les quantifications et les paramétrisations s'expriment dans un langage logique minimal.

P ::= Vrai | (type <= type) | P et P

Une propriété peut être

• vraie (et alors omise),
• une comparaison utilisant la relation de sous-typage soit l'inclusion suivant le point de vue ensembliste, ou enfin
• une conjonction de propriétés.

Elle représente donc une suite de contraintes liées à la relation de sous-typage.

La généricité en Java repose sur des unions et des intersections dépendantes (d'un type), suivant le point de vue ensembliste, dans le sens où la structure ne reflète pas la structures des types union ou intersection. Les propriétés utilisées pour la relativisation sont élémentaires : pas de contrainte, majorations (au pluriel pour les intersections, au singulier pour les unions) ou minoration (au singulier) du paramètre de type.

On représente une union dépendante en utilisant le joker ? (wildcard).

Union T.A : A[?/T]

L'expression A[?/T] signifie que le paramètre T est remplacé par le joker ? dans le type A. Comme on utilise un seul symbole, le joker, le paramètre T a au plus une occurrence. Cette occurrence ne peut être qu'un argument d'un constructeur de type (sinon, elle pourrait être remplacée par la borne supérieure du paramètre de type). Il est possible de préciser des contraintes de sous-typage, sous une forme simplifiée, puisqu'un unique majorant ou minorant est possible.

(? remplaçant T)
  ? : T tel que Vrai
  ? extends A : T tel que (T <= A) 
  ? super A : T tel que (A <= T)

Enfin, un type représentant une union dépendante n'est pas un type plein : il ne peut servir de sur-type dans une déclaration d'héritage ou d'implémentation. En revanche, il peut servir à borner un paramètre de type ou à typer une variable.

Exemples

Union T.List<T> : List<?>
Union T.Couple<T, T> : impossible
Union T1 T2.Couple<T1, T2> : Couple<?, ?> 
Union T tel que T <= Comparable<T>.List<T> : List<? extends Comparable<T>>

Avec cette interprétation du joker, il est facile de justifier différentes règles de sous-typage.

Premier exemple : inclusion dans l'union

List<A> sous-type de List<?> :
  List<A> inclus dans Union(List<A>, ...)

Second exemple : covariance pour des listes

si A sous-type de B, alors 
  List<? extends A> sous-type de 
  List<? extends B> :
si A inclus dans B, alors   
  (Union T tel que T <= A. List<T>) inclus dans 
  (Union T tel que T <= B. List<T>)   
(puisque (T <= A et A <= B) implique (T <= B), <= étant l'inclusion)

Grâce à cette règle, il devient possible d'obtenir des listes covariantes en Java. Il suffit de remplacer Liste<E> par Liste<? extends E>.

interface Liste<E> {
  boolean estVide();
  E tete();
  Liste<? extends E> reste();
}

Un calcul générique peut avoir pour type une intersection dépendante : c'est une généralisation de la surcharge interprétée comme une intersection. Seuls les types fonctionnels (implicites) sont donc concernés.

Inter T.(A -> B) : <T> B f(A x)
  (f : nom arbitraire)

Il est possible de préciser des contraintes de sous-typage, sous une forme simplifiée, comme précédemment.

T : T tel que Vrai
T extends A: T tel que (T <= A) 
T extends A & B : T tel que (T <= A) et (T <= B)

Exemples #+BEGIN_SRC java interface I { // Méthode d'une interface <T> B f(A x); } class C { // Constructeur <T> C(A x) { … } // Méthode d'une classe <S extends E, T extends F & G> B g(A x) { … } // Fonction static <T> B h(A x) { … } } #+END_SRC java

Avec cette interprétation des calculs génériques, il est facile de justifier certaines règles de typage, comme précédemment. Voici un exemple en Java 8, où A est un sous-type de B. #+BEGIN_SRC java @FunctionalInterface interface EG { <T extends A> T f(T x); } class FG { public static <T extends B> T g(T x){ return …; } } … EG f = FG::g; // Conversion de (<T extends B> (T -> T)) vers (<T extends A> (T -> T)) #+END_SRC java Voici la justification.

si A sous-type de B, alors 
  <T extends B> (T -> T) sous-type de 
  <T extends A> (T -> T) :
si A inclus dans B, alors   
  (Inter T tel que T <= B. (T -> T)) inclus dans 
  (Inter T tel que T <= A. (T -> T))
(puisque (T <= A et A <= B) implique (T <= B), <= étant l'inclusion)

Résumons les limitations observées précédemment.

• Minoration impossible sauf pour le joker.
• Minoration et majoration uniquement possibles par un unique type pour le joker.
• Minoration ou majoration pour le joker, mais pas les deux simultanément.
• Utilisation du joker pour représenter la variable de quantification.
• Pas d'ordre supérieur pour la généricité.

Pour des raisons de compatibilité avec la machine virtuelle qui n'évolue pas, le compilateur Java depuis la version 5, qui a introduit la généricité, procède ainsi.

• Il vérifie le typage en utilisant la généricité.
• Il traduit du Java avec généricité en Java sans généricité, en effaçant les paramètres de types et en rajoutant les conversions explicites manquantes.

C'est la stratégie dite d'effacement. Elle s'oppose à la stratégie dite de récriture : chaque instanciation d'un type générique est compilée en un nouveau type, la récriture du type générique en un type non générique, où toutes les occurrences des paramètres de types sont remplacées par leurs valeurs. C'est la stratégie utilisée par le langage C++, où les types génériques sont appelés "templates", à raison.

Effacement (après vérification du typage)

• Un type générique est compilé en un type non générique où le paramètre de type est remplacé par un majorant, le premier type apparaissant dans la majoration, Object par défaut.

  interface A<T> {
    T f();
  }
  // devient
  interface A {
    Object f();
  }
  
  interface B<T extends M & N> {
    T f();
  }
  // devient
  interface B {
    M f();
  }
  

• Des conversions explicites sont ajoutées.

  B<L> x = ...; // L sous-type de M et N
  L y = x.f();
  // devient
  B x = ...; 
  L y = (L)(x.f());
  

L'effacement entraîne des limitations : cf. https://docs.oracle.com/javase/tutorial/java/generics/restrictions.html.

Impossibilités et possibles remèdes (résumé)

• Impossible d'instancier avec des types primitifs : utiliser les types enveloppes (Integer au lieu de int, etc.)
• Impossible de construire des instances des paramètres de types : utiliser des fabriques
• Impossible d'avoir des paramètres de types libres dans les variables et les fonctions statiques : utiliser des tables prenant des types (Class<?>) en argument
• Impossible d'avoir des tableaux utilisant un paramètre de type : utiliser ArrayList
• Impossible de surcharger une méthode par une autre dont les versions après effacement sont identiques
• Impossible de convertir explicitement ou de tester le type pour les types instanciés : passer par le type utilisant le joker au lieu du paramètre ou utiliser une meilleure représentation des types par une nouvelle méthode équivalente à getClass
• Impossible de définir des exceptions génériques ou de traiter (par un catch) des exceptions paramétrées par un type

Cf. genericite.limitations.Effacement et genericite.limitations.GenericiteEtModule pour des exemples et des explications en commentaire pour chacun des cas précédents.

En Java, le joker, qui sert à représenter des unions dépendantes, pose des problèmes de deux sortes essentiellement :

• la non-terminaison de l'algorithme déterminant la relation de sous-typage (lors de la compilation),
• des imprécisions dans l'inférence des types.

Globalement, les choix faits par les concepteurs pour résoudre ces problèmes ne sont pas toujours cohérents ni réguliers. Heureusement, ces problèmes apparaissent rarement, à la marge, lorsqu'on programme en Java. En revanche, ils importent dès lors qu'on veut spécifier et implémenter un compilateur (et possiblement une machine virtuelle).