Ours & Hippy — le blog [~bluestorm]

En ces périodes d’activité intense, il est de plus en plus difficile de prendre le temps d’écrire un bon gros billet comme on les aime. Je me permets de vous servir ici un billet un peu réchauffé : j’ai écrit un article sur Macaque, et j’en profite pour en parler ici.

Macaque a déjà été mentionné sur ce blog, mais sans vraiment d’introduction concrète. J’espère ici présenter Macaque de façon plus introductive, et surtout vous donner le lien vers l'article (18 pages) et vous inciter à le lire.

Macaque

Qu’est-ce que c’est que Macaque ? Puisque la paresse préside ce billet, je me permets de citer, verbatim, le résumé et une partie de l’introduction de l’article.

Macaque est une bibliothèque OCaml permettant d’interagir avec un serveur SQL. Elle permet de construire des requêtes vérifiées statiquement, de façon modulaire. Une extension Camlp4 apporte une syntaxe concrète inspirée des compréhensions. Des types > fantômes sont utilisés pour encoder, en utilisant les types objets d’OCaml, certaines propriétés fines des valeurs SQL, comme la nullabilité.

Les bases de données sont des méthodes solides et reconnues de stockage d’information pour les besoins d’une application. Un programmeur qui voudrait s’en servir est cependant confronté à une situation désagréable : il doit communiquer avec un programme externe (le serveur de base de données) en lui envoyant des requêtes en format texte, c’est-à-dire oublier, dans cette partie de son programme, tout le confort des données structurées et des moyens d’expression de son langage.

La méthode la plus flexible pour construire des requêtes SQL est la production d’une chaîne de caractères correspondant à la requête :

let interroge table predicat =
  "SELECT * FROM " ^ table ^ " WHERE " ^ predicat

Son inconvénient majeur et qu’elle transporte toutes les données sous forme de chaînes de caractères, qui n’apportent aucune information de typage, donc aucune vérification de correction (même syntaxique) à la compilation. En particulier, il y a facilement des problèmes de sécurité si des portions de la requête peuvent provenir d’un utilisateur malicieux du programme.

La méthode la plus sûre pour écrire des requêtes est de vérifier leur validité, au moment de la compilation, en interrogeant directement le serveur SQL, comme le fait le projet PG'OCaml :

let interroge predicat =
  PGSQL(dbh) "select * from ma_table where $predicat"

Pour que cette vérification statique soit possible, la requête doit contenir assez d’information : le serveur PostgreSQL sait vérifier le type des données mais ne dispose ni d’un moteur d’inférence sophistiqué, ni d’une forme de polymorphisme. En particulier, on a dû préciser ici la table étudiée, ma_table. On ne peut pas écrire de fonction générique interroge, qui fonctionne sur n’importe quelle table. On a donc perdu en flexibilité.

Quels sont les compromis acceptables ? Macaque est un langage de requête, embarqué dans OCaml, qui se veut à la fois sûr et flexible. C’est une extension syntaxique couplée à une bibliothèque logicielle à l’interface fortement typée, qui permettent d’écrire des requêtes modulaires en conservant la sûreté à laquelle sont habitués les programmeurs OCaml.

Macaque est un logiciel libre, disponible sur le site OCamlForge.

L’article présente Macaque à des utilisateurs potentiels (Oui, vous !), mais discute aussi de son implémentation. En particulier, la section dédiée au traitement de l’opération GROUP BY décrit les méthodes de métaprogrammation utilisées pour renforcer la sûreté statique permise par le typage.

La petite histoire

J’ai écrit Macaque au cours d’un stage de deux mois dans le laboratoire PPS. Cela ne vous dit sans doute rien, mais beaucoup les connaissent indirectement, car ce sont eux qui hébergent la principale version en ligne du livre « Développement d’applications avec Objective Caml », DA-OCAML pour les intimes, un cours OCaml pas forcément très accessible pour les débutants, mais très complet et qui met les pieds dans le plat de la programmation fonctionnelle.

Une partie des gens de ce laboratoire travaillent sur un ensemble d’outils pour le développement Web dans le langage OCaml. C’est le projet Ocsigen, dont le but est grosso-modo d’apporter la beauté de la programmation fonctionnelle aux sauvages qui codent des sites Web. Comme vous pouvez vous en douter, la diffusion de leur travail est restée plutôt restreinte, mais il y a des choses intéressantes dedans et je vous invite à jeter un coup d’oeil ; personnellement, j’ai abandonné ce terrain depuis longtemps et je ne suis pas impatient d’y remettre les pieds.

Toujours est-il que le sujet qu’ils m’ont proposé était intéressant, puisqu’il combinait beaucoup d’OCaml, du typage, de la métaprogrammation, et plus globalement le travail sur la conception d’une partie d’un langage de programmation, ce qui reste un des points qui me plaisent le plus en informatique.

J’y étais encadré par Jérôme Vouillon, un type très sympathique qui a su m’aider, malgré sa terrible timidité. Sa connaissance du langage OCaml m’a parfois impressionné ; il m’a permis en particulier de résoudre un problème de typage assez velu :

module M : sig
  type 'a t
  val of_option : 'a option -> 'a t
  val to_option : 'a t -> 'a option
end = struct
  type 'a t = 'a option
  let id x = x
  let of_option, to_option = id, id
end

Ce module a l’air tout à fait inoffensif, mais il ne permet pas de conserver le polymorphisme de la valeur None, naturellement de type 'a option :

# let pas_assez_polymorphe = M.of_option None;;
val pas_assez_polymorphe : '_a M.t = <abstr>

Une toute petite modification suffit. Voyez-vous laquelle ?

C’est d’ailleurs un problème que j’aurais dû reconnaître, puisqu’il est mentionné dans un article que j’ai déjà survolé plusieurs fois, Relaxing the value restriction (12 pages).

La rédaction de l’article a eu lieu après le stage proprement dit, et, malheureusement pour moi, sur mon temps libre. Je dirais que cela représente environ 40 heures de travail. Il n’est pas du tout exhaustif, et même pas aussi complet que je l’aurais souhaité : après la première phase de rédaction, une grande partie de l’effort de relecture/retravail avait pour but de le raccourcir pour respecter les contraintes de taille. En pratique, cela constitue à enlever les explications, certains exemples de code, une partie du contenu, et surtout à rogner le plus possible sur les espaces verticaux du document.

Chaque paragraphe a donc été soigneusement retravaillé pour être le moins compréhensible possible, tout en contenant toute l’information nécessaire pour que l’on puisse expliquer à un éventuel critique que s’il n’a pas compris quelque chose, c’est qu’il n’a pas lu assez attentivement. L’étape suivante, utilisée par les copistes avant le septième siècle, est de supprimer la ponctuation et les espaces entre les mots.

Quel futur pour Macaque ?

Je continue à maintenir Macaque sur mon temps libre. La force de développement est donc plutôt réduite, puisque le temps que je lui accorde est faible, mais elle est pour l’instant largement supérieure à la demande : à part le projet Ocsigen, personne ne semble pour l’instant envisager d’utiliser Macaque, et je n’ai donc pas de demandes d’utilisateurs. Pas de retours, pas de développement.

J’ai encore quelques idées de choses à ajouter à Macaque. J’en ai un peu parlé sur le canal IRC #ocaml, et flux m’a fait des remarques qui ont conduit à l’ajout, par exemple, des valeurs par défaut à l’insertion.

Je pense que Macaque est une bonne solution pour le problème qu’il essaie de résoudre : générer des requêtes vers une base de données depuis le langage OCaml. Pour cette raison (et aussi peut-être un peu d’ego), je serais heureux de voir plus de gens s’en servir, profiter de ses qualités, et se plaindre de ses défauts. Je n’ai pas non plus fait beaucoup d’efforts pour populariser Macaque et pousser des gens à s’en servir : j’envisage mollement d’écrire un message consistant à la mailing list OCaml, et ce billet fait lui aussi partie d’une timide campagne de propagande.

Pour ma part, je suis content du travail que j’ai effectué pendant mon stage, et de l’expérience que j’en ai retirée, et je ne m’inquiète pas trop pour le sort des utilisateurs de SQL et OCaml. En plus du projet PG’OCaml déjà cité, d’autres personnes essaient de combiner les deux, dont par exemple quelques divagations sur eigenclass.org, ou le projet Ocaml-orm-sqlite, qui a commencé exactement en même temps que mon stage, mais prend une approche très différente.

