Ours & Hippy — le blog Ours & Hippy ourshippy@huoc.org tag:blog.huoc.org,2009:atom 2010-03-01T23:29:26+01:00 tag:blog.huoc.org,2009:bluestorm/6 Expression problem (2/3) : dualités somme/produit et fonctionnel/OO 2009-10-11T12:17:16+02:00 2010-03-01T23:29:26+01:00 Gabriel 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 &quot;(%s + %s)&quot; 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 -&gt; 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 -&gt; bprintf buf &quot;%d &quot; n); ops = int n } let add a b = let rpn buf = a.rpn buf; b.rpn buf; bprintf buf &quot;+ &quot; 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 &quot;*&quot; in { rpn = rpn; ops = { eval = a.ops.eval * b.ops.eval; print = sprintf &quot;(%s * %s)&quot; 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 &quot;(%s + %s)&quot; 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 -&gt; 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 &quot;récursion ouverte&quot; des objets pour obtenir l’analogue de la &quot;somme ouverte&quot; : 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:00 2010-03-01T23:29:26+01:00 Gabriel 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) = {&lt; mem = x :: mem &gt;} method aggregate : ('a list -&gt; 'c) -&gt; 'c = fun f -&gt; f mem end </code></pre><p>Mais ça ne marche pas : <code>The method aggregate has type ('a list -&gt; 'c) -&gt; '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>&lt; add : ...; aggregate : ('a list -&gt; 'c) -&gt; 'c &gt; </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 -&gt; 'c) -&gt; '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 -&gt; 'b) -&gt; 'b)</code> est un type du second ordre, et <code>(∀ 'c . (t -&gt; 'c) -&gt; t -&gt; '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 -&gt; captured_parser := Some (prey_parser); object (* fake table object *) end in ignore (Sql.table (* ... *) fake_builder); match !captured_parser with | None -&gt; failwith « failed to capture the flag! » | Some univ_parser -&gt; 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 -&gt; 'a) -&gt; '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 &amp; 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 -&gt; '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>