Ours & Hippy — le blogOurs & Hippyourshippy@huoc.orgtag:blog.huoc.org,2009:atom2010-03-01T23:29:26+01:00tag:blog.huoc.org,2009:bluestorm/6
Expression problem (2/3) : dualités somme/produit et fonctionnel/OO
2009-10-11T12:17:16+02:002010-03-01T23:29:26+01:00Gabriel Scherer (bluestorm)
<div class="Edito"><p>Après deux semaines d’absence, le blog reprend vie ! Mais ce n’est,
comme trop souvent, pas grâce à moi… mais ça devrait changer
bientôt… bref, acclamez le, il est de retour, pour tous les
enfants de la terre… chui fatigué moi… comment ça, ça se
voit ? :]
</p><p>—minh
</p></div><p>J’aime bien l’<em>expression problem</em>, mais il n’est pas particulièrement
utile dans la pratique logicielle de tous les jours : les langages
utilisés aujourd’hui ne permettent pas en général de le résoudre de
façon complètement satisfaisante, soit parce que leurs concepteurs ne
se sont même pas posés la question, soit parce qu’ils ont estimé que
quelque chose de plus statique mais de plus simple était
préférable. Car l’extensibilité à un prix, et les solutions sont
souvent compliquées ; certains langages en contiennent en fait d’assez
satisfaisante, mais elles ne sont pas au cœur du langage (car on
préfère se baser sur des choses sûres et éprouvées), et donc
relativement de seconde zone dans la pratique des programmeurs : il
faut privilégier la simplicité, donc sauf dans les cas où en
a <em>vraiment</em> besoin, on évite d’utiliser ces constructions plus
délicates.
</p><p>Ce qui est intéressant, c’est que ce probème est un très bon moyen de
voir les liens entre les langages fonctionnels et les langages
orientés objet. Il n’est pas spécifique à un seul paradigme, et les
différentes solutions révèlent des caractéristiques, à mon avis assez
profondes, des différents paradigmes. En deux mots, généralement les
langages fonctionnels facilitent l’ajout d’opérations au détriment de
l’extensibilité des données, et les langages à objets favorisent les
données plutôt que les opérations.
</p><div class="Navigation"><b>Sommaire</b>
<ul><li><a href="#produits">Produits d’opérations</a>
</li><li><a href="#caracteristiques_approche_produit">Caractéristiques de l’approche produit</a>
</li><li><a href="#motif_composite">POO et motifs de conception</a>
</li><li><a href="#motif_visiteur">Approche somme en POO</a>
</li></ul></div><h3>Produits d’opérations <a id="produits"></a>
</h3><p>On pourrait ne pas être tout à fait satisfait de la solution des types
sommes extensibles : il y a pas mal de code chiant et qui a l’air
inutile (on parle de code <i>boilerplate</i>). En effet :
</p><ul><li><p>tout ce qui concerne les expressions sans multiplication est
coiffé d’un constructeur supplémentaire. Ça passe mais si on fait
trois extensions de suite, trois couches de constructeurs, ça
commence à faire lourd ;
</p></li><li><p>pour la même raison, on ne peut pas réutiliser directement les
fonctions des types étendus pour manipuler des éléments de type
simple : si on a une fonction qui sait manipuler des nombres, des
sommes et des produits, on ne peut pas lui donner directement un
élément de <code>expr</code>, alors qu’elle saurait pourtant manipuler les
nombres et les sommes. C’est encore plus compliqué si on voulait
n’avoir que des nombres et des produits (pas de somme) sur une
partie du programme, puisqu’ils ne sont pas dans un type commun ;
il faudrait travailler sur <code>expr2</code> en lançant une erreur si on
tombe sur une somme, ce qui n’est pas très propre.
</p></li></ul><p>Je vous ai parlé de langages dans lesquels il était plus facile
d’étendre les données que les opérations, sans modifier le code
existant. Comment faire, et peut-on le faire en OCaml ? La réponse est
oui, mais cela demande un changement (assez radical) de point de vue.
</p><p>Actuellement, les programmes sont centrés autour des <em>données</em> : on
définit leur type, et on exprime ensuite, <i>a posteriori</i>, des
opérations comme des fonctions qui opèrent sur ce type : c’est aux
opérations de faire le travail de tripoter les données pour en
extraire un résultat.
</p><p>On peut voir la situation complètement différemment en se plaçant du
point de vue des <em>opérations</em> : on commence par définir les opérations
qui nous intéressent, on en fait un type. Ensuite on exprimera des
données qui feront le travail d’exploiter les opérations de leurs
composants pour produire leurs opérations.
</p><pre><code>type ops =
{ eval : int;
print : string }
</code></pre><p>Voici nos opérations : l’évaluation, dont le résultat est un entier,
et l’affichage.
</p><pre><code>let int n =
{ eval = n;
print = string_of_int n }
</code></pre><p>Voici une donnée. Citoyen de seconde zone ! C’est une fonction qui
construit les opérations <i>quivontbien</i>.
</p><pre><code>let add a b =
{ eval = a.eval + b.eval;
print = sprintf "(%s + %s)" a.print b.print }
</code></pre><p>Voici une autre donnée. C’est à elle de faire tout le travail, elle
utilise les opérations de ses composants pour construire ses
opérations à elle. Parce que sans opérations, une donnée n’est
rien. Vous remarquez que je l’ai ajoutée comme ça, sans rien modifier
d’existant.
</p><pre><code>let eval_test = (add (int 1) (int 2)).eval
</code></pre><p>Ça marche. Mais comme on est coquet :
</p><pre><code>let eval ops = ops.eval
let print ops = ops.print
let eval_test = eval (add (int 1) (int 2))
let print_test = print (add (int 1) (int 2))
</code></pre><p>Ça marche et, du point de vue de l’utilisateur, rien n’a changé.
</p><p>Maintenant, on essaie d’étendre nos opérations. On va rajouter
l’opération <code>rpn</code> (notation polonaise inversée) que je vous ai
brièvement présentée avec les types sommes simples.
</p><pre><code>type ops2 =
{ rpn : Buffer.t -> unit;
ops : ops }
</code></pre><p>On a une surcouche avec une opération de plus. Celle-ci a de
particulier qu’elle demande, pour produire son résultat, un
paramètre : un buffer dans lequel est insèrera son contenu. Le sucre
syntaxique (qui transforme l’accès à une donnée en fonction) nous rend
ici service puisqu’il cache ce détail :
</p><pre><code>let rpn ops2 =
let buf = Buffer.create 47 in
ops2.rpn buf;
Buffer.contents buf
</code></pre><p>Par contre, maintenant qu’on a changé le type des opérations, il faut
redéfinir les anciennes données pour supporter cette nouvelle
opération, et le sucre syntaxique correspondant aux opérations de
l’ancien type.
</p><pre><code>let int n =
{ rpn = (fun buf -> bprintf buf "%d " n);
ops = int n }
let add a b =
let rpn buf =
a.rpn buf; b.rpn buf;
bprintf buf "+ " in
{ rpn = rpn;
ops = add a.ops b.ops }
let eval ops2 = ops2.ops.eval
let print ops2 = ops2.ops.print
</code></pre><div class="Remarque"><p>Attention, on définit ici une nouvelle donnée <code>int</code> (pour le type
<code>ops2</code>) en utilisant l’ancienne donnée <code>int</code> (pour le type
<code>ops</code>) : ce n’est pas une définition récursive (absence du mot clé
<code>rec</code>).
</p></div><p>On peut encore étendre nos données et nos opérations, en rajoutant une
donnée <code>mul</code> pour la multiplication.
</p><pre><code>let mul a b =
let rpn buf =
a.rpn buf; b.rpn buf;
bprintf buf "*" in
{ rpn = rpn;
ops = { eval = a.ops.eval * b.ops.eval;
print = sprintf "(%s * %s)" a.ops.print b.ops.print } }
let rpn_test =
rpn (add (int 1) (mul (int 2) (int 3)))
</code></pre><h3>Caractéristiques de l’approche produit <a id="caracteristiques_approche_produit"></a>
</h3><p>On a donc l’extensibilité dans les deux dimensions, comme avec les
sommes ouvertes. Mais cette fois-ci, on n’a eu besoin que d’une seule
itération pour trouver quelque chose de satisfaisant, et c’est
relativement simple puisque ça ne demande pas de types paramétrés ni
même de traitement de la récursion : la définition des données de ce
problème est récursive, mais pas celle des opérations ! En changeant
de point de vue on l’attaque donc selon un angle plus simple. Cette
méthode a cependant deux défauts assez importants.
</p><p>D’abord, La définition des données est éparpillée un peu partout, et
chacune contient un peu d’information sur les opérations, ce qui rend
le code moins facile à suivre (surtout pour des opérations plus
complexes) : pour voir la définition d’une opération, il faut trouver
ses petits morceaux dans chaque définition de donnée, il n’y a pas de
vue d’ensemble.
</p><p>En réalité il y a un problème symétrique dans le cas des sommes : si
l’on considère l’ensemble des effets des opérations sur un cas
spécifique de notre structure comme un tout, on se retrouve à devoir
lire le code de chaque opérations pour y voir à chaque fois le
traitement du cas qui nous intéresse : « Je m’intéresse seulement aux
multiplications et pas aux additions : comment sont-elles évaluées ?
Comment sont-elles affichées ? » Et les opérations sont définies en
plusieurs endroits pour une même donnée, donc ça rend plus difficile
la vision d’ensemble sur un cas spécifique. On observe donc vraiment
les deux facettes d’une même pièce : il faut pouvoir prendre un point
de vue ou l’autre, car l’un pourra être plus adapté que l’autre dans
certaines situations.
</p><p>D’autre part, cette écriture des opérations en fonction des opérations
des composants ne marche bien que pour une certaine classe
d’opérateurs, les catamorphismes (c’est en gros leur definition :
opérateurs que l’on peut définir avec uniquement le résultat
d’opérations sur les composants directs de notre donnée). C’est une
classe plutôt générale mais certaines opérations n’en font pas partie.
</p><p>Typiquement, dans le cas d’arbres comme celui qui nous intéresse (les
expressions mathématiques forment un arbre dont les nombres sont les
feuilles, et les opérations les noeuds), le catamorphisme va favoriser
un mode de parcours de l’arbre en particulier (tu parcours chaque fils
de ton noeud séparément puis tu réunis les résultats) alors que
certains problèmes demandent des modes de parcours différents (par
exemple une fonction dont le résultat dépend à chaque fois du père et
du fils gauche, au lieu du fils gauche et du fils droit). On peut
toujours tout faire rentrer à la hache dans la pensée unique du
catamorphisme (qui est assez naturel donc très courant), mais dans
certains cas ça donne des codes illisibles.
</p><p>Dans ce cas, la meilleure solution, au lieu de chercher à accéder
intelligemment aux résultats des fils dans le bon ordre, et de mettre
une machinerie complexe pour faire passer les résultats dans tous les
sens, est souvent de :
</p><ul><li>reconstruire l’« arbre » correspondant à la donnée, qui est
l’information la plus générale que l’on puisse obtenir, et dont
la construction s’exprime comme un catamorphisme ;
</li><li>implémenter l’opération à partir de l’arbre, dans un style plus direct.
</li></ul><p>Le problème est alors : quel type donner à l’arbre ? On se retrouve en
fait à définir un type somme, et c’est donc le retour à la case
départ : si notre type somme n’est pas extensible, les opérations qui
l’utilisent ne le seront pas non plus. Si on veut garder
l’extensibilité par les produits d’opérations, il faut donc sacrifier
de la facilité à programmer.
</p><h3>POO et motifs de conception <a id="motif_composite"></a>
</h3><p>Vous l’aurez peut-être remarqué en lisant ma dernière partie, mais
elle est en fait très proche de certaines idées de la
POO. L’insistance en particulier sur le fait que les opérations
(« méthodes ») font parties du type que l’on définit, au point d’en
faire l’élément le plus important du programme. Comme on l’a vu, cela
a selon les besoins des avantages, mais aussi des inconvénients.
</p><p>Dans un langage plus POO, la structure que j’ai mise en place dans la
dernière partie correspond au motif <strong>Composite</strong>. Dans ce motif, on
définit une interface qui décrit les opérations, puis une classe pour
chaque donnée :
</p><pre><code>class type expr = object
method eval : int
method print : string
end
class int n : expr = object
method eval = n
method print = string_of_int n
end
class add a b : expr = object
method eval = a#eval + b#eval
method print = sprintf "(%s + %s)" a#print b#print
end
let test = (new add (new int 1) (new int 2))#eval
</code></pre><p>On peut remarquer que les langages OO aussi auront bien besoin de
sucre syntaxique pour alléger un peu tout ça. Par contre, là où une
solution objet est intéressante par rapport à notre solution à base
d’enregistrements, c’est qu’on peut étendre les opérations avec le
mécanisme d’<em>héritage</em> :
</p><pre><code>class type expr2 = object
inherit expr
method rpn : Buffer.t -> string
end
</code></pre><p>On peut alors appeler directement les méthodes <code>eval</code> et <code>print</code> sur
des objets vérifiant l’interface <code>expr2</code>, sans devoir passer par une
couche d’indirection (le <code>.ops</code> de la solution produit). De notre
point de vue c’est presque un détail syntaxique, et la première
méthode a aussi ses mérites puisqu’elle correspond à la relation de
<em>composition</em> qui est souvent considérée par les programmeurs POO
comme plus adaptée que l’héritage dans un grand nombre de cas.
</p><h3>Approche somme en POO <a id="motif_visiteur"></a>
</h3><p>J’ai présenté cette vision POO du problème, qui correspond au motif
<em>Composite</em>. C’est la méthode la plus naturelle pour un programmeur OO
(qui est donc sans le savoir un descendant de la solution produit),
mais il est aussi possible d’effectuer un changement radical de point
de vue, dans le but de retrouver une approche avec des sommes. Ça
correspond au motif <strong>Visiteur</strong> : au lieu de mettre les <em>opérations</em>
dans les méthodes, on met les <em>données</em>.
</p><p>L’idée est la suivante : on imagine chaque donnée comme un <em>lieu</em> que
l’on peut visiter ; chaque donnée est chargée de coder une fonction
<code>accept</code> qui appelle une méthode adaptée du visiteur :
</p><pre><code>let int n = object
method accept visitor = visitor#int n
end
let add a b = object
method accept visitor = visitor#add a b
end
</code></pre><p>Ces fonctions <code>accept</code> prennent des visiteurs en argument, et leurs
donnent leurs composants. Chaque opérateur est un visiteur :
</p><pre><code>let eval = object (self)
method int n = n
method add a b = a#accept self + b#accept self
end
let test_eval =
let expr = add (int 1) (int 2) in
expr#accept eval
</code></pre><p>Cette solution est donc l’analogue OO des types sommes; on peut de
plus profiter de la "récursion ouverte" des objets pour obtenir
l’analogue de la "somme ouverte" : pas besoin de paramétrer les objets
de départ pour les enrichir ensuite, le mécanisme d’héritage
suffit. Elle est cependant beaucoup plus difficile à typer (c’est
pourquoi elle est plus souvent utilisée dans des langages à typage
dynamique qui ne se posent pas la question).
</p>
tag:blog.huoc.org,2009:bluestorm/4
Singeries appliquées en OCaml : Polymorphisme d'ordre supérieur (2/2)
2009-09-09T06:58:17+02:002010-03-01T23:29:26+01:00Gabriel Scherer (bluestorm)
<div class="Edito"><p>Après le boudin, les restes. bluestorm nous offre ici une collection
de petits détails alléchants pour certains, sans goût ni odeur pour
d’autres, mais qui viendront en tout cas accompagner, étendre et
embellir sa précédente composition (à laquelle ma présence
a semble-t-il cruellement manqué), en mettant l’accent sur des
aspects divers, et divers aspects : bref, à parler pour ne rien dire,
j’y perds mon inspiration, moi…
</p><p>–minh
</p></div><p>Comme promis, voici la suite, et fin, de mon billet précédent :
<a href="http://blog.huoc.org/./2-macaque_polymorphisme_superieur.html">Singeries appliquées en OCaml : Polymorphisme d’ordre supérieur
(1/2)</a>. Contrairement à ce que j’avais dit, je ne parlerai
pas de la restriction syntaxique sur le polymorphisme explicite : j’ai
remplacé cette partie par une rapide présentation d’une publication
(<i>paper</i>) qui est à l’origine de l’introduction de ce polymorphisme
d’ordre supérieur dans le langage OCaml.
</p><div class="Navigation"><b>Sommaire</b>
<ul><li><a href="#exemple_poo">Autre utilisation du procédé</a>
</li><li><a href="#lexique">Pourquoi dit-on « ordre supérieur »</a>
</li><li><a href="#evasion">Évasion du ’parser’ universel et perennité de la méthode</a>
</li><li><a href="#publication">Une publication à se mettre sous la dent</a>
</li></ul></div><h3>Autre utilisation du procédé <a id="exemple_poo"></a>
</h3><p>Un autre exemple pour enfoncer le clou en vous montrant encore de
petits exemples de polymorphisme d’ordre supérieur. Il n’est pas tiré
de Macaque, et c’est de l’orienté objet. On veut écrire une classe de
« collections », qui proposent l’interface suivante :
</p><ul><li><p>ajouter un objet à la collection ;
</p></li><li><p>aggréger la collection, c’est à dire calculer une valeur en prenant
en compte l’ensemble des éléments : on prend en paramètre une
fonction à qui on donne la liste des éléments de la collection,
pour faire son calcul.
</p></li></ul><p>Le type de la collection dépend du type de ses éléments : on va avoir
des <code>int collection</code>, etc. On commence donc par le code suivant :
</p><pre><code>class ['a] collection = object
val mem = []
method add (x : 'a) = {< mem = x :: mem >}
method aggregate : ('a list -> 'c) -> 'c =
fun f -> f mem
end
</code></pre><p>Mais ça ne marche pas : <code>The method aggregate has type ('a list ->
'c) -> 'c where 'c is unbound</code>. Le problème ici c’est que <code>'c</code> n’est
pas un paramètre de type spécifique à la méthode : c’est l’objet qui
dans son ensemble a le type
</p><pre><code>< add : ...; aggregate : ('a list -> 'c) -> 'c >
</code></pre><p>Implicitement, le quantificateur sur le type <code>'c</code> est placé au début du
type de l’objet, donc c’est un paramètre global à la classe, et OCaml
se plaint qu’on ne l’ait pas renseigné dans les paramètres de la
classe. On pourrait effectivement dire <code>class ['a, 'c] collection =
..</code>, mais c’est un peu idiot : on aura les collections d’entiers qui
peuvent calculer des booléens, et les collections d’entiers qui
peuvent calculer des flottants, et ce seraient des types différents ?
La « bonne » solution, pour ne pas laisser le paramètre <code>'c</code> s’échapper,
est d’utiliser le polymorphisme d’ordre supérieur :
</p><pre><code>method aggregate : 'c . ('a list -> 'c) -> 'c = ...
</code></pre><p>Ainsi, on a replacé le quantificateur au bon endroit : au début du
type de la méthode <code>aggregate</code>. Le compilateur est content et on peut
utiliser <code>aggregate</code>, au sein d’un même objet, avec des types de retour
différents.
</p><h3>Pourquoi dit-on « ordre supérieur » ? <a id="lexique"></a>
</h3><p>On parle de « polymorphisme d’ordre supérieur » par opposition à la
pratique dans le typage ML classique, qui est du « polymorphisme de
premier ordre » : grosso modo, on compte l’ordre en fonction du nombre
de couches de quantificateurs imbriquées. Dans les types habituels,
sans quantificateurs explicites, on considère qu’ils sont tous placés
au début du type, donc il n’y a qu’un seul niveau, c’est le premier
ordre. <code>type t = (∀ 'b. (∀ 'a . 'a -> 'b) -> 'b)</code> est un type du
second ordre, et <code>(∀ 'c . (t -> 'c) -> t -> 'c)</code> du troisième (à cause
des quantificateurs implicites de <code>t</code>).
</p><p>Avec la possibilité de mettre des quantificateurs dans les records, on
peut en fait mettre autant de couches qu’on veut, donc c’est
« à l’ordre qu’on veut ». On parle alors d’<em>ordre supérieur</em>.
</p><p>Le concept d’<em>ordre</em> revient souvent quand on essaie de décrire la
puissance expressive d’un système. Ici on parle de l’ordre du
polymorphisme (des types), mais il y a aussi un concept d’ordre des
fonctions : dans certains langages, les fonctions ne peuvent prendre
en paramètre et renvoyer comme valeur de retour que des types de base,
non fonctionnels, du langage (entiers, flottants, tableaux,
structures, etc..). Ce sont des fonctions de premier ordre. Il
y a aussi des langages qui peuvent prendre en paramètre des types de
base, ou des fonctions du premier ordre (qui ne prennent que des types
de base) : c’est le deuxième ordre. On peut imaginer un troisième,
quatrième ordre, etc., mais en pratique les langages sont souvent
conçus pour déclarer des fonctions d’« ordre supérieur » : les
fonctions peuvent prendre en paramètre et retourner des fonctions de
n’importe quel type (des fonctions de fonctions de fonctions de … de
fonctions des types de base).
</p><h3>Évasion du <i>parser</i> universel et perennité de la méthode <a id="evasion"></a>
</h3><p>J’ai expliqué qu’un des intérêts de demander une fonction qui dépend
du <i>parser</i> universel, plutôt que de divulger le <i>parser</i> universel
dans l’interface de Macaque, était de le « cacher »
à l’utilisateur. En fait ce secret est purement stylistique (« c’est
pas dans l’interface donc tu touches pas ») et n’augmente pas la
« sécurité » (commme si l’utilisateur était un délinquant) de
l’interface. En effet :
</p><pre><code>let pirate : univ_parser =
let captured_parser = ref None in
let fake_builder = fun prey_parser ->
captured_parser := Some (prey_parser);
object (* fake table object *) end
in ignore (Sql.table (* ... *) fake_builder);
match !captured_parser with
| None -> failwith « failed to capture the flag! »
| Some univ_parser -> univ_parser
</code></pre><p>Démoniaque non ? On fait semblant de vouloir construire une table,
dans la fonction, au moment où il nous donne le <i>parser</i>, on le
capture en le mettant dans une référence qu’on avait déclarée au
préalable. Cette technique ne marche que si l’implémentation de
Sql.table utilise vraiment la fonction pour obtenir le parser, en lui
donnant vraiment le <i>parser</i> universel en paramètre, mais à priori
c’est ce qu’elle fait (sinon elle n’aurait pas accès au parser et il
faudrait tout recommencer).
</p><p>Cette astuce repose sur la présence d’un effet de bord qui permet au
paramètre de <em>s’évader</em> hors de la fonction, sans passer par la valeur
de retour. Elle pose aussi problème quand on veut implémenter des
fonctions du style <code>with_open_file : (input_channel -> 'a) -> 'a</code>. On
n’aurait pas ce problème dans un langage pur, qui empêche totalement
les effets de bords (ce n’est pas le cas en Haskell qui
a <code>unsafePerformIO</code>), mais pour l’instant les restrictions que ça
apportent sont énormes, ça ne vaut tout simplement pas le coup de
faire ça dans le seul but de pouvoir garantir qu’aucune variable ne se
sauve. On peut aussi s’en sortir avec un système de typage plus
expressif (closure & effect typing), il y a des systèmes expérimentaux
qui font ça (par exemple le langage Discipline lié à Haskell), mais
encore une fois ils sont bien trop lourds à l’utilisation pour que
leur coût soit compensé par leurs bénéfices dans la grande majorité
des situations (où la sûreté est importante, mais la productivité du
programmeur l’est encore plus).
</p><table><tr><td></td></tr></table><p>Je tiens aussi à vous donner, en toute honnêteté, la nouvelle la plus
triste du billet : le type <code>univ_parser</code> est décédé. Quelques temps
après sa naissance, j’ai rajouté des fonctionnalités, ce qui a induit
de nouveaux besoins, et quand j’ai refactorisé, je me suis retrouvé
à devoir publier le <i>parser</i> universel dans l’interface, et ai donc
supprimé le type spécifique. C’est triste, mais c’est la vie : quand
on code il faut parfois, souvent même, supprimer des choses qu’on
a faites avec, même si on les trouve tout à fait intéressantes. Du
reste, une valeur de type <code>('a sql_type -> 'a parser)</code> dans mon
interface est toujours plus simple à comprendre pour les gens qu’un
polymorphisme d’ordre supérieur, donc ce n’est pas forcément une perte
pour la lisibilité de mon programme.
</p><h3>Une publication à se mettre sous la dent <a id="publication"></a>
</h3><p>Ce billet n’est pas une réaction, mais il me paraît tout de même
pertinent de citer l’article des gens qui ont mis en place le
polymorphisme d’ordre supérieur en Caml : <a class="extern" href="ftp://ftp.inria.fr/INRIA/Projects/cristal/Didier.Remy/iandc.ps.gz">Extending ML with
Semi-Explicit Higher-Order Polymorphism (.ps.gz)</a>, par Jacques
Garrigue et Didier Rémy.
</p><p>Le papier est, dans sa plus grande partie, trop technique pour moi,
mais si vous avez envie d’essayer, voilà l’histoire en deux mots. Les
auteurs étudient des compromis entre le système de typage ML
(polymorphisme de premier ordre seulement, mais inférence des types)
et le <a class="extern" href="http://en.wikipedia.org/wiki/System_F">Système F</a> (polymorphisme d’ordre supérieur,<sup>א</sup>
pas d’inférence de types).
</p><div class="Notes"><p>א : le concept d’ordre revient à la charge : je parle du Système F2,
qui propose le polymorphisme d’ordre supérieur, mais donc les
<i>kinds</i> (un niveau supplémentaire de typage) sont d’ordre 2. Il
existe aussi un système F d’ordre supérieur, Fω.
</p></div><p>Le système F est un langage plus expressif que ML, mais aussi
nettement plus lourd à utiliser (syntaxiquement). En particulier, le
polymorphisme y est introduit et appliqué explicitement : quand on
veut écrire un terme polymorphe, on écrit un terme qui « prend un type
en paramètre », et quand on veut l’utiliser on lui « applique » le
type particulier avec lequel on l’utilise. On note par exemple
<code>Λα. λx:α. x</code> la fonction identité (on prend un type <code>α</code> en paramètre,
puis une variable <code>x</code> de type <code>α</code>, et on renvoie <code>x</code>), et si <code>t</code> est
de type <code>τ</code>, on écrira <code>id τ t</code> pour l’identité de <code>t</code> : on commence
par donner à la fonction le type du paramètre, puis le paramètre
lui-même.
</p><p>Les gens<sup>ב</sup> qui ont travaillé sur l’ajout de polymorphisme d’ordre
supérieur à ML se sont en général inspirés de l’approche Système
F. L’originalité de la publication de Garrigue et Rémy, c’est qu’ils
demandent des annotations explicites pour l’introduction de
polymorphisme d’ordre supérieur (la syntaxe <code>'a . foo</code> est équivalente
au <code>Λα . foo</code>), mais pas pour son utilisation.
</p><div class="Notes"><p>ב : Parmis ces joyeux lurons se trouve Odersky, qui travaillait sur
ces choses-là dans les années 90, et qui est maintenant connu comme
le principal auteur du langage <i>Scala</i>.
</p></div><p>Je ne parlerai presque pas de l’article, mais quand même une
remarque : pour avoir un système qui ne fait pas de choses étranges,
les auteurs de l’article décident de respecter le polymorphisme
indiqué par les annotations des programmeurs, mais de ne pas laisser
le système en ajouter lui-même; ils utilisent pour cela un système
basé sur (encore une fois) le polymorphisme, qu’on peut considérer
comme l’équivalent en théorie des types d’un <em>joli hack</em>.
</p>