En bref, ce n’est pas moi, de mon point de vue, qui décidera du futur (ou pas) de Macaque. Si des gens s’en servent, tant mieux, et je le ferai évoluer vers quelque chose de plus complet, sinon ce n’est pas grave, de toute façon j’ai déjà beaucoup trop de choses à faire.

Ce week-end, je me suis promis que je rédigerai, pour le prochain article que je lirai en entier, un court résumé de deux ou trois paragraphes, pas plus, pour cesser d’écrire des réactions à la longueur démesurée. Voici le résultat.

Coherent Reaction (pdf, 8 pages) est un papier de Jonathan Edwards (pas le prédicateur américain), un type intéressant dont le blog s’appelle Alarming Development (Dispatches from the Programmer Liberation Front). C’est aussi le créateur du langage de programmation visuelle Subtext.

Problématique

En travaillant sur Subtext, il s’est rendu compte que l’ordonnancement des effets de bords pose problème dans un programme interactif (avec une interface utilisateur, comme par exemple des formulaires Web). Son exemple, dans un cadre MVC classique, est le suivant : imaginez qu’on travaille sur trois valeurs, qui pour avoir du sens doivent vérifier une contrainte de correction commune (par exemple la troisième, 5, doit être la somme des deux premières, 2 et 3). C’est le contrôleur qui vérifie ces contraintes : il dispose pour chaque valeur d’une fonction de vérification.

Maintenant, si on change deux de ces valeurs en même temps (la première à 4 et la troisième à 7), il y a risque de "fausse erreur" si les vérifications ne sont pas faites dans le bon ordre : si on modifie la première valeur à 4, puis on vérifie, on a une erreur (la contrainte n’est plus vérifiée, car 4 + 3 ne vaut pas 5) alors que si on avait modifié les deux ensemble tout se serait bien passé.

Il y a aussi des situations ou l’ordre de modification est important : fondamentalement, on voudrait que chaque modification s’effectue en parallèle, indépendamment, mais les langages impératifs effectuent les effets les uns après les autres, donc il y a toujours un risque d’interférence.

Les solutions classiques proposent que le modèle donne plus d’informations sur les contraintes liées au données : quelles sont les données liées, par exemple, pour qu’on les modifie toujours toutes en même temps au lieu d’une par une. Leur inconvénient, d’après l’article, est une perte en modularité, puisque cela révèle une partie de l’implémentation du modèle.

Coherent Reaction

Pour Edwards, le problème de fond est la difficulté à coordonner les effets de bords dans les langages impératifs classiques : plus les contraintes sont complexes, plus elles sont difficiles à gérer et donnent lieu facilement à des erreurs de programmation difficile à repérer. Il propose de libérer le programmeur des questions de coordination avec sa notion de cohérence, qui est une forme d’atomicité : le programmeur ne précise pas dans quel ordre faire les modifications, et c’est le programme qui le découvre par essais/erreurs : si des modifications produisent un état inconsistent ou introduisent des interférences, on les annule (rollback) pour les recommencer dans un ordre différent.

Il a aussi conçu, comme expérience pratique, un langage de programmation basé sur cette idée. C’est un langage dynamique centré sur les données (plutôt que les comportements, comme la POO), mettant en avant deux concepts :

dérivation

une façon de déduire des champs du reste de l’objet : on peut dire par exemple qu’un champ c dérive de la somme de deux champs a et b. Si l’un de ces champs est mis à jour, le champ c sera modifié en conséquence, pour maintenir cet invariant.

réaction

propagation de modifications dans le sens inverse de la dérivation : une réaction est une sorte de callback qui est exécuté quand le champ auquel elle se rattache est modifié

Ces deux mécanismes de transmission des modifications permettent de maintenir simplement l’état des données; pour les combiner, c’est le programme qui se charge de trouver un ordre des dérivations/réactions qui évite les interférences.

Remarques personnelles

J’ai apprécié cet article, mais peut-être un peu déçu : pour la réinvention des effets de bord, je m’attendais à quelque chose de plus profond. La discussion des travaux similaires, étendue dans la version longue du papier, est très intéressante.

Je ne suis pas tout à fait convaincu que cette idée peut être reprise dans le cadre d’un langage généraliste, mais elle pourrait être appropriée comme paradigme spécialisé des parties interactives d’un programme. La comparaison avec la programmation fonctionnelle réactive serait certainement intéressante, mais c’est un sujet que je ne connais pas (bien que j’envisage de m’y intéresser prochainement) donc je ne pourrais pas en dire plus.

Enfin, l’article se termine quasiment par un paragraphe, en réaction à une citation très classique d’Alan Kay, qui me semble tout à fait obscur. Je ne pense pas le comprendre, c’est bien trop flou/littéraire/psychologique pour moi, mais je pense qu’il pourrait intéresser certains lecteurs :

Smalltalk’s design—and existence—is due to the in- sight that everything we can describe can be repre- sented by the recursive composition of a single kind of behavioral building block that hides its combina- tion of state and process inside itself and can be dealt with only through the exchange of messages.

– Alan Kay : The early history of smalltalk

The conceptual model of Coherence is in a sense opposite to that of Object Oriented languages. As Alan Kay’s quote above indicates, the central metaphor of OO is that of mes- saging: written communication. The central metaphor of Co- herence is that of observing a structure and directly manip- ulating it. These two metaphors map directly onto the two primary mechanisms of the mind: language and vision.

Il est arrivé une bonne chose à mon dernier billet : des gens m’y ont répondu en commentaire. Je les remercie tous chaudement. Ce n’est pas complètement rationnel, mais je trouve ça vraiment appréciable, et ça m’a motivé pour retenter l’expérience de ces billets « en bref ». Mais pas pour cette fois : c’est intéressant quand on a différentes choses à dire, et il vaut mieux que ce ne soit pas trop souvent, sinon ils deviennent de plus en plus vides et répétitifs.

Dans les commentaires, que j’ai lus avec intérêt (j’ai même répondu à certains, c’est fou les blogs), se trouve une question qui m’a donné envie d’en faire un billet à part entière. C’est le commentaire de robocop :

Il y a quelque chose qui ressort quand même pas mal dans nombre de tes articles, c’est l’importance que tu attaches aux types. J’ai la facheuse impression d’être passé à coté de quelque chose de fondamental, pour moi, les types ce n’est qu’une vérification supplémentaire qui est fait à la compilation et ou à l’interpretation, mais à la façon dont tu en parles, le système de type semble le cœur même d’un langage de programmation.

Si comme je le pressens, je loupe vraiment quelque chose, pourrais-tu disserter rapidement là-dessus ?

En une phrase : pourquoi, parmi toutes les caractéristiques d’un langage de programmation, attacher autant d’importance à son système de typage ?

J’ai été surpris de ne pas pouvoir répondre à cette question sur le moment. J’ai pris du temps pour y réfléchir, et je pense avoir maintenant une réponse satisfaisante (mais pas rapide).

J’ai apprécié les commentaires de la carotte qui, avant l’ours, a relu ce texte et m’a permis de l’améliorer.

Rappels

Je ne compte pas expliquer dans ce billet les divers avantages et inconvénients, existants ou fantasmés, des différents systèmes de typage ; ce n’est pas le sujet. Je me contenterai ici d’un bref rappel de deux notions qui reviennent souvent quand on discute les systèmes de typage, et dont je reparlerai par la suite :

typage statique

désigne les systèmes de typage qui vérifient les types dans un programme avant de l’exécuter, typiquement au moment de la compilation. Les erreurs de typage, s’il y en a, sont signalées pendant cette phase et le programme n’est pas exécuté tant qu’il n’est pas correctement type. En général, à l’exécution, on n’a plus à se soucier des types et on peut raisonner comme s’ils n’existaient plus.

typage dynamique

désigne les systèmes de typage qui vérifient les types pendant l’exécution du programme. Avant chaque opération que le programme doit exécuter, il vérifie que les types des données sont correctes ; cela implique que le programme a accès à ces types quelque part : ils sont stockés dans la mémoire du programme pendant son exécution.

