UP | HOME

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

Table of Contents

1 Introduction : de la logique à la programmation

Pour bien comprendre la généricité, il est utile de prendre un point de vue logique ou ensembliste sur les types. Plus généralement, un tel point de vue favorise une compréhension fine de tout système de types d'un langage de programmation. Après une introduction générale sur les systèmes de types, nous adoptons ce point de vue, logique ou ensembliste, pour expliquer le système de types de Java, et en particulier la généricité.

2 Systèmes de types

Lorsqu'un langage de programmation est typé, dans toute déclaration, on associe un type à un nom. Cette association peut être d'une part, implicite ou explicite, d'autre part, statique ou dynamique.

2.1 Typage explicite, typage implicite

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.

2.2 Typage statique, typage dynamique

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

2.3 Sûreté de typage

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.

2.4 Typage dynamique ou statique ?

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

2.5 Syntaxe

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.

2.5.1 Des types de base

type ::= Base

Ces types forment les types de base de la définition inductive.

Exemple: int, boolean, Object, Date en Java (ensemble des types primitifs et des types références)

2.5.2 Des constructeurs de types

type ::= ... | Constructeur(type^*)

Un constructeur de types est aussi appelé un type générique : à partir de types déjà construits, le constructeur permet de construire un nouveau type.

Exemples en Java

Généricité

interface Liste<T> { ... }

Le type générique Liste est défini pour tout type T ainsi : (une définition pouvant utiliser T).

Il est possible de relativiser la définition, en majorant le type T par un ou plusieurs types. La minoration est impossible en Java, mais possible en Scala par exemple.

interface ListeTriee<T extends Comparable<T>> { ... }

Le type générique ListeTriee est défini pour tout type T sous-type de Comparable<T> ainsi : (une définition pouvant utiliser T sous-type de Comparable<T>).

Tableaux

int[]

En java, le constructeur de tableaux [] est le seul constructeur de types qui est primitif.

Les constructeurs précédents sont du premier ordre : à partir de types, ils produisent un type. On pourrait aussi autoriser des constructeurs d'ordre supérieur : à partir de types et d'autres constructeurs, ils produisent des types. En Java, seuls les constructeurs du premier ordre sont licites. Cette limitation est levée en Scala où par exemple le code suivant (utilisant la syntaxe de Java) est possible.

import java.util.function.Function;
// Définition d'une propriété par une interface.
// Cette propriété dépend 
// - d'un constructeur de types L (pour Liste),
// - d'un type E (pour Element).    
interface FoncteurListe<L<_>, E> {
  <F> L<F> application(Function<E, F> f);
}
// Définition du type générique Liste.
// Ce constructeur de types a la propriété FoncteurListe.
interface Liste<E> extends ..., FoncteurListe<Liste, E> { ... }

Pour plus de détail sur les constructeurs d'ordre supérieur en Scala, cf. Generics of a Higher Kind.

3 Types comme propositions ou comme ensembles

Pour définir un système sûr de types, le point de vue logique ou ensembliste est d'une aide précieuse. En effet, il permet de définir des constructeurs non seulement de types mais aussi de valeurs ou d'expressions. Il permet aussi de déduire des règles de typage garantissant la sûreté de typage.

Approche logique : disjonction (ou), conjonction (et)

type ::= ... | type ou type | type et type

Approche ensembliste : union, intersection

type ::= ... | type union type | type inter type

Ces constructeurs sont fondamentaux et universels, au sens où ils sont utilisés implicitement ou explicitement dans tout langage de programmation. On pourrait aussi ajouter la négation et le complémentaire, ce qui serait utile mais est rarement rencontré dans les langages courants de programmation.

Le sens de ces opérateurs logiques et ensemblistes dans le langage de programmation doit alors correspondre à celui habituel. Comment le définir ? On utilise deux correspondances fondamentales, associées aux points de vue logique et ensembliste respectivement. Elles permettent de définir le sens des opérateurs dans un langage de programmation.

3.1 Point de vue logique

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.

Logique Langage
Preuve Programme
Proposition
Type
Relation Démonstration Habitation

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.

Opérateur logique
Constructeur de types
Constructeur Destructeur
conjonction (et)
produit cartésien
couple projection
disjonction (ou)
somme disjointe
plongement filtrage par cas
implication type flèche des fonctions
abstraction fonctionnelle
application

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.

