On appelle surcharge (overloading en anglais) le fait d'utiliser un
même nom ou une même notation pour désigner des fonctions différentes.
La surcharge est tellement usuelle en mathématiques qu'on aurait presque
tendance à l'oublier. Par exemple, x + y a un sens différent selon que
x et y soient des entiers, des vecteurs, des matrices, des fonctions, etc.
La plupart des langages de programmation ont suivi cette présentation.
Ainsi, dans le langage C, on peut écrire a + b pour
additioner des entiers ou des flottants.
Certains langages vont au-delà des opérateurs de prédéfinis.
C'est le cas en C++, où l'on peut écrire t[i] pour accéder au i-ème élément
de n'importe quelle structure de données : l'opérateur crochet peut
être librement défini par l'utilisateur pour chaque type.
Ce principe s'applique également pour des fonctions nommées, par exemple
t.size() appelle la fonction size associée au type de la
structure t, sans faire référence au nom de la structure de donnée
en écrivant array::size ou bien Array.size, selon la syntaxe.
La surcharge apparaît aussi pour l'accès au champ des records,
par exemple r.x permet d'accéder au champ x, qui peut avoir
des types différents selon le type du record r.
Dans un langage fonctionnel, la surchage serait de plus utile pour pouvoir
utiliser le même nom de constructeur dans différents types inductifs vivant dans
le même scope.
Le problème de la surcharge apparaît en Coq non seulement lorsqu'on écrit
des programmes, mais encore davantage lorsqu'on formalise des mathématiques.
En effet, l'écriture d'expressions mathématiques sans surcharge aboutit très
rapidement à des formules illisibles en pratique par un humain. Dans le
cadre d'un système interactif, le problème est encore plus important au
moment de l'écriture parce
l'utilisateur doit retrouver une notation peu naturelle pour une opération
qu'il aurait naturellement écrite avec une notation surchagée. Par exemple,
on peut décider d'utiliser *: au lieu de * pour la
multiplication d'un vecteur par un scalaire, mais l'utilisateur doit retrouver
ce symbole *: qui est difficile à mémoriser.
En Coq, le mécanisme des typeclasses ou des canonical structures permet, dans une certaine mesure,
de bénéficier de surcharge. Avec ce mécanisme, l'addition de deux entiers
a + b s'élabore vers l'expression plus Z plus_inst_Z a b, où
Z est le type des entiers, et plus_inst_Z est l'instance
qui enregistre le fait que l'opérateur d'addition sur les entiers est Z.add.
Pour faire court, là où l'on s'attendrait naïvement à ce que l'expression
a + b soit une notation pour le terme Z.add a b,
celle-ci s'élabore en réalité vers le terme plus Z plus_inst_Z a b.
Ce dernier terme est équivalent (convertible) avec Z.add a b, mais il n'est
pas syntaxiquement égal. Ce décalage est un obstacle important
pour des opérations de réécriture, en particulier.
En résumé, il y aurait énormément de bénéfices à pouvoir bénéficier d'un mécanisme
de surcharge en Coq. Le mécanisme de surchage proposé par C++
donne des pistes, mais il n'explique pas comment gérer les constantes
(déterminer le type d'un symbole comme zéro ou l'ensemble vide),
et n'explique pas comment faire interagir la résolution de la surcharge
avec l'inférence de types réalisée par un algorithme d'unification.
En particulier, il y a des difficultés pour traiter correctement les
appels à des fonctions d'ordre supérieur.
Des algorithmes de résolution de la surcharge basés sur du typage bidirectionnel
ont été proposés dans le langage ADA ainsi que dans le prouveur PVS, et ont
démontré leur passage à l'échelle industrielle.
Ils fournissent des pistes intéressantes, néanmoins ces systèmes ne traitent
pas le cas des fonctions polymorphes, ni des types dépendants.
L'objectif de notre travail est de spécifier les détails et d'implémenter un algorithme de typage bidirectionnel qui soit capable de résoudre la surchage de manière :
On portera par ailleurs un soin particulier à produire des messages d'erreurs compréhensibles et informatifs dans les cas où l'algorithme de résolution de la surcharge rejette le terme fourni.