Ce sont deux méthodes très différentes qui ont un but commun : empêcher l’ordinateur d’effectuer des opérations mal typées (« mélanger des patates et des carottes »). Chaque façon de faire a ses adeptes, et les deux camps se livrent des guerres terribles, depuis plusieurs générations de langages de programmation — et, bientôt, d’informaticiens. Le point important ici est que les langages mettant en place l’une ou l’autre de ces méthodes ont un système de typage. Il sera plus ou moins bien défini, selon la précision de la définition du langage lui-même, mais dans tous les cas on peut s’y intéresser.

J’ai déjà parlé du typage dans un article publié sur le SdZ : Le typage, présentation thématique et historique. Je n’en suis pas complètement satisfait : je le trouve trop jeune et un peu naïf, et j’essaierai peut-être de le reprendre quand je saurai mieux ce que je veux dire.
Pour les débats autour du choix d’un système, j’aime bien l’article What To Know Before Debating Type Systems. Il est peut-être un peu biaisé en faveur des systèmes statiques, et un peu trop technique, mais il apporte une vue d’ensemble assez intéressante. C’est une bonne base si vous voulez vous lancer dans le débat : statique ou dynamique ?

Cependant, ce que je voudrais discuter ici, ce n’est pas le choix de telle ou telle méthode de typage, mais plutôt la place du typage au sein d’un langage de programmation, relativement aux autres aspects du langage.

Types comme information

Imaginez que vous voulez écrire un petit morceau de programme dans le langage de votre choix, qui soit réutilisable par d’autres programmeurs. Vous devez leur décrire ce que vous avez fait. Vous commencez par leur dire ce que fait ce bout de programme (« c’est une compression selon le codage de Huffman »), et vous allez décrire la manière dont ils doivent interagir avec ce bout de programme pour profiter de ses bienfaits : « on lui donne un texte, et il le renvoie compressé, avec le dictionnaire de compression ». Avec cette simple phrase, vous avez déjà transmis des informations de typage : on lui fournit un texte, donc en général une chaîne de caractère. S’il a besoin de plus d’informations (par exemple sur la nature du dictionnaire de compression), vous donnerez une description plus précise qui contiendra autant d’informations de typage supplémentaires.

Cette façon de procéder est commune à l’ensemble des programmes et langages. Choisissez un langage que vous appréciez et qui a une documentation utilisable : elle contient (plus ou moins explicitement) des informations de typage. Par exemple, j’ai choisi une page au hasard de la documentation du langage PLT Scheme, réputé « non typé », dans laquelle on peut trouver le texte (code ?) suivant :

(directory-exists? path) → boolean?
  path : path-string?

C’est tout à fait du typage : on décrit une fonction qui vérifie qu’un répertoire existe dans un système de fichier. Cette fonction accepte un chemin de type path-string, et renvoie un boolean. Les points d’interrogation soulignent un détail intéressant : les noms choisis pour décrire les types sont aussi des fonctions (prédicats) que l’on peut utiliser pour vérifier qu’une valeur est bien du type donné. Par exemple la documentation de la fonction path-string? contient :

(path-string? v) → boolean?
  v : any/c

Ces prédicats sont utilisés au sein de ces fonctions pour vérifier que l’utilisateur ne donne pas n’importe quoi, et la vérification de validité est donc effectuée à l’exécution : c’est une forme de typage dynamique.

Ce ne sont pas les seules explications concernant ces fonctions, il y a aussi du texte en langue naturelle qui explique leur usage. Certaines documentations ne mettent aucune information de typage aussi claire (je pense à Python par exemple), il faut aller la pêcher dans le texte explicatif, ou encore elle peut être implicitement contenue dans les noms des paramètres, qui respectent des conventions facilitant cette tâche.

L’idée importante c’est qu’au fond, un type c’est essentiellement une information sur une expression du langage de programmation.

Le langage qui parle de lui-même

Cette idée des types comme informations est très large, car elle doit faire cohabiter les notions de typage très différentes selon les langages. Elle est peut-être même un peu trop étendue, puisqu’elle désigne tout et n’importe quoi, et que je ne vais pas avoir de mal à vous convaincre que vous avez besoin d’informations pour coder correctement. On peut affiner un peu plus.

Quand on parle du système de typage d’un langage, on n’a pas en tête les conventions de nommage des paramètres utilisées dans sa documentation. On parle en général d’une manière de décrire ces informations qui fait partie du langage lui-même : le système de typage, c’est la partie du langage qui permet de donner des informations sur les valeurs.^α Je désigne cette partie par le terme langage de types : par exemple le langage des types du C est un sous-ensemble du langage C qui contient les types de base (int, float..), des modulateurs (unsigned), enum, struct, …, des pointeurs, tableaux, et même des types fonctionnels.

En d’autres termes, le système de typage, c’est un méta-langage, qui détient le pouvoir d’expression du langage sur lui-même. Plus le système de typage est expressif, plus on peut dire de choses sur un programme au sein de ce programme, plutôt que dans la documentation ou en commentaire.

Vous comprenez sans doute pourquoi, avec ce point de vue, j’attache tellement d’importance, quand je m’intéresse à un langage de programmation, à son système de typage : c’est une partie toute fondamentale puisqu’elle détermine la capacité des programmes dans ce langage, en plus de faire quelque chose d’utile, à transmettre des informations sur ce qu’il fait.

Il faut cependant bien remarquer que, bien que très importante, elle n’est pas non plus indispensable : on peut très bien imaginer des langages qui ne permettent de formuler aucune information sur les programmes, mais qui ont d’autres qualités qui en font des langages intéressants. Je pense par exemple à Forth, un des premiers langages à pile haut niveau.

Système de typage et vérification

La définition actuelle reste assez molle : est-ce que les prédicats de PLT Scheme constituent un système de typage ? Ils font partie du langage, mais leur utilisation est laissée au bon vouloir de l’utilisateur : il peut aussi implémenter sa fonction sans faire aucune vérification. On pense en général plutôt à des systèmes dans lesquels le typage est obligatoire, et vérifié automatiquement^γ par le compilateur. Ce qui est sûr c’est que les informations implicites de la documentation Python ne rentrent pas dans ce cadre : le typage en Python, c’est ce que le compilateur sait vérifier de lui-même et afficher dans un message d’erreur : l’appartenance à une classe, l’existence d’une méthode donnée, etc.

Quand on décrit le système de typage d’un langage, il faut donc aussi préciser la manière dont ces informations sont vérifiées, ou plus généralement exploitées par le reste du langage. Il y a d’autres distinctions que la vérification statique ou dynamique que j’ai évoquée. Par exemple, certains langages permettent des conversions implicite d’un type vers un autre, ou le choix dans une fonction d’un comportement différent selon le type des paramètres ; on parle dans ce dernier cas de polymorphisme ad-hoc, car il permet de gérer chaque cas particulier séparément.

Autres points à considérer pour son système de typage

L’expressivité et les conditions de vérification ne sont pas les seuls points à débattre d’un système de typage.

On peut s’intéresser à l’emplacement, au sein des programmes de ce langage, des annotations de typage. Certains langages demandent au programmeur très peu d’indications de typage, car ils peuvent les reconstruire à partir des informations déjà présentes dans le langage : c’est l’inférence de type. Plus le langage des types est expressif, plus cette reconstruction est difficile. Les annotations peuvent encombrer le programme si elles sont trop nombreuses, mais placées judicieusement elles peuvent augmenter la lisibilité. Plus généralement, les informations de typage, qu’elles soient produites par le programmeur ou ses outils, renforcent la documentation et la modularité entre les différentes partie du programme : donner le type des valeurs d’une bibliothèque logicielle facilite beaucoup son utilisation par d’autres programmeurs, surtout quand il est assez expressif pour traduire l’ensemble des contraintes d’utilisation de cette interface.