3.2 Point de vue ensembliste

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.

Théorie des ensembles
Langage
Elément Programme
Ensemble
Type
Relation Appartenance Habitation

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.

3.3 Combinaison des deux points de vue

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

3.3.1 Constructions logiques

Le point de vue logique s'applique pour les constructeurs de types et d'expressions. Il permet ainsi de définir les implémentations. Typiquement, pour une implémentation, on utilise :

  • des sommes disjointes (disjonction, ou),
  • des produits cartésiens (conjonction, et),
  • des types flèches (implication).

Ainsi, dans un langage fonctionnel, on définit un type de données par des définitions inductives. La forme la plus simple d'une définition inductive est un type algébrique, une somme définie récursivement de produits. Les opérations sur les données sont définies par des fonctions récursives.

Exemple de listes inductives en Coq

Inductive Liste(T : Set) :=
| Vide : Liste T
| Cons : T -> Liste T -> Liste T.

Fixpoint longueur {T : Set} (l : Liste T) :=
match l with
    Vide => 0
  | Cons t r => 1 + (longueur r)
end.

Dans un langage à objets, on suit une approche assez similaire : une implémentation est une somme disjointe de classes, chaque classe étant un produit cartésien d'attributs et de méthodes.

Exemple de listes inductives en Java (patron composite)

interface Liste<E> {
  Liste<E> reste();
  E tete();
  boolean estVide();
  int taille();
}
final class Vide<E> implements Liste<E> {
  private Vide(){}
  @SuppressWarnings("rawtypes")
  private static final Liste<?> VIDE = new Vide();
  @SuppressWarnings("unchecked")
  public static <E> Liste<E> fabriquer() {
    return (Liste<E>)VIDE;
  }
  @Override
  public Liste<E> reste() {
    throw new UnsupportedOperationException();
  }
  @Override
  public E tete() {
    throw new UnsupportedOperationException();
  }
  @Override
  public boolean estVide() {
    return true;
  }
  @Override
  public int taille() {
    return 0;
  }
}
final class Cons<E> implements Liste<E> {
  private E tete;
  private Liste<E> reste;       
  private Cons(E head, Liste<E> tail) {
    this.tete = head;
    this.reste = tail;
  }
  @Override
  public Liste<E> reste() {
    return reste;
  }
  @Override
  public E tete() {
    return tete;
  }
  @Override
  public boolean estVide() {
    return false;
  }
  @Override
  public int taille() {
    return 1 + this.reste().taille();
  }
}

3.3.2 Constructions ensemblistes

Le point de vue ensembliste s'applique aux types. Principalement, il permet d'introduire une notion de sous-typage, fondée sur l'inclusion ensembliste. A la relation de sous-typage est associée la règle de subsomption, permettant de convertir d'un sous-type vers un super-type. Elle exprime exactement l'inclusion ensembliste.

\[\small \begin{array}{c} (e : A) \quad A \leq B \\ \hline (e : B) \end{array} \]

Comme le point de vue ensembliste ne fournit pas de constructeurs d'expressions, il ne s'applique qu'aux types purs, en particulier aux interfaces. On s'intéresse à ce cas fondamental ci-dessous.

3.3.2.1 Sous-typage en largeur

La relation de sous-typage intervient tout d'abord entre une interface et ses implémentations : chaque implémentation est un sous-type de l'interface. Elle s'applique aussi aux interfaces. On peut considérer qu'une interface définit une liste de méthodes typées. La relation de sous-typage correspond alors à une extension de cette liste. De même, la réunion correspond à l'intersection des listes et l'intersection à la réunion des listes.

Voici ce que cela donnerait en utilisant une syntaxe inspirée de Java.

interface I {
  A f(B x);
  C g(D y);
}
interface J {
  C g(D y);
  E h(F z);
}
interface K {
  A f(B x);
}
I union J {
  C g(D y);
} 
I inter J { 
  A f(B x);
  C g(D y);
  E h(F z);
}
K inter J { 
  A f(B x);
  C g(D y);
  E h(F z);
}
K union J {}

On aurait alors :

  • I et J incomparables, comme K et J,
  • I sous-type de *K,
  • I inter J, égal à K inter J, sous-type de I, J et K,
  • I et J sous-types d'I union J,
  • interface vide plus grand élément (pour la relation de sous-typage).

