Best viewed in 24pt and full-screen

Typage polymorphe paramétrique

Nous avons proposé de substituer au polymorphisme générique le polymorphisme paramétrique [Louvet et Ridoux 96, Louvet 96]. Le polymorphisme ne vient plus de l'instanciation de schémas de type, mais du paramétrage de fonctions ou prédicats par des types. Selon ce point de vue, une fonction ou un prédicat polymorphe attend des paramètres de type qui lui indiquerons quels sont les types des autres arguments. Il faut donc prévoir des notations pour ce passage de paramètre de type et pour le type de ces objets qui acceptent des types en paramètre, et puisque Prolog est un langage d'ordre supérieur, une notation pour les fonctions qui acceptent des types en paramètre.

Nous présentons ces notations sur l'exemple de la fonction identité. La variante paramétrique de la fonction identité, Id, s'utilise en l'appliquant à un type puis à un terme : par exemple, ([Id int] 1729). L'application de type ([... ...]) et l'application de terme ((... ...)) consomment respectivement les paramètres de type et de terme. En première approximation, le type de Id pourrait être noté qui exprime bien que le premier paramètre est un type, mais ne dit pas que le paramètre suivant et le résultat ont précisément le type qui est passé en paramètre. La bonne notation utilise un quantificateur qui lie le paramètre de type dans les types qui en dépendent : . C'est la notation d'un type produit*. Enfin, une seconde construction d'abstraction, , permet de distinguer les deux sortes de paramètres formels. La définition de l'identité polymorphe paramétrique est donc Id = .

Cette forme de polymorphisme répond aux problèmes mentionnés plus haut. Premièrement, les types ne sont plus obligatoirement prénexes, et on peut donc amalgamer le typage du langage objet et celui du métalangage (quand ils sont compatibles bien sûr). Par exemple, le prédicat d'application d'une fonction polymorphe aux membres d'une paire peut s'écrire schématiquement comme suit.

type appliquer_à_paire VW( U(U->U) -> (paire V W) -> (paire V W) -> o ) .

appliquer_à_paire F (p G D) (p ([F ] G) ([F ] D)) .

Cet exemple montre aussi qu'il faut introduire des variables de type libres dans les clauses, et des quantifications de type pour les lier. Nous verrons à la section suivante en quoi cette écriture est schématique.

Deuxièmement, la condition de tête se trouve vidée de sa substance car il n'y a plus d'instanciation des types. Elle est satisfaite trivialement. Par exemple, le prédicat pred_ad_hoc peut s'écrire schématiquement comme suit.

type pred_ad_hoc A(A -> o) .

[pred_ad_hoc int] 1 .                   % Type de pred_ad_hoc : A(A -> o).

[pred_ad_hoc string] "1" .         % Type de pred_ad_hoc : A(A -> o).

Troisièmement, les types représentés durant l'exécution sont exactement des types paramétriques. Enfin, il n'y a plus de variable cachée et la transparence définitionnelle est restaurée.

Comme on peut le voir dans les exemples qui précèdent, des types peuvent être passés en paramètre et traités comme le sont les termes. On a souhaité maintenir une distinction en proposant une construction de «garde de type» qui permet de conditionner l'exécution de sous-buts par la vérification d'une propriété de typage. Un but gardé (garde ==> but) est équivalent à la conjonction (garde, but), mais spécifie aussi que la garde doit être vérifiée avant de tenter de prouver le but. Ainsi, une variante du prédicat pred_ad_hoc peut s'écrire de la façon suivante,

[pred_ad_hoc T] X :- ( T = int ==> X = 1 ; T = string ==> "1" ) .

au lieu de

[pred_ad_hoc T] X :- ( T = int , X = 1 ; T = string , "1" ) .

Le typage paramétrique introduit de nouvelles difficultés, les deux principales étant que le problème d'unification est encore plus difficile que celui des -termes simplement typés, et que la notation paramétrique, prise à la lettre, est beaucoup trop verbeuse pour être proposée à un programmeur. Nous n'avons pas encore de réponse formelle au problème de l'unification. La réponse empirique est que déjà les systèmes Prolog actuels calculent dans un domaine qui n'est plus celui des -termes simplement typés et qui tend vers un polymorphisme paramétrique. Les systèmes Prolog ne résolvent pas tous les problèmes d'unification qui leur sont posés : ils suspendent ceux qui sont trop difficiles jusqu'à ce qu'ils s'instancient en des problèmes moins difficiles. C'est une technique largement utilisée pour la programmation par contraintes. Par exemple, la contrainte ax+bxy+cy = 0, où a, b et c sont des constantes, et x et y sont des variables, est assez difficile à résoudre alors que son instanciation pour y constant est très facile.

La suspension de contrainte se produit déjà en Prolog pour deux raisons. D'abord, le semi-algorithme de Huet* qui est utilisé pour unifier les -termes retarde l'unification des paires flexible-flexible* jusqu'à ce qu'elles ne le soient plus [Huet 75]. Il n'est pas grave que des paires restent flexible-flexible jusqu'à la fin du calcul car ce qui est effectivement calculé est un préunificateur*. Ensuite, cet algorithme est défini pour des types simples purs (sans variables), et il est assez naturel de l'étendre au cas des types avec variable en appliquant la méthode de la suspension aux paires de termes dont les types ne sont pas assez connus.