Un dernier exemple, plus sophistiqué, la propriété de séparation : dans certains langages (dont OCaml), le typage est une phase totalement séparée de l’évaluation, dans le sens où une fois qu’on a un programme bien typé, on peut oublier complètement tout ce qui concerne le typage, et cela ne change absolument rien au déroulement du programme.^δ Dans d’autres langages, en particulier ceux qui possèdent le polymorphisme ad-hoc, il n’y a pas cette séparation. L’avantage de cette propriété est qu’elle donne un langage plus simple à comprendre, avec des phases plus indépendantes. L’inconvénient est qu’elle est contradictoire avec certaines fonctionnalités que les concepteurs du langage peuvent avoir envie de fournir : imposer la séparation peut réduire l’expressivité. Il n’y a pas de bon et de mauvais choix dans l’absolu, cela dépend des besoins du langage, mais c’est un choix auquel les systèmes de typage sont confrontés. On peut enfin imaginer des distinctions plus fines, avec une partie du langage qui brise la séparation, mais qui est traduit dans une première phase vers un langage plus simple, bien séparé. C’est comme cela par exemple qu’on manipule les type classes de Haskell quand on veut en donner des définitions très précises (formelles).

Contraintes et limitations

Si le langage des types est peu expressif, et la vérification très rigoureuse (impossible de définir des termes non typés), le typage peut vite devenir une contrainte. Par exemple, le langage des types du C ne permet pas d’exprimer le polymorphisme paramétrique (une fonction qui marche sur tous les types ayant structure donnée) ; on fait avec, en utilisant une sorte de type-à-tout-faire, void *, qui permet d’abandonner à la fois l’information de typage et la restriction qui y est associée.

Cette limitation que l’on rencontre n’est pas seulement un artefact de systèmes pratiques, mais se trouve déjà dans la théorie des langages. Par exemple, le lambda-calcul simplement typé de base ne permet pas d’écrire des programmes qui ne terminent pas : tous les programmes bien typés terminent en un temps fini. Ça a ses avantages, mais aussi un inconvénient : ce langage n’est pas Turing-complet. En gros, il y a des fonctions qu’on ne peut pas écrire avec. On peut lever cette limitation,^ε soit en enrichissant le langage des types (polymorphisme plus types récursifs par exemple), soit en ajoutant des constructions au reste du langage (opérateur de point fixe ou définitions de fonctions récursives).

Les langages au typage dynamique ont en général un langage de type assez faible, mais ont du coup l’avantage de ne poser que très peu de contraintes : comme ils ne vérifient pas grand chose au niveau du typage (par exemple, ils ne vérifient pas le fait que les deux branches d’une condition renvoient le même type), ils ne posent pas non plus de contraintes gênantes. C’est un autre choix qui peut se justifier ; par exemple, certains motifs de conception de la programmation objet sont notoirement difficiles^ζ à typer correctement (ils demandent un langage très expressif), les langages dynamiques n’ont pas ce problème.

Pour bien typer, il faut bien comprendre

Il arrive donc assez souvent que des idées sur de nouvelles façon de programmer soient développées dans un cadre non typé, et qu’elles trouvent seulement ensuite leur place dans un système de typage, comme par exemple le transfert du langage de programmation Oz, langage dynamique qui a popularisé certains paradigmes de concurrence, à AliceML, langage typé qui reprend une partie de ces fonctionnalités.

Cela ne veut pas dire que le cadre non typé est plus fructueux : exprimer précisément une information statique sur ces nouvelles idées permet souvent de les éclairer d’un jour nouveau. Par exemple, la recherche de sémantiques statiques pour les langages à effets de bords a donné lieu à l’idée de monade, qui est utilisée en Haskell pour représenter, entre aures, les effets de bords, et qui a pour conséquence de modifier le type des programmes en y rendant ces effets explicites. On y a gagné des outils intéressant, un point de vue nouveau, et une meilleure compréhension^η de la programmation impérative.

Malheureusement, la programmation est un sujet compliqué dont nous n’avons fait qu’égratigner la surface : il y a beaucoup de choses qu’on ne sait pas encore expliquer de manière simple et précise à la fois, par exemple la concurrence, les manipulations mémoire, la communication avec les programmes extérieurs, etc. L’explication et le typage précis de manières avancées de programmer est un sujet de recherche actif, dont on espère qu’il nous apportera des réponses ; en attendant, il faut se contenter de typages correspondant à l’état des connaissances aujourd’hui, et qui ne sont pas forcément aussi expressifs qu’on le voudrait.

Puissance du typage et complexité du langage

Cette difficulté que rencontrent les concepteurs de langage de programmation se retrouve aussi, à plus petite échelle, quand un programmeur essaie de donner un type statique à son programme. Quand on code dans un langage dynamique, on ne se soucie essentiellement que d’une chose : il faut qu’au moment de l’exécution, notre programme marche. Donner un type très expressif à un programme, cela peut demander de rendre explicites plus d’informations : qu’est-ce que notre programme fait, comment le fait-il, pourquoi cette fonction est-elle correcte ? L’ordinateur peut en deviner une partie (c’est le principe de l’inférence des types), le programmeur en connaît une partie (par exemple ce qui est un entier, et ce qui est un booléen dans son programme), mais il y a parfois des programmes compliqués pour lesquels ce n’est pas aussi simple : donner un type très précis impose une bonne compréhension du programme.

Bien entendu, même dans les langages typés, un programmeur a toujours la possibilité d’utiliser des représentations moins expressives, et qui demandent donc moins de réflexion. Par exemple, au lieu d’avoir un type de donnée spécialisé pour décrire les dates (jours, mois, heure, etc.), on peut par exemple utiliser des chaînes de caractères. C’est généralement une mauvaise idée : un effort au départ pour décrire et utiliser un type plus précis permet ensuite des manipulations plus sûres et plus directes.

Il y a cependant un point à ne pas oublier quand on cherche des langages de types expressifs : ils rendent nécessairement les langages plus complexes. Quand des débutants en Ada doivent comprendre les différences entre les paramètres in, out, et in out, ils peuvent penser qu’un langage faisant moins de fioritures aurait été plus simple. On peut se demander s’il vaut mieux concevoir des langages simplifiés pour les débutants et des langages moins simples mais ayant d’autres qualités pour les experts, ou si une taille unique peut convenir à tout le monde. Cette question intéressante est encore ouverte, mais il est clair que la simplicité (réelle ou perçue) d’un langage joue dans son adoption par les programmeurs, et qu’on ne peut pas se permettre de concevoir des systèmes de typage arbitrairement compliqués en espérant qu’ils vont dominer le monde.

Tous les langages sont typés, parfois sans le savoir

Ma définition est suffisamment large pour qu’on puisse trouver un système de typage à tous les langages, même ceux qui se proclament traditionnellement « non typés ». Les cas les plus extrêmes sont les langages dont les types sont tellement pauvres qu’ils ne peuvent essentiellement rien dire d’intéressant. Par exemple, en Brainfuck, le système de typage est vide : on ne peut rien dire sur les programmes, et d’ailleurs il n’y a rien à dire puisqu’ils ne manipulent jamais rien d’autre qu’une bande mémoire dont une case est pointée.

Plus utiles, les assembleurs sont aussi des langages avec des typages très pauvres : il y a en général des registres, des valeurs immédiates et des adresses mémoires (et par exemple des labels à plus haut niveau), et des considérations de taille, alignement, etc., qui sont assez riches mais ne nous apprennent pas beaucoup sur le comportement à plus haut niveau du code, tant qu’on ne le munit pas d’un système de typage plus expressif.^θ On peut encore citer le langage de Matlab/Octave, qui ne connaît essentiellement que les matrices de scalaires, ce qui peut parfois donner de très mauvaises surprises.

Mélanger typage statique et typage dynamique ?

Cette idée de décrire les langages peu typés comme possédant un petit nombre de « types poubelles » ne donnant que très peu d’information peut en fait être utilisée pour mélanger au sein d’un langage le typage statique et le typage dynamique : on peut rajouter ces types poubelles à l’éventail des types du langage.

Il s’agit de permettre de « perdre » localement l’information de typage, en transformant toutes les valeurs, quelle que soit leur type, vers un même type dynamic. On peut ensuite utiliser une fonction d’extraction pour récupérer des valeurs bien typées dans les parties du programme qui n’ont pas besoin de typage dynamique. Cette idée est vieille comme le monde, il s’agit de faire un cast (conversion d’un type vers un autre) au détriment de la sûreté du typage, et elle est présente dans un grand nombre de langages de programmation.