La notion de sous-typage que nous venons de décrire pour les interfaces définies comme une liste de méthodes correspond à un sous-typage dit en largeur. Il existe une autre notion de sous-typage : celui en profondeur. Il correspond au raffinement d'une méthode par une méthode d'un sous-type.

3.3.2.2 Sous-typage en profondeur et variance

Considérons les deux interfaces suivantes.

interface I {
  A f(B x);
}
interface J {
  C f(D x);
}

A quelle condition a-t-on J sous-type de I ? Il suffit que le type fonctionnel D -> C soit sous-type de B -> A, ce qui est le cas si C est un sous-type de A et B est un sous-type de D : c'est un exemple de sous-typage en profondeur. A chaque constructeur de types est associée une règle dite de variance, qui exprime la possible monotonie (croissance ou décroissance) du constructeur relativement à la relation de sous-typage. Voici le cas des trois constructeurs correspondant au point de vue logique.

Produit cartésien : covariance (croissance)

\[\small \begin{array}{c} A_1 \leq B_1 \quad A_2 \leq B_2 \\ \hline A_1 \times A_2 \leq B_1 \times B_2 \end{array} \]

Somme disjointe : covariance

\[\small \begin{array}{c} A_1 \leq B_1 \quad A_2 \leq B_2 \\ \hline A_1 + A_2 \leq B_1 + B_2 \end{array} \]

Flèche fonctionnelle : covariance pour le résultat, contravariance (décroissance) pour l'argument

\[\small \begin{array}{c} B_1 \leq A_1 \quad A_2 \leq B_2 \\ \hline A_1 \rightarrow A_2 \leq B_1 \rightarrow B_2 \end{array} \]

Pour déterminer ces règles pour un constructeur K de types, on procède ainsi. Considérons une expression e de type K(A,B) (en supposant que le constructeur admette deux arguments) convertible en K(C, D). On étudie alors tous les usages possibles en tant qu'expression de type K(C, D), en veillant à garantir l'absence d'erreurs de typage, ce qui permet de définir les relations entre C et A d'une part, D et B d'autre part. Par exemple, considérons e de type A -> B convertible en C -> D. La fonction e peut être appliquée à un argument de type C, qui doit être un sous-type de A. Elle produit alors un résultat de type B qui doit être un sous type de D. Cet exemple illustre l'intuition derrière la variance : la covariance s'applique aux types produits, la contravariance aux types consommés.

