Historiquement,
le système de Mycroft et O'Keefe
[Mycroft et O'Keefe 84]
implémente la première discipline de type prescriptif pour Prolog.
C'est une transposition de la discipline de
[Milner 78] à Prolog.
Leur proposition a soulevé quelques interrogations
[Hanus 89a, Hanus 89b, Hanus 91]
et a abouti à la définition d'un Prolog typé,
Typed Prolog [Lakshman et Reddy 91].
Le système Gödel [Hill et Topor 92, Hill et Lloyd 94]
met aussi en 
uvre cette discipline.
À notre connaissance,
Typed Prolog n'a pas été implémenté ni diffusé.
Gödel, 
Prolog et, depuis peu, Mercury [Somogyi et al. 96]
sont probablement les seuls
langages de programmation logique typés prescriptivement
à avoir été implémentés en vraie grandeur
et avoir été utilisés relativement largement.
On peut donc déjà tirer quelques enseignements de ces expériences.
Le système de type de Mycroft et O'Keefe a été aussi implémenté
sous la forme d'un outil de vérification de programmes.
Cependant,
l'usage de cet outil reste optionnel.
Cela ne confronte pas le programmeur à l'obligation de ne produire que des
programmes bien typés.
Le point positif,
prévisible,
est que beaucoup d'erreurs sont découvertes dès la compilation.
Elles vont de l'oubli ou la permutation de paramètres à la faute de frappe.
De plus, en cas de type non déclaré,
le système 
propose un type dans le message d'erreur.
Cela signifie que même si nous avons souhaité ne pas fonder la notion
de programme bien typé sur l'inférence de type,
le système
l'utilise opérationnellement comme un mécanisme d'assistance au programmeur.
Le point négatif vient de ce que la discipline de type mise en uvre
est parfois trop rigide et interdit certaines pratiques bien établies en
programmation logique.
Nous pensons que certaines de ces pratiques sont nuisibles,
et que le typage ne fait que le révéler.
Par exemple,
le typage de interdit d'utiliser un symbole avec des
arités* différentes.
Nous pensons que c'est une bonne chose car permettre cet usage empêche de
détecter les omissions de paramètre.
La confusion entre le contenant et le contenu
(par exemple, liste et élément)
est aussi fréquente et reconnue nuisible [O'Keefe 90].
Par exemple,
considérons le prédicat qui relie un arbre binaire et la liste de ses feuilles.
C'est un classique où les deux premières
clauses ont pour premier argument une liste d'éléments,
alors que la troisième a pour premier argument un élément.
aplatir [] [] :- ! .
aplatir [L1 | L2] F3 :- ! , aplatir L1 F1 , aplatir L2 F2 , conc F1 F2 F3 .
aplatir E [E] .
La version bien typée de ce prédicat est la suivante :
kind arbre2 type -> type .
type feuille F -> (arbre2 F) .
type n
type aplatir (arbre2 F) -> (list F) -> o .
aplatir (feuille F) [F] .
aplatir (nud (arbre2 F) -> (arbre2 F) -> (arbre2 F) .
ud G D) Fs :-
aplatir G FG , aplatir D FD , conc FG FD Fs .
Il faut noter que même reconnu nuisible par certains, ce genre de pratique abonde dans la littérature, et la position qui consiste à défendre une discipline de typage (donc de programmation) contre la pratique courante n'est pas confortable.
Il subsiste d'authentiques points négatifs
dont certains ont trait à la métaprogrammation*.
Ici,
la difficulté est que même si les formules et les termes de Prolog
sont bien adaptés à la métaprogrammation,
les types de Prolog ne le sont pas complètement.
Un des enjeux de la métaprogrammation est de sous-traiter à la machine
du métalangage des
opérations du niveau objet quand langage objet et métalangage sont proches.
Par exemple,
si on a des langages de programmation logique aux deux niveaux,
il est intéressant de sous-traiter l'unification des termes objet
à la procédure du métalangage,
et c'est quelque chose qui se fait très bien
(voir le vanilla interpreter* [Sterling et Shapiro 90]).
De façon similaire,
on voudrait que le typage des termes objet soit sous-traité au méta-langage
(seulement s'il est compatible, évidemment).
Il se trouve que la discipline de type de Prolog est trop faible pour pouvoir
faire cela avec les types polymorphes.
On voudrait appliquer au typage des termes objet la discipline du
métalangage (ici, Prolog),
de telle sorte qu'un terme objet est bien typé si et seulement si
le métaterme qui le représente l'est aussi.
Cela marche assez bien, sauf pour le polymorphisme.
Par exemple,
essayons d'appliquer aux deux membres d'une paire polymorphe une fonction
polymorphe inconnue mais qui sera le résultat d'un calcul
(c'est-à-dire une fonction objet).
kind paire type -> type -> type .
type p A -> B -> (paire A B) .
type appliquer_à_paire (U -> U) -> (paire V W) -> (paire V W) -> o .
appliquer_à_paire F (p G D) (p (F G) (F D)) .
Ce programme ne répond pas à notre besoin car le typage générique force les trois types inconnus, U, V et W, à être égaux. Pour cette application, le type inconnu U ne devrait pas être traité comme le sont V et W. On voudrait pouvoir prendre une instance nouvelle de son type pour chaque application de la fonction F. Ce n'est pas possible lorsque le polymorphisme est représenté par des formules uniquement prénexes* : durant l'exécution, le type d'un terme ne peut donc être qu'une instance monomorphe d'un type polymorphe, mais jamais un type polymorphe.
Le problème posé peut sembler très spécifique et ne mériter
qu'une réponse locale.
En fait,
il est assez général et le programmeur Prolog fait souvent de
la métaprogrammation sans le savoir.
Il faut se rappeler aussi le sens assez large que nous avons donné
à métaprogrammation.
On peut se demander alors pourquoi ce problème n'est pas aussi apparu
dans un autre langage polymorphe générique comme .
En fait,
il est apparu [Dubois et al. 95]
mais peut être pas avec la même acuité pour
une raison qui semble en partie culturelle.
Il n'y a pas en
d'opérations génériques que l'on voudrait réutiliser au niveau objet,
alors que la programmation logique utilise depuis ses débuts des
opérations génériques comme l'unification, la comparaison de termes,
la décomposition de terme (prédicat =.., alias univ), etc.
Une autre difficulté est le statut de la condition de tête*. Celle-ci précise que non seulement chacune des clauses doit obéir à la discipline de typage générique,
toutes les occurrences d'une même variable ont le même type et toutes les occurrences d'une même constante ont des types qui sont des instances indépendantes d'un même type polymorphe,
mais aussi que les clauses d'un même prédicat doivent «s'accorder»,
les constantes prédicatives en tête des clauses d'un même prédicat doivent avoir les mêmes types.
Par exemple, la condition de tête fait que le prédicat suivant est mal typé.
type pred_ad_hoc A -> o .
pred_ad_hoc 1 . % Type de pred_ad_hoc : int -> o.
pred_ad_hoc "1" . % Type de pred_ad_hoc : string -> o.
Cette condition a été exhibée pour répondre à des
questions de correction sémantique du typage et d'inférence de type.
Un programme bien typé qui satisfait la condition est sémantiquement correct,
c'est-à-dire qu'il ne causera pas d'erreur de type durant l'exécution.
En revanche,
l'inférence de type polymorphe est indécidable en présence de cette condition.
Il faut le savoir,
mais ce n'est pas une limitation très grave car on peut
spécialiser un peu le problème pour le rendre
décidable [Lakshman et Reddy 91].
Ce qui est plus grave est que
la condition de tête interdit quasiment le polymorphisme ad hoc.
On ne peut retrouver le polymorphisme ad hoc qu'au prix de tolérer
des constructeurs qui ne sont pas transparents* :
des constructeurs dont le type contient des variables qui n'apparaissent
pas dans le type du résultat.
Par exemple
cons : 
est transparent,
mais
f : 
ne l'est pas.
On remarque qu'aucun constructeur de prédicat polymorphe n'est transparent.
Ils ont tous un type de la forme 
.
Ce faisceau de circonstances un peu contradictoires fait qu'il n'y a pas
de consensus sur l'adoption de la condition de tête.
Nous l'avons adoptée dans
parce qu'elle permet la
compilation et la vérification de type séparées,
tout en sachant qu'elle contribue à aggraver la rigidité du typage,
contrairement aux autres implémentations de Prolog qui ne l'adoptent
pas [Nadathur et Pfenning 92].
Il faut noter que,
dans leurs premiers articles sur Prolog,
Miller et Nadathur ne se prononcent pas sur cette
condition [Nadathur 87].
La correction sémantique* est la propriété d'un système de vérification de type qui est tel qu'aucun programme bien typé selon ce système ne peut causer d'erreur de type à l'exécution (en anglais, «Well-typed programs cannot go wrong» [Milner 78]).
L'intérêt de la correction sémantique et qu'elle permet de ne plus représenter
de types durant l'exécution car leur correction peut être établie dès la
compilation.
Cependant,
on peut avoir d'autres raisons de représenter les types que pour les vérifier.
En Prolog,
l'opération de
projection* les utilise pour sélectionner
les arguments à projeter.
Cela signifie que même quand la correction sémantique est établie,
il faut représenter suffisamment de type pour contrôler la projection.
Notre implémentation représente donc des types durant l'exécution,
mais pas tous loin s'en
faut [Brisset 92, Brisset et Ridoux 92b, Brisset et Ridoux 94].
Le polymorphisme générique n'éclaire pas tellement le statut
de ces types représentés durant l'exécution.
Ils apparaissent comme paramètres cachés des termes et des prédicats,
ils subissent l'unification comme les termes,
mais contrôlent aussi l'unification des termes.
Ils peuvent en particulier se propager par substitution et
empêcher l'unification de deux termes sans que la syntaxe ne le laisse prévoir.
Un dernier point est que le polymorphisme générique fait perdre la propriété de transparence définitionnelle. Dans le contexte de la programmation logique, être transparent définitionnellement signifie que l'on peut toujours remplacer un terme par une variable en ajoutant la contrainte que cette variable est égale à ce terme. C'est la base d'une forme normale des programmes utilisée pour les compiler, les analyser, ou calculer la complétion de Clark [Clark 78] des programmes avec négation.
Par exemple, une clause
... :- ... , (p ... t ...) , ... , (q ... t ...) , ... .
peut être transformée en
... :- ... , X = t , (p ... X ...) , ... , (q ... X ...) , ... .
Les types des deux occurrences de t peuvent être différents, alors que les types des deux occurrences d'utilisation de X ne peuvent qu'être égaux. Le polymorphisme générique introduit des variables cachées (les variables de type) qui empêchent d'appliquer les transformations habituelles.
La discipline de typage polymorphe générique inspirée de ne nous
semble donc pas complètement adaptée à Prolog et Prolog.