Pour que cette méthode ne nuise pas trop à la sûreté de l’application dans son ensemble, il faut réutiliser les méthodes de vérification de typage des langages dynamiques : quand on envoie la valeur vers le type poubelle, on lui associe une autre valeur runtime^ι qui décrit son type. Ensuite, quand on convertit à nouveau la valeur dynamique vers un type plus expressif du langage, on peut insérer un test pendant l’exécution qui vérifie que le type d’arrivée est bien compatible avec le type dynamique stocké avec la valeur.

Au-delà du dynamic_cast de C++, les langages fortement typés ont fait des tentatives dans cette direction. La solution la plus simple est de demander à l’utilisateur de ces fonctions d’insertion et extraction dans le type dynamique de manipuler lui-même les types dynamiques, en utilisant une bibliothèque logicielle dédiée. On peut utiliser des fonctionnalités du langage pour simplifier cette manipulation (par exemple des macros syntaxiques, des types fantômes,^κ ou des type classes), et mettre en place des bibliothèques logicielles apportant ces facilités aux programmeurs.

Ça n’est cependant pas suffisant : si l’on se contente d’une bibliothèque logicielle à part, le langage ne garantit pas la cohérence entre l’information statique de typage dont il dispose, et les valeurs dynamiques construites par l’utilisateur ou sa bibliothèque spécialisée : même quand elle est fortement typée (les manipulations à l’extérieur de la bibliothèque sont sûres) il faut faire confiance à l’auteur de cette bibliothèque de valeurs dynamique pour n’avoir pas fait d’erreurs de conversion à l’intérieur.

Si l’on veut plus de simplicité et de sûreté, il faut intégrer cette fonctionnalité directement au sein du langage de programmation. La communauté CAML a fait partie des pionniers de ce domaine avec Dynamics in ML, une extension du langage proposant des valeurs dynamique même pour les types polymorphes. Les langages fonctionnels Clean et AliceML proposent aussi cette fonctionnalité.

Ces méthodes permet de concevoir des langages typés statiquement mais qui acceptent de « laisser la main » gracieusement quand on atteint les limites de leur expressivité. Cela permet de résoudre les problèmes des constructions trop difficiles à typer mentionnés auparavant, sans abandonner trop de typage. Malheureusement, en pratique la mise en place de tels systèmes au sein d’un langage peut compliquer sensiblement son implémentation efficace, et elles ne sont donc pas très répandues. C’est encore une fois un sujet de recherche actif. Il y a des langages qui essaient de rendre encore plus transparente la frontière entre les mondes dynamiquement et statiquement typés. Cela demande de nouvelles méthodologies de typages, et tout une zoologie se crée autour du sujet : soft typing, gradual typing, blame typing, hybrid typing, …

En attendant, les programmeurs se contentent en général de méthodes plus indirectes, en utilisant des valeurs dans des types moins expressifs mais plus souples, comme le font sans le savoir les utilisateurs de langages dynamiques.

Les types ne font pas tout

Ce billet a beaucoup parlé des types, et de pourquoi le système de typage est un ingrédient majeur d’un langage de programmation. Il ne faut pas non plus oublier que ce n’est pas le seul, et qu’une grande partie de l’intérêt des langages ne vient pas du tout de leur système de types.^λ

L’un des livres sur la programmation qui m’a beaucoup plu est le CTM : Concepts, Techniques and Models of Computer Programming. C’est un livre vraiment formidable, qui a étendu mon horizon en matière de techniques de programmation, et qui pourtant ne parle pas du tout, ou quasiment pas, de typage.

Comme rz0 l’a admirablement fait remarquer, le blog est plutôt mort ces temps-ci. Sans surprises, je suis occupé depuis le début de l’année, et le temps pour poster des billets en a diminué d’autant. Je me suis fixé l’objectif de ne pas passer plus d’une heure à écrire ce billet (écriture seulement, il y aura sans doute de la relecture ensuite), et ça me paraît un pari assez raisonnable, bien que nettement plus ambitieux que les billets précédents. La qualité en souffrira certainement, mais j’essaie de trouver un équilibre.

Je remarque d’ailleurs que je ne suis pas le seul à être occupé : tous ces gens qui avaient promis juré que oui, ils feraient des efforts pour poster des commentaires de temps en temps, histoire qu’on conserve la motivation, ils ont visiblement un travail fou. Tant pis ; de toute façon je n’ai pas les moyens (temps, motivation et envie) d’écrire de gros billets bien préparés en ce moment. Si j’écris celui-ci, c’est parce que j’ai honte de laisser cet espace tellement vide alors que rz0 a fait tant d’effort pour m’installer un petit coin bien douillet. Et j’espère aussi que ce que j’ai à vous raconter pourrait vous intéresser.

Débuts en Coq

Cette année, j’ai décidé de me lancer dans le vaste monde des assistants de preuve. En un mot, ce sont des programmes qui permettent d’écrire des preuves mathématiques, et qui les valident : ils savent dire si oui ou non, une preuve est correcte.

Je leur vois deux intérêts principaux. D’une part, ils permettent de se redonner confiance en mathématiques ; si vous connaissez le malaise de celui qui écrit un brouillon de preuve, mais sans savoir vraiment si elle est juste ou contient une erreur désagréable que vous n’aviez pas vue, vous comprendrez ce que je veux dire. Plus généralement, c’est un peu comme la différence, en informatique, entre écrire du pseudo-code, et écrire dans un vrai langage de programmation : l’avantage d’un vrai langage, c’est que vous pouvez exécuter le programme pour vérifier qu’il fonctionne (et en particulier vérifier sa syntaxe, etc. automatiquement), alors qu’on est rarement motivé pour relire avec soin un pseudo-code. L’ordinateur apporte un retour d’expérience (feedback) direct, impartial et incontestable.

D’autre part, les assistants de preuve sont essentiellement des langages de programmation. Ils se placent en effet à cheval entre la théorie des types (côté informatique) et la théorie de la démonstration (côté mathématiques) : c’est essentiellement le même domaine, vu de points de vue différents. On parle souvent de l’isomorphisme de Curry-Howard, mais ce théorème précis concerne des systèmes bien précis, et l’étendue de la correspondance est en fait beaucoup plus large ; fondamentalement, depuis le début du 20e siècle, on pense les preuves formelles comme des programmes (fonctionnels). Ces outils font donc de bons mélanges entre des preuves très formelles et des langages très fortement typés, et ça a tout pour me plaire. On peut d’ailleurs aussi utiliser ces systèmes pour prouver des choses sur les langages de programmation (tous paradigmes confondus, cette fois-ci).

Il existe plusieurs systèmes d’assistants à la démonstration. Les plus utilisés actuellement sont Coq et Isabelle (et éventuellement Twelf et HOL-Light, avec aussi des anciens couverts de lauriers (Mizar), et de jeunes qui explorent l’espace de recherche (Agda)). Ces systèmes ont des qualités et des défauts variés. J’utilise Coq. D’une part parce que c’est le système conçu en France, et donc je suis entouré de gens qui l’utilisent, l’enseignent, voire le développent.^α D’autre part, j’utilise pour apprendre les bases le livre en ligne Certified Programming with Dependent Types, qui conseille d’utiliser Coq et qui a certainement ses raisons, moi, je ne connais pas assez le domaine pour faire un choix informé.

Ces outils sont majoritairement codés dans un des langages dont le nom contient « ML » et ne commence pas par « X ». C’est une corrélation historique, puisque le langage ML (notre grand-père à tous) a été créé conjointement à l’assistant de preuve LCF.

Au passage, si vous envisagez vous-même de vous intéresser un jour au sujet, je suis assez content de ce bouquin. En particulier, il prend surtout ses exemples dans le monde des langages de programmation : dès le premier chapitre, on compile des expressions arithmétiques simples vers une machine à pile simple, en rajoutant du typage à gogo, et sera donc plus accessible qu’un livre orienté vers la logique formelle si vous vous sentez plutôt informaticien. Une connaissance (au moins des bases) de la programmation fonctionnelle est tout de même indispensable.

Il est temps de signaler les deux articles qu’asmanur a écrit comme une petite introduction à Coq (un passe-temps qu’il a certainement abandonné assez vite, comme tous les autres) : Voyage au bout de la logique, et sa deuxième partie. Si vous vous intéressez à la discussion sur le choix de l’assistant à la démonstration, vous pouvez aussi lire l’introduction du livre de Chiplala. Au passage, le mode Emacs qu’il recommande, Proof General, est vraiment très bien.