Tableau : invariance (c'est-à-dire ni covariance ni contravariance, pas de monotonie)

Pour montrer l'invariance, on raisonne par l'absurde. Supposons que la règle de variance s'applique. Voici un exemple qui montre qu'on peut provoquer une erreur de typage lors de l'exécution.

interface A {}
interface B extends A {
        void f();
}
// Hypothèse : règle de covariance valide
  B[] tabB = new B[1];
  A[] tabA = tabB; // Covariance licite en java
  tabA[0] = new A(){};
  tabB[0].f(); // Erreur : pas de f sur un A
// Hypothèse : règle de contravariance valide
  A[] tabA = new A[1];
  B[] tabB = (B[])tabA; // Contravariance illicite en java (d'où une conversion explicite) 
  tabA[0] = new A(){};
  tabB[0].f(); // Erreur : pas de f sur un A

Noter qu'en Java, les erreurs sont détectées avant l'invocation de f, lors de l'écriture et lors de la conversion respectivement.

Tableau en lecture seulement : covariance

\[\small \begin{array}{c} A \leq B \\ \hline A[] \leq B[] \end{array} \]

Tableau en écriture seulement : contravariance

\[\small \begin{array}{c} A \leq B \\ \hline B[] \leq A[] \end{array} \]

Intuitivement, un tableau de A

  • en lecture seulement, produit des A, d'où la covariance,
  • en écriture seulement, consomme des A, d'où la contravariance,
  • en lecture et en écriture, produit et consomme des A, d'où l'invariance.

Constructeur générique : covariance pour un paramètre de type si tout type de méthode est covariant pour ce paramètre, contravariant si tout type de méthode est contravariant pour ce paramètre, invariance sinon (la détermination de la covariance exige donc de décomposer récursivement chaque type en une liste des types de ses méthodes.)

Exemples de listes

Java (incorrect - en Java, les constructeurs génériques de types sont invariants)

// Covariance (en principe mais pas en réalité)
interface Liste1<T> {
  T tete();
  Liste1<T> reste();
}
// Invariance
interface Liste2<T> {
  T tete();
  Liste2<T> reste();
  Liste2<T> cons(T t); // fabrique
}
// Covariance grâce à une astuce classique (en principe mais pas en réalité)
interface Liste3<T> {
  T tete();
  Liste3<T> reste();
  <S super T> Liste3<S> cons(S t); // Pour tout S surtype de T, ... 
                                   //   (minoration impossible en Java)
}
// Contravariance (en principe mais pas en réalité)
interface Liste4<T> {
  void setTete(T t)
  Liste4<T> reste();
}

Scala (correct moyennant des annotations de variance) - Cf. les annotations de variance.

# Covariance 
trait Liste1[+T] {
    def tete() : T
    def reste() : Liste1[T] 
}
# Invariance
trait Liste2[T] {
    def tete() : T
    def reste() : Liste2[T]
    def cons(t : T) : Liste2[T]
}
# Covariance grâce à l'astuce classique
trait Liste3[+T] {
    def tete() : T
    def reste() : Liste3[T]
    def cons[S >: T](t : S) : Liste3[S]
}
# Contravariance
trait Liste4[-T] {
    def tete_=(t : T)
    def reste() : Liste4[T]
}

Remarque : le compilateur du langage Scala vérifie la cohérence de la définition de la variance (par un plus ou un moins). Précisément, il suppose la variance et vérifie que tous les types des méthodes varient de la même manière, en utilisant l'hypothèse de variance. Bref, pour montrer la variance, il utilise la variance : c'est une exemple de raisonnement coinductif.

3.4 Cas du langage Java

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

3.4.1 Point de vue logique : des constructeurs implicites

Le produit cartésien est présent implicitement, lorsqu'on définit les membres d'une classe ou d'une interface. On peut aussi le coder explicitement par un type générique : c'est ce qui est fait en Scala.

La somme disjointe est présente implicitement, lorsqu'on implémente une interface par plusieurs classes.

Le type flèche des fonctions est défini implicitement : c'est le type implicite des fonctions et des méthodes. Depuis Java 8, il existe une représentation des fonctions et donc des types flèches par des objets, via les interfaces fonctionnelles. Une interface fonctionnelle est une interface possédant une seule méthode abstraite (non implémentée), correspondant à l'application. Cf. le cours sur les lambda-expressions.

De manière générale, le langage utilise peu de règles de variance.

  • Tableaux : covariance. Cette règle est valide mais n'est pas sûre. Elle nécessite un contrôle du bon typage des écritures. Elle était utile dans les versions initiales de Java, sans généricité.

    // B sous-type de A
    B[] tabB = new B[1];
    A[] tabA = tabB; // Conversion licite par covariance
    tabA[0] = new A(){};  // Contrôle : A sous-type de B (type des éléments stockés) ?
                          // -> Erreur : java.lang.ArrayStoreException
    
  • Type flèche des méthodes : covariance pour le type de retour. Cette règle permet de raffiner le type de retour d'une méthode redéfinie. En revanche, la règle de contravariance ne s'applique pas : si une méthode raffine par un sur-type le type des arguments, alors elle surcharge la méthode initiale.

    interface A {
      A fabrique();
    }
    interface B extends A {
      B fabrique(); // Redéfinition
    }
    
  • Type flèche des interfaces fonctionnelles : covariance du type de retour et contravariance du type des arguments pour les références de méthodes et de fonctions, mais pas pour les lambda-expressions. On privilégiera donc des lambda-expresssions sans indication de types, ce qui impose une inférence qui utilise naturellement les règles de variance.

    interface A {}
    interface B extends A {}
    interface A1 {}
    interface B1 extends A1 {
      A g();
    }
    @FunctionalInterface
    interface F {
      A f(B1 x);
    }
    
    public static A f1(B1 x){ ... }
    public static B f2(A1 x){ ... }
    
      F fctn = Variance::f1; // B1 -> A sous-type de B1 -> A
      fctn = Variance::f2;   // A1 -> B sous-type de B1 -> A
      fctn = B1::g; // B1 -> A sous-type de B1 -> A
      fctn = (B1 x) -> null; // B1 -> A sous-type de B1 -> A
      // fctn = (A1 x) -> null; // erreur : pas de variance
      fctn = x -> null; // Inférence : B1 -> A
    

Les types génériques sont tous invariants. En effet, comme pour les tableaux, les règles de covariance ou de contravariance pourraient aboutir à des erreurs de typage. Cette discipline, très restrictive, est abandonnée en Scala au profit d'annotations de variance.

3.4.2 Point de vue ensembliste : le sous-typage comme point de départ

Le relation d'inclusion ensembliste est représentée par la relation de sous-typage : c'est la fermeture réflexive et transitive engendrée par la réunion

  • de la relation d'héritage (mot clé extends) et
  • de la relation d'implémentation (mot clé implements).

Elle forme une relation d'ordre.

Une fois que la relation de sous-typage est définie, l'union et l'intersection peuvent se définir implicitement, comme la borne supérieure (plus petit des majorants) et la borne inférieure (plus grand des minorants). De fait, elles n'existent pas toujours, comme le montre l'exemple suivant.

interface A {}
interface B {}
interface I extends A, B {}
interface J extends A, B {}

Voici le diagramme correspondant de types.

Set_unionIntersectionJava.png

On constate que l'union de I et J et l'intersection de A et B n'existent pas comme types. Pour représenter une union, la seule solution est d'utiliser un nouveau type. Pour une intersection, il est possible de la définir, mais dans deux contextes restreints.

  • Héritage : on peut spécifier qu'on hérite de plusieurs interfaces, ce qui correspond à un type intersection.

    interface I extends A, B // I sous-type de Intersection(A, B)
    
  • Majoration d'un paramètre de type : on peut spéciifer que le majorant d'un paramètre est un type intersection.

    interface K<T extends A & B> // pour tout type T sous-type de Intersection(A, B)
    

    Remarque : la minoration par une intersection est impossible pour une raison obscure.

    K<? super I & J> // non autorisé
    

En dehors de ces contextes, il est nécessaire d'utiliser un nouveau type pour représenter une intersection.

Enfin, pour les fonctions ou les méthodes, la surcharge définit implicitement une intersection de types fonctionnels.

B f(A x);
D f(C y);

La méthode surchargée f a le type (A -> B) inter (C -> D).

4 La généricité comme disjonctions/conjonctions ou unions/intersections infinies

On peut généraliser les constructeurs disjonctions/unions et conjonctions/intersections, en passant du cas fini au cas infini. L'idée est de considérer des familles paramétrées par un type : la paramétrisation permet de représenter une famille infinie de manière finie.

4.1 Généralisation

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.

4.2 La généricité en Java

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 d'un programme 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

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) { ... }
}

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.

