Best viewed in 24pt and full-screen

Verbosité du typage polymorphe paramétrique

Nous avons apporté une réponse formelle à la verbosité de la notation sous la forme d'une procédure qui complète les notations de type manquantes [Louvet et Ridoux 96, Louvet 96]. Elle permet d'omettre la plupart des notations de type, pour les laisser reconstituer par un compilateur. L'intuition que l'inférence de type au second ordre n'est pas faisable semble contredire la possibilité de cette complétion. En effet, au second ordre, il n'y a pas de type principal, et après une longue période où on ne savait pas si le problème d'inférence était décidable [Leivant 83, Mitchell 84, Pierce et al. 89] Wells a prouvé que ce problème ne l'était pas [Wells 94]. En fait, la complétion proposée n'a pas pour but de résoudre complètement l'inférence de type au second ordre : comme en Prolog, les types des constantes et des prédicats doivent être donnés, et les -quantifications inférées sont toutes prénexes. Par exemple, partant des déclarations suivantes,

type p A -> B -> (paire A B) .

type appliquer_à_paire D(D->D) -> (paire A B) -> (paire A B) -> o .

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

la complétion reconstitue d'abord les manquants dans les déclarations de type,

type p AB( A -> B -> (paire A B) ) .

type appliquer_à_paire AB( D(D->D) -> (paire A B) -> (paire A B) -> o ) .

puis les applications de type dans les clauses,

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

et enfin les quantifications manquantes, en distinguant les quantifications de variables de terme, , et les quantifications de variables de type, .

TypeG TypeD D:TypeD G:TypeG F:D(D->D)
         ([appliquer_à_paire TypeG TypeD]
                  F
                  ([p TypeG TypeD] G D)
                  ([p TypeG TypeD]([F TypeG] G) ([F TypeD] D))) .

On peut constater que les variables de types qui décoraient les deux applications de la fonction F ont été dupliquées comme paramètres de appliquer_à_paire et p. C'est ce qui va permettre la propagation des informations de type jusqu'aux points que le programmeur a explicitement annoté dans le source du programme.

La procédure de complétion permet de convertir au polymorphisme paramétrique tous les programmes Prolog. Cependant, tous les programmes paramétriques ne sont pas accessibles par complétion d'un programme Prolog. Par exemple, le prédicat pred_ad_hoc n'a pas de version purement Prolog (avec condition de tête). En fait, les programmes qui implémentent du polymorphisme ad-hoc ne peuvent pas être atteints par complétion d'un programme Prolog vérifiant la condition de tête. Par exemple,

type plus A -> A -> A -> o .

type conc (list A) -> (list A) -> (list A) -> o .

[plus A] X Y Z :- ( A = int ==> Z = X + Y ; A = (list B) ==> conc X Y Z ) .

est complété en le programme suivant,

type plus A( A -> A -> A -> o ) .

type conc A( (list A) -> (list A) -> (list A) -> o ) .

A B X:AY:AZ:A [plus A] X Y Z :- ( A = int ==> [= A] Z (X + Y) ; A = (list B) ==> [conc B] X Y Z ) .

mais on ne peut pas se passer de mentionner les variables de type A et B dans la version abrégée du programme.