Programmation par contraintes

Cette fois-ci, cela tient plus de l’anecdote, mais je trouve ça assez amusant pour avoir envie de vous en parler. En plus de la logique formelle fonctionnelle typée et des hautes sphères éthérées de la théorie des catégories, je fais cette année des choses bassement matérielles qui demandent de la programmation. Évidemment, je fais tout en OCaml.

Depuis cet été, je suis assez séduit par les types fantômes. C’est un outil vraiment puissant et agréable, à tel point que je suis tenté d’en mettre un peu partout dans mes divers projets. Par exemple, je dois coder un projet de bataille navale en réseau (et d’ailleurs c’est assez ennuyeux ; je prends sur mon temps de développement pour vous écrire cet article). Ça a l’air assez trivial, mais j’ai perdu tellement de temps à refactoriser dans tous les sens pour avoir le typage le plus expressif possible que j’en suis venu à m’auto-imposer la règle suivante : « Interdiction d’utiliser les types fantômes ! »

Et vous, avez-vous des règles personnelles que vous appliquez avec cruauté, pour éviter de perdre votre temps dans des considérations, certes intéressantes, mais déraisonnables pour le projet précis sur lequel vous travaillez ?

J’en profite pour vous signaler que j’étais passé à côté jusqu’à présent, mais j’ai découvert récemment que la bibliothèque standard OCaml utilise elle aussi, des types fantômes, ma bonne dame : ça se passe dans le module le plus haut niveau de la bibliothèque, Bigarray.

Traitement d’images

Je suis, par un curieux hasard de circonstances, un cours de traitement d’images. C’est un sujet très éloigné de mes centres d’intérêt habituels, mais je ne le regrette pas. Je vois défiler beaucoup de jolies photos, et de méthodes pour les améliorer encore, parfois franchement inventives. J’ai un professeur formidable, qui est un mordu de la photographie, mais aussi un amateur de l’analyse de Fourier. Sans entrer dans les détails pénibles, il nous fait des démonstrations « avec les mains » qui sont parfois assez sympathiques, et donnent un petit coup de jeune à toutes ces choses qui sombrent lentement dans l’oubli quand on ne les utilise pas.

Au cas où ça vous intéresse, voici un exemple d’algorithme que nous avons étudié : Colorization Using Optimization. Il s’agit de donner des couleurs à des images en noir et blanc, à partir de quelques indications de l’utilisateur (des traits de couleur connue). L’idée de base, c’est de supposer que deux pixels de luminosité proche doivent être de couleur proche. On peut alors exprimer la teinte de chaque pixel en fonction de celle de ses voisins et, combiné aux conditions initiales de l’utilisateur, ça donne un gros système linéaire (une grosse matrice) qu’on fournit à une fonction de résolution et pouf, une image en couleur. Ça marche étonnamment bien.

Pour ce cours, j’ai participé à l’écriture de bindings OCaml vers des bibliothèques C (ou interfacées par l’intermédiaire du C), par exemple OpenCV ou SuiteSparse. C’est très drôle, on retrouve la joie du segfault (et c’est encore mieux à plusieurs). Je ne m’étais jamais vraiment plongé dans l’interface C-OCaml, et je peux vous dire que ce n’est pas inoubliable mais ça reste une expérience amusante. Cela m’a d’ailleurs permis de mettre mon petit grain de sel dans un tutoriel de Cacophrène à ce sujet sur le SdZ. Ça fait toujours une introduction en français à ce sujet, qui peut servir de mise en bouche, mais si un jour vous voulez vraiment coder quelque chose je vous conseille ensuite de lire conjointement le manuel officiel pour les idées, et le tutorial en anglais de François Monnier pour les exemples de code. Attention au DA-Ocaml, sur ce point il est un peu vieux.

Une petite réaction pour finir ?

Que serait mon billet mensuel sans une référence, ou du moins une allusion, à un petit papier à se mettre sous la dent ? J’en ai survolé une bonne poignée depuis la rentrée, mais les derniers que j’ai croisés sont des articles de Gilad Bracha. C’est un type qui a commencé ses exploits en codant un système Smalltalk avec annotations optionnelles de typage très performant^γ, pour aller ensuite réutiliser ses compétences en travaillant sur Java, sa spécification et sa VM chez Sun pendant quelques temps, avant de repartir construire un nouveau langage dynamique, Newspeak.

J’ai jeté un coup d’oeil à la bête. Comme vous imaginez, les langages très dynamiques ne sont pas forcément ceux qui me tentent le plus, mais ça fait du bien de voir ce qui se fait ailleurs de temps en temps. J’ai aussi lu deux de ses papiers au hasard : Executable Grammars in Newspeak, et Pluggable Type Systems.

Le premier papier présente une façon possible de créer une bibliothèque de parsing combinators dans un langage dynamique. Comme l’annonce l’auteur d’entrée de jeu, c’est plutôt le point fort des langages fonctionnels (l’étalon dans le domaine étant le très bon Parsec de Haskell). Il promet que les fonctionnalités nouvelles de son langage, ainsi que son fort dynamisme, permettront d’en faire une traduction « objet dynamique » adaptée. Je n’ai pas été émerveillé par le résultat (en particulier, comme toutes les approches « DSL internes au langage », la syntaxe n’est au final pas si géniale que ça), mais ça reste une lecture intéressante. Il discute aussi de la facilité ou non à typer ces opérations dans un langage statique, mais le référentiel semblant être celui de Java, on en apprend plus sur l’état des systèmes de types mainstream que sur le fond du problème.

Le deuxième article n’est pas vraiment un article scientifique, mais plutôt une prise de position de l’auteur. Il voudrait qu’on envisage les systèmes de type non pas comme une donnée fondamentale du langage de programmation, à laquelle tout programme dans ce langage doit se soumettre, mais comme une étape supplémentaire, optionnelle. C’est une idée très séduisante, mais assez délicate à mettre en place en pratique (la plupart des avantages théoriques des systèmes de types actuels venant justement de leur capacité à (presque) tout contrôler).

Il voudrait aussi que l’inférence soit optionnelle/désactivable, en un mot « pluggable », ce qui est un point de vue intéressant (et trouve des échos chez les théoriciens^δ). Il voudrait même pouvoir faire cohabiter plusieurs systèmes d’inférence pour « choisir le meilleur selon les situations », et là je ne suis franchement pas convaincu : ça mène à une situation où le type repose sur beaucoup d’heuristiques diverses que le programmeur ne maîtrise pas en général, et cela pourrait à mon avis poser plus de problèmes que ça n’en résoud. Ça reste une lecture intéressante, c’est agréable de voir que les universitaires grisonnants ne sont pas les seuls à se poser la question.

Pour amadouer mes lecteurs potentiels les plus revêches, je dois signaler que cet article cite explicitement les essais d’ajout (partiel) d’un typage statique au langage Erlang.

P.S. : Mon pari de temps n’a pas été tenu, j’ai plutôt mis une heure et demie, mais c’est toujours agréable d’écrire. Ma bataille navale avance assez bien : les clients peuvent se connecter, lancer des parties et placer leurs bateaux, et je vais bientôt être obligé de coder la partie où ils tirent les uns sur les autres. Heureusement, j’ai glissé des variantes polymorphes pour que le type des fonctions reflète le protocole de communication.

J’aime bien l’expression problem, 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 vraiment besoin, on évite d’utiliser ces constructions plus délicates.

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.

Produits d’opérations

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 boilerplate). En effet :

• 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 ;

• 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 expr, 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 expr2 en lançant une erreur si on tombe sur une somme, ce qui n’est pas très propre.

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.

Actuellement, les programmes sont centrés autour des données : on définit leur type, et on exprime ensuite, a posteriori, 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.

On peut voir la situation complètement différemment en se plaçant du point de vue des opérations : 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.

type ops =
  { eval : int;
    print : string }

Voici nos opérations : l’évaluation, dont le résultat est un entier, et l’affichage.

let int n =
  { eval = n;
    print = string_of_int n }

Voici une donnée. Citoyen de seconde zone ! C’est une fonction qui construit les opérations quivontbien.