@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))

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)

5 Limitations de la généricité en Java

En dehors de choix discutables de conception, les limitations ont deux causes principales :

  • l'effacement des paramètres de types lors de la compilation,
  • la présence du joker, autrement dit des unions dépendantes.

5.1 Choix discutables de conception

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é.

5.2 Effacement

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.GenericiteEtClasseModule pour des exemples et des explications en commentaire pour chacun des cas précédents.

5.3 Imperfections du joker

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).

5.3.1 Non-terminaison pour le sous-typage

On cherche un jugement de sous-typage tel que sa preuve ne peut être qu'infinie, ce qui provoquera la non-terminaison du compilateur. On définit progressivement des hypothèses pour produire une preuve infinie d'un jugement de sous-typage. La preuve est formée des buts successifs à prouver.

  • But 1 : A <= B
  • Hypothèse 1 : A = C<D>, B = C<? tel que P(?)> (union dépendante)
  • But 2 : P(D)
  • Hypothèse 2 : P(D) = A <= B
  • But 2' : A <= B - Problème : c'est le but 1 !

Les hypothèses 1 et 2 permettent-elles de définir A, B, C et D ?

Deux scénarios possibles (finalement incohérents)

  • Scénario 1 (un mauvais choix finalement)
    • Hypothèse 2 : D = A, P(X) = (X <= B) (où X est une variable)
    • Hypothèse 1 : A = C<A>, B = C<? extends B> - Impossible : définitions circulaires de A et B
  • Scénario 2 (un mauvais choix finalement)
    • Hypothèse 2 : D = B, P(X) = (A <= X) (où X est une variable)
    • Hypothèse 1 : A = C<B>, B = C<? super A> - Impossible : définition circulaire de A

Cette première tentative a échoué : cependant, les scénarios pourraient fonctionner si on remplace l'égalité par la relation de sous-typage, puisque la circularité disparaîtrait. Voici la nouvelle tentative, où on introduit un type intermédiaire A1.

  • Hypothèse 1 : A <= A1
  • But 1 : A <= B
  • But 2 (impliquant But 1) : A1 <= B
  • Hypothèse 2 : B = C<? tel que P(?)> (union dépendante)
  • Hypothèse 3 : A1 = C<D>
  • But 3 : P(D)
  • Hypothèse 4 : P(D) = (A <= B)
  • But 3' : A <= B - Problème : c'est le but 1 !

Les hypothèses 1, 2, 3 et 4 permettent-elles de définir A, A1, B, C et D ?

Deux scénarios possibles (finalement un seul cohérent)

  • Scénario 1 (un mauvais choix finalement)
    • Hypothèse 4 : D = A, P(X) = (X <= B) (où X est une variable)
    • Hypothèse 3 : A1 = C<A>
    • Hypothèse 2 : B = C<? extends B> - Impossible : définition circulaire
  • Scénario 2 (le bon choix)
    • Hypothèse 4 : D = B, P(X) = (A <= X) (où X est une variable)
    • Hypothèse 3 : A1 = C<B>
    • Hypothèse 2 : B = C<? super A>
    • Hypothèse 1 : A <= C<C<? super A>>

Traduction en Java

interface C<T> {}
interface A extends C<C<? super A>> {}

    A x = null;
    C<? super A> y = x;

Le compilateur (version 1.8) n'accepte pas ce programme.

error: incompatible types: A cannot be converted to C<? super A>
	C<? super A> y = x;
	                 ^
1 error

Il est en effet spécifié que les preuves d'un jugement de sous-typage sont finies, obtenues par réflexivité et transitivité à partir de la relation de sous-typage direct.

Cf. la spécification du langage Java, chapitre \(4.10\) : https://docs.oracle.com/javase/specs/jls/se8/html/jls-4.html#jls-4.10.

De cet exemple, on peut définir une variante générique.

  • Hypothèse 1 : A<T> <= C<C<? super A<T>>>
  • But 1 : A<E> <= C<? super A<E>>
  • But 2 (impliquant But 1) : C<C<? super A<E>>> <= C<? super A<E>>
  • But 3 : A<E> <= C<? super A<E>> (circularité)

Le compilateur produit le même verdict. Mais à partir de cette version générique, on peut maintenant obtenir une preuve infinie, mais non régulière, que le compilateur ne peut plus détecter.

  • Hypothèse 1 : A<T> <= C<C<? super A<A<T>>>>
  • But 1 : A<E> <= C<? super A<E>>
  • But 2 (impliquant But 1) : C<C<? super A<A<E>>>> <= C<? super A<E>>
  • But 3 : A<E> <= C<? super A<A<E>>>
  • But 4 : C<C<? super A<A<E>>>> <= C<? super A<A<E>>>
  • But 5 : A<A<E>> <= C<? super A<A<E>>> (But 1, avec E transformé en A<E>, d'où l'infini sans circularité, sans régularité)

    interface C<T> {}
    interface ADiv<T> extends C<C<? super ADiv<ADiv<T>> >> {}
    
      ADiv<String> x = null;
      C<? super ADiv<String>> y = x;
    

Le compilateur fait exploser la pile d'exécution : il ne termine pas normalement !

La solution de ce problème n'est pas aisée : en effet, avec un système de types très riche, il est possible que la relation de sous-typage ne soit plus décidable. C'est un domaine actif de recherche.

Cf. genericite.limitations.PreuveInfinie.

5.3.2 Inférence imprécise des types

L'inférence imprécise se manifeste particulièrement dans le typage de l'alternative, expression qu'on écrit ainsi en Java :

cond ? a : b

Comment l'alternative est-elle typée ? Le système de types de Java possède une règle qu'on peut décrire ainsi.

(cond : Boolean)  (a : A)  (b : B)  (A <= M)  (B <= M) 
------------------------------------------------------
                  ((cond ? a : b) : M)

Elle affirme que si

  • cond est un booléen,
  • a est un A,
  • b est un B et
  • A et B sont deux sous-types de M,