let add a b =
  { eval = a.eval + b.eval;
    print = sprintf "(%s + %s)" a.print b.print }

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.

let eval_test = (add (int 1) (int 2)).eval

Ça marche. Mais comme on est coquet :

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))

Ça marche et, du point de vue de l’utilisateur, rien n’a changé.

Maintenant, on essaie d’étendre nos opérations. On va rajouter l’opération rpn (notation polonaise inversée) que je vous ai brièvement présentée avec les types sommes simples.

type ops2 =
  { rpn : Buffer.t -> unit;
    ops : ops }

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 :

let rpn ops2 =
  let buf = Buffer.create 47 in
  ops2.rpn buf;
  Buffer.contents buf

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.

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

On peut encore étendre nos données et nos opérations, en rajoutant une donnée mul pour la multiplication.

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)))

Caractéristiques de l’approche produit

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.

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.

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.

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.

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.

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 :

• 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 ;
• implémenter l’opération à partir de l’arbre, dans un style plus direct.

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.

POO et motifs de conception

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.

Dans un langage plus POO, la structure que j’ai mise en place dans la dernière partie correspond au motif Composite. Dans ce motif, on définit une interface qui décrit les opérations, puis une classe pour chaque donnée :

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

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’héritage :

class type expr2 = object
  inherit expr
  method rpn : Buffer.t -> string
end

On peut alors appeler directement les méthodes eval et print sur des objets vérifiant l’interface expr2, sans devoir passer par une couche d’indirection (le .ops 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 composition qui est souvent considérée par les programmeurs POO comme plus adaptée que l’héritage dans un grand nombre de cas.

Approche somme en POO

J’ai présenté cette vision POO du problème, qui correspond au motif Composite. 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 Visiteur : au lieu de mettre les opérations dans les méthodes, on met les données.

L’idée est la suivante : on imagine chaque donnée comme un lieu que l’on peut visiter ; chaque donnée est chargée de coder une fonction accept qui appelle une méthode adaptée du visiteur :

let int n = object
  method accept visitor = visitor#int n
end

let add a b = object
  method accept visitor = visitor#add a b
end

Ces fonctions accept prennent des visiteurs en argument, et leurs donnent leurs composants. Chaque opérateur est un visiteur :

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

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).

À chaque fois que je veux rédiger une réaction, c’est la même chose : je vais voir dans ma liste de publications pour voir ce que je pourrais traiter. Il y en a qui m’ennuient, qui sont trop techniques pour être agréables, ou encore d’autres qui sont très tentants, mais dont je sais qu’ils demanderont beaucoup de travail, par exemple parce qu’ils sont suivis de quelques annotations « commencer par relire ceci et cela, ne pas oublier de mentionner aussi ceci et cela », etc.

Et là, je tombe sur la publication qui me tente : pas trop difficile, je sens que j’ai envie des choses à dire mais pas trop. Je vais le relire et ça commence typiquement par un « haha, il est super clair, je vais mettre deux lignes d’introduction, un résumé, et hop je les envoie le lire ». Mais le malheur arrive vite : les remarques indispensables s’accumulent, je me pose de nouvelles questions, je commence à expérimenter de mon côté, et quatre heures après j’ai un tas de code bizarre dans un fichier, et rien d’écrit.

Cette fois-ci, ça a tellement bien marché que je ne vais vous citer aucune publication dans ce billet : les développements préliminaires méritent un billet à eux tout seul, et sont assez lourds pour qu’une publication en plus frôle l’indigestion. Je ferai donc un billet suivant, et pour me racheter j’y citerai non pas une publication, ni deux, mais trois. Beware!

Édit : je vous écris depuis le futur pour vous signaler qu’un développement inattendu a nécessité la création d’un deuxième billet préliminaire. Les liens seront donc pour le troisième billet.

Pour profiter de ce billet, vous devez savoir lire du code en Objective Caml.

Types, opérations et extensibilité

Qu’est-ce qu’une structure de données en informatique ? C’est une question essentielle quand on veut programmer, et la réponse, en gros, on l’a, ma bonne dame, ce sont les types algébriques :

• une structure de donnée peut se présenter sous plusieurs formes différentes ;

• sous chaque forme, elle est composée d’un certains nombres de composants, qui sont aussi des données, mais pas forcément de la même sorte.

Par exemple, quelqu’un dans une école est soit un élève, soit un professeur. Si c’est un élève, il est caractérisé par son nom, son âge, et la marque de ses chaussures. Si c’est un professeur c’est la matière, la note moyenne, et le nom de ses antidépresseurs. Bien sûr, ce n’est qu’un modèle donné pour un problème donné, un modèle étant par définition réducteur : si on s’intéresse à d’autres aspects de la même chose (les personnes présentes dans une école) on pourra être amené à faire d’autres distinctions, ajouter des informations dans chaque cas, ou au contraire approximer en enlevant des informations (les profs, tous des salauds !). Ne vous laissez pas influencer par les gens qui prétendent que leur modèle décrit vraiment la nature profonde du monde matériel : en particulier, si vous croyez qu’en envoyant à un élève au hasard un message pour lui demander son nom, il va répondre (et, le cas échéant, que la réponse sera bien typée)…

Bref, les types algébriques des langages fonctionnels typés, c’est bon, mangez-en. Ce n’est pas la solution ultime (ça n’existe pas) et ça ne suffit pas toujours, mais c’est une solution générale et commode dans la plupart des cas. Qu’on se mette d’accord tout de suite : quand un type a plusieurs composants accessible simultanément (il a un champ foo et un champ bar), je parle de type produit, comme le produit cartésien en mathématiques (un couple avec un élément de chaque), et quand on a un choix (c’est soit un foo, soit un bar) je parle de type somme, comme la somme disjointe de deux ensemble en mathématiques. On peut évidemment faire des combinaisons, par exemple des sommes de produits (c’est soit un nom et une adresse, soit un identifiant et une adresse web), ou des produits de sommes (c’est, d’une part, un numéro de téléphone ou une adresse mail, et d’autre part un site web ou rien du tout).

Les types algébriques c’est le bien, mais comment fait-on si on a besoin de changer un peu les informations sur notre type (par exemple on veut rajouter un cas « personnel de la cantine ») ? Facile : On change notre type algébrique. Et comme on est dans un langage fortement typé, le compilateur va repérer^α tous les endroits de notre code où on utilise ce type, puisque leur typage sera devenu incorrect, et nous donner leur position pour qu’on les modifie pour prendre en compte le changement de type, un par un, il nous prend par la main et ça simplifie énormément la maintenance^β du programme.

Ça ne marchera pas si les modifications n’impliquent pas de changement incompatible du type (par exemple on remplace un composant de type entier par un composant de type entier, qui n’a pas la même signification), mais là c’est que vous le faites exprès : vous avez un langage au typage expressif, profitez-en pour que vos types soient un peu précis !

Expression problem

Maintenant, comment faire si on envie de rajouter des informations, mais sans modifier le code existant ? Ça arrive quand vous avez le malheur d’utiliser une bibliothèque propriétaire (mais alors c’est de votre faute), ou même que ça demanderait de modifier une bibliothèque et que vous n’avez pas envie de maintenir un fork, ni de justifier vos changements upstream (ou qu’ils les refuseraient de toute façon car ils cassent la compatibilité avec l’existant), bref que le type existant n’est pas de vous. Ou tout simplement que vous n’avez pas envie de devoir recompiler le code existant, car votre compilateur est terriblement lent.

Pour ajouter des cas à un type somme (par exemple ancien_type), sans le modifier, on définit un nouveau type somme :

type nouveau_type =
  | Ancien_cas of ancien_type
  | Nouveau_cas of nouvelles_informations

On peut ensuite définir de nouvelles opérations, et il est utile de faire du filtrage de motif sur les objets^γ de type nouveau_type :

match ma_donnee with
  | Ancien_cas ancienne_donnee -> ...
  | Nouveau_cas nouvelle_donnee -> ...

Dans les premiers ... on met le traitement à effectuer sur les anciennes valeurs (on réutilise souvent directement les fonctions de traitement définies sur l’ancien type), et dans les deuxièmes on gère le nouveau cas. C’est clair (quand on l’habitude), commode, expressif^δ, bon pour la peau, etc.