alors l'alternative (cond ? a : b) a pour type M. Malheureusement, le compilateur ne peut pas déterminer en général le plus petit des majorants M (la borne supérieure de A et B n'existant pas toujours), et se révèle incapable d'inférer un majorant dans des situations pourtant simples.

Distinguons trois cas pour le typage d'une alternative.

  • Conversion implicite : l'alternative doit être convertie implicitement en un certain type X, pris alors pour le majorant M.
  • Conversion explicite : l'alternative doit être convertie explicitement en un certain type X, pris alors pour le majorant M.
  • Inférence : l'alternative doit être convertie implicitement en un type X paramétré par T, que le compilateur prend pour majorant. Il essaie alors d'inférer le type T, supposé identique pour les deux branches.

Si les conversions fonctionnent correctement, en revanche l'inférence ne fonctionne pas. Un remède possible mais partiel est de remplacer le paramètre de type T par ? extends T, ce qui est possible s'il n'y a qu'une occurrence de T.

L'erreur dans la spécification est de considérer le même type T dans les deux branches de l'alternative. Cette interprétation diffère de celle ensembliste, où le type de l'alternative serait A union B.

Exemple

class A<T>{}

static <T> void inference1(A<T> x){}
// Version raffinée permettant l'inférence 
static <T> void inference1Cor(A<? extends T> x){}

static void test2(int x, A<? super Double> d, A<? super Double> i){
  A<? super Double> c = (x == 0)? d : i;
  inference1(c); // inférence du paramètre T avec capture
  inference1Cor(c); // inférence du paramètre T avec capture
  // inference1((x == 0)? d : i); // échec de l'inférence de T
  inference1Cor((x == 0)? d : i); // inférence du paramètre T donnant Double
}

Lors de l'échec de l'inférence, le compilateur cherche un T vérifiant les inégalités suivantes, les types T1 et T2 représentant le joker, pour d et i respectivement, et appelés captures du joker par le compilateur.

A<T1> <= A<T> 
A<T2< <= A<T>

Par invariance des constructeurs génériques, on obtient T1 = T et T2 = T, ce qui impliquerait T1 = T2, qui est faux, T1 et T2 étant deux sur-types quelconques de Double. Il n'y a donc pas d'inférence possible. Dans l'interprétation ensembliste, on peut donner à l'expression ((x == 0)? d : i) le type AD union AD, soit AD, où AD = Union T tel que T >= Double.A<T>, et à la fonction inference1 le type Inter T.(A<T> -> void). On peut alors typer correctement inference1((x == 0)? d : i) : comme ((x == 0)? d : i) appartient à AD, il existe un type T1 tel que ((x == 0)? d : i) appartient à A<T1>, et inference1 appartient à (A<T1> -> void).

Cf. genericite.limitations.Alternative pour plus d'exemples. Attention : le compilateur incrémental d'Eclipse ne se comporte pas comme le compilateur javac en ligne de commande, et comporte donc des bugs (si l'on admet que javac se comporte correctement).

5.3.3 Sûreté de typage compromise

Il est possible de définir des unions dépendantes qui n'ont pas de sens.

class Min<T>{}
class Sup<A, B extends A> extends Min<B> {

  static <A, B> A convertir(B b) {
    Sup<A, ? super B> erreur = null; // X >= B, X <= A d'où B <= A
    ...
  }

La fonction convertir est définie pour tous types A et B. Le type Sup<A, ? super B> correspondant à une union des types Sup<A, X>, où X vérifie X >= B et par définition de Sup, X <= A. Ces deux contraintes impliquent que B <= A, une conclusion qui ne peut être déduite des hypothèses portant sur A et B. Le compilateur accepte cependant la définition de ce type, qui est habité par une valeur, null, et aucune autre.

Pour obtenir une erreur de type, il suffit de compléter la définition de la fonction convertir ainsi.

static <A, B> A convertir(B b) {
  Sup<A, ? super B> erreur = null; // X >= B, X <= A d'où B <= A
  return id(erreur, b); // inférence de T : T = X
}
static <T> T id(Min<T> c, T x){
  return x;
}

La fonction convertir réalise ainsi une conversion de B vers A, alors que A et B sont quelconques. On obtient une erreur en testant ainsi.

public static void main(String[] args) {
  String zero = convertir(0);
  System.out.println(zero); 
}
Exception in thread "main" java.lang.ClassCastException: 
  java.lang.Integer cannot be cast to java.lang.String

Cf. genericite.limitations.SureteTypage.

5.3.4 Bibliographie

Le système de types de Java est très imparfait en ce qui concerne la généricité, beaucoup plus en théorie qu'en pratique. Dans la pratique, on rencontre des limitations curieuses alors que dans la théorie, on est plutôt confronté à des fondations insuffisantes. De nombreux travaux de recherche lui sont consacrés : ils visent à dépasser les limitations et à proposer de solides fondations, permettant ainsi d'enrichir le système de types.

5.3.4.1 Java and Scala’s Type Systems are Unsound, de Nada Amin et Ross Tate

Sous-titre : The Existential Crisis of Null Pointers

(Papier dont est extrait le dernier exemple)

We present short programs that demonstrate the unsound- ness of Java and Scala’s current type systems. In particular, these programs provide parametrically polymorphic functions that can turn any type into any type without (down)casting. Fortunately, parametric polymorphism was not integrated into the Java Virtual Machine (JVM), so these examples do not demonstrate any unsoundness of the JVM. Nonetheless, we discuss broader implications of these findings on the field of programming languages.

Conférence OOPSLA de 2016

Cf. https://raw.githubusercontent.com/namin/unsound/master/doc/unsound-oopsla16.pdf.

5.3.4.2 Taming Wildcards in Java's Type System de Ross Tate, Alan Leung, and Sorin Lerner

(Papier dont sont extraits les exemples précédents)

Wildcards have become an important part of Java's type system since their introduction 7 years ago. Yet there are still many open problems with Java's wildcards. For example, there are no known sound and complete algorithms for subtyping (and consequently type checking) Java wildcards, and in fact subtyping is suspected to be undecidable because wildcards are a form of bounded existential types. Furthermore, some Java types with wildcards have no joins, making inference of type arguments for generic methods particularly difficult. Although there has been progress on these fronts, we have identified significant shortcomings of the current state of the art, along with new problems that have not been addressed.

In this paper, we illustrate how these shortcomings reflect the subtle complexity of the problem domain, and then present major improvements to the current algorithms for wildcards by making slight restrictions on the usage of wildcards. Our survey of existing Java programs suggests that realistic code should already satisfy our restrictions without any modifications. We present a simple algorithm for subtyping which is both sound and complete with our restrictions, an algorithm for lazily joining types with wildcards which addresses some of the shortcomings of prior work, and techniques for improving the Java type system as a whole. Lastly, we describe various extensions to wildcards that would be compatible with our algorithms.

Conférence PLDI de 2011

Cf. http://www.cs.cornell.edu/~ross/publications/tamewild/.

5.3.4.3 Java type inference is broken: can we fix it? de Daniel Smith et Robert Cartwright

Java 5, the most recent major update to the Java Programming Language, introduced a number of sophisticated features, including a major extension to the type system. While the technical details of these new features are complex, much of this complexity is hidden from the typical Java developer by an ambitious type inference mechanism. Unfortunately, the extensions to the Java 5 type system were so novel that their technical details had not yet been thoroughly investigated in the research literature. As a result, the Java 5 compiler includes a pragmatic but flawed type inference algorithm that is, by design, neither sound nor locally complete. The language specification points out that neither of these failures is catastrophic: the correctness of potentially-unsound results must be verified during type checking; and incompleteness can usually be worked around by manually providing the method type parameter bindings for a given call site.

This paper dissects the type inference algorithm of Java 5 and proposes a signficant revision that is sound and able to calculate correct results where the Java 5 algorithm fails. The new algorithm is locally complete with the exception of a difficult corner case. Moreover, the new algorithm demonstrates that several arbitrary restrictions in the Java type system—most notably the ban on lower-bounded type parameter declarations and the limited expressibility of intersection types—are unnecessary. We hope that this work will spur the evolution of a more coherent, more comprehensive generic type system for Java.

Conférence OOPSLA de 2008

Cf. http://www.cs.rice.edu/~javaplt/papers/oopsla2008.pdf.

Version history: v1: 2015-12-02; v2: 2016-11-04[update]; v3: 2016-11-16[*text, +type unsoundness].
Comments or questions: Send a mail.
The webpage content is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.