Cette méthode a quand même ses limites. Déjà elle est un peu lourde (à l’écriture, et à l’exécution) parce qu’on rajoute une nouvelle couche de distinction de cas à chaque fois (là ça va mais après trois ajouts vous devrez faire trois distinctions successives…), mais aussi des problèmes plus profonds que vous verrez en partie dans le reste de ce billet. Ça a poussé les chercheurs en langages de programmation à expérimenter de nouvelles façon d’exprimer la chose, et c’est ce qu’on appelle l’expression problem :

Comment définir des données et les opérations sur ces données, tout en pouvant ensuite ajouter des données et des opérations, sans modifier le code existant ?

Chacun a apporté sa petite solution, et la compare à celle des autres. Elles sont plus ou moins compliquées, et plus ou moins solutionnesques (certaines gèrent des choses que les autres ne gèrent pas, et chacun prétend que son petit plus est déterminant). Je ne compte pas apporter une solution dans ce billet, mais plutôt développer la question par des essais successifs, pour vous faire sentir son intérêt et une partie des difficultés.

Fil conducteur

On s’intéressera dans ces billets au problème de l’extensibilité dans le cas particuliers d’expressions arithmétiques simples. Je présenterai différentes façon de représenter des nombres, des sommes, de calculer leur valeur ou de les afficher non calculées, éventuellement des produits (extensibilité des données) ou d’autres opérations.

Avec des types somme

On commence par des expressions qui sont soit des nombres, soit des sommes d’expressions :

type expr =
  | Int of int
  | Add of expr * expr

On peut facilement définir une fonction d’évaluation et d’affichage :

let rec eval = function
  | Int n -> n
  | Add (a, b) -> eval a + eval b

let eval_test = assert (eval (Add (Int 1, Int 2)) = 3)

let rec print = function
  | Int n -> string_of_int n
  | Add (a, b) -> sprintf "(%s + %s)" (print a) (print b)

let print_test = assert (eval (Add (Int 1, Int 2)) = "(1 + 2)")

Pour la deuxième fonction il faut ouvrir le module Printf. Je donne le code en OCaml pour montrer que ce n’est pas que du vent, mais ne vous focalisez pas sur de petits détails (pourquoi renvoyer une chaîne ? et la concaténation ça coûte cher ? blablabla).

Comme vous pouvez le voir, rajouter une fonction, c’est très facile, tellement qu’on n’y pense même pas (tous les langages n’ont pas la même chance). Par contre, si on veut étendre les données, pour ajouter le produit d’expressions, ça coince :

type expr2 =
  | Expr of expr
  | Mul of expr2 * expr2 

Epic fail! En effet, ce type ne correspond pas à ce qu’on veut : on peut rajouter des multiplications par dessus des valeurs existantes, mais pas l’inverse : on ne peut pas dire Add (Mul (..), ..), car Add prend des paramètres de type expr, et Mul n’en fait pas partie, il n’est que dans le type expr2. Dans certains cas spécifiques ce comportement est utile, mais ici on veut pouvoir mélanger les multiplications et les additions, donc ça ne va pas. On est arrivé à une limite de la méthode d’extensibilité par types somme : utilisée naïvement, elle supporte très très mal les données récursives (ici le problème c’est que le type expr fait référence à lui-même, et pas à expr2).

Frustré, vous décidez de rajouter une opération, nah.

(* notation polonaise inversée *)
let rpn expr = 
  let buf = Buffer.create 37 in
  let print fmt = bprintf buf (format_of_string fmt) in
  let rec rpn = function
  | Int n -> print "%d " n
  | Add (a, b) -> 
      rpn a; rpn b;
      print "+ " in
  rpn expr;
  Buffer.contents buf

let test_rpn = rpn (Add (Int 1, Int 2))

Types somme ouverts

Examinons le code suivant.

type expr =
  | Int of int
  | Add of expr * expr

type expr2 =
  | Expr of expr
  | Mul of expr2 * expr2 

Le deuxième type ne fait pas ce qu’on voudrait, parce que le type expr est fermé : on a fixé le type de ses composants et il refuse d’en accepter de nouveaux. On peut essayer de s’en sortir en le forçant à s’ouvrir, c’est à dire en rajoutant un paramètre de type :

type 'a _expr =
  | Int of int
  | Add of 'a * 'a

Je mets le mignon petit _ devant pour montrer que c’est un type ouvert, tolérant, hippie quoi. On pourrait maintenant avoir un type expr2 convenable :

type expr2 =
  | Expr of expr2 _expr
  | Mul of expr2 * expr2

La partie « ancienne » de expr2 accepte maintenant des composants de type expr2 : on peut mettre des multiplications dans les additions, mission accomplie. Mais il ne faut pas brusquer les choses, on va commencer avec juste _expr, et s’intéresser à l’ajout d’opérations.

let _eval eval = function
  | Int n -> n
  | Add (a, b) -> eval a + eval b

Vous remarquez sans doute un paramètre supplémentaire, eval : en effet les sommes contiennent un composant 'a à priori inconnu, et on ne sait pas comment l’évaluer : on prend donc en paramètre une fonction auxiliaire eval qui sait évaluer le type 'a. C’est charmant mais ça ne nous dit pas comment évaluer les expressions avec juste des additions et des nombres qu’on essaie de manipuler : il faut une version fermée du type _expr :

type expr = Fix of expr _expr

Toute ressemblance avec un point fixe de récursion serait purement fortuite. Ça revient à définir un type d’expressions qui se contient lui-même : on est en fait revenu au type récursif fermé expr de départ, mais avec un constructeur explicite pour la récursion car sinon le compilateur râle (ou alors il faut ajouter l’option -rectypes).

Dans le même genre tying the knot, on a l’évaluateur d’expressions fermées :

let rec eval (Fix expr) = _eval eval expr

let eval_test = eval (Fix (Add (Fix (Int 1), Fix (Int 2))))

C’est quand même un peu lourd à écrire, donc on définit du sucre syntaxique sous forme de smart constructors :

let _int n = Int n
let _add a b = Add (a, b)
  
let int n = Fix (_int n)
let add a b = Fix (_add a b)

let eval_test = eval (add (int 1) (int 2))

On a bien l’extensibilité des opérations, maintenant on récolte les bénéfices de toutes ces complications avec l’extensibilité des données :

type 'a _mul_expr =
  | Expr of 'a _expr
  | Mul of 'a * 'a

let _mul_eval (!) = function
  | Expr e -> _eval (!) e
  | Mul (a, b) -> !a * !b

Deux remarques. J’ai choisi une forme ouverte pour mul_expr, puisque cela permettra de l’étendre elle aussi si le besoin s’en fait sentir (heureusement pour la longueur de ce billet, il ne se fera pas sentir, mais imaginez ! :pirate:). J’ai choisi le rigolo nom (!) pour la fonction d’évaluation prise en paramètre parce qu’on peut l’utiliser comme opérateur infixe, c’est amusant.

Smart constructors, on ferme la récursion, et on profite :

let _int n = Expr (_int n)
let _add a b = Expr (_add a b)
let _mul a b = Mul (a, b)

type mul_expr = Fix2 of mul_expr _mul_expr
let rec eval (Fix2 expr) = _mul_eval eval expr

let int n = Fix2 (_int n)
let add a b = Fix2 (_add a b)
let mul a b = Fix2 (_mul a b)

let eval2_test = eval (add (int 1) (mul (int 2) (int 3)))

Vous notez que je ne vous ai pas arnaqués, en faisant sans le dire à nouveau le travail effectué pour le premier type (si on doit introduire des redondances, ce n’est plus de la vraie extensibilité) : j’ai défini les nouveaux constructeurs _int et _add en fonction des anciens, de façon mécanique et indolore : on n’a pas à connaître leur signification (juste leur arité) ou, pire, leur implémentation.

Pour enfoncer le clou sur l’extensibilité, on se reconvainc de l’extensibilité des opérations avec une fonction print sur le tard :

let _print print = function
  | Expr (Int n) -> string_of_int n
  | Expr (Add (a, b)) -> sprintf "(%s + %s)" (print a) (print b)
  | Mul (a, b) -> sprintf "(%s * %s)" (print a) (print b)

let rec print (Fix2 expr) = _print print expr
let print_test = print (add (int 1) (mul (int 2) (int 3)))