Ours & Hippy — le blog

Pourquoi le C est moins puissant que votre langage favori

2010-03-27T02:38:35+01:00

On entend souvent dire que l’on peut tout faire dans un langage comme dans un autre, Turing-complétude, tout ça. La variante de ce discours est que l’on peut tout faire en C parce que c’est un langage de bas niveau. Certes, on peut tout faire, mais on ne peut pas tout faire aussi bien, c’est-à-dire aussi efficacement.

Ainsi, avant de poursuivre avec mes articles sur les techniques de programmation en C, j’ai décidé de prendre le temps d’écrire un court billet sur ce que l’on ne peut pas faire en C. Ce petit texte n’a pas pour prétention d’être exhaustif, car la liste de ce que l’on ne peut pas faire en C est sûrement longue, très longue. Mais je souhaite donner ici quelques points de réflexion et principes de base, pour les plus débutants d’entre nous.

Le problème

Pourquoi donc ne peut-on pas faire aussi efficacement en C certaines choses que l’on peut bien faire dans un autre langage ? La réponse tient en cela : l’abstraction.

L’argument que l’on entend souvent est le suivant : le C étant plus bas niveau, il suffit de recoder les mécanismes internes abstraits par tel ou tel langage de plus haut niveau. Je suis d’accord avec cette méthode, je l’aime même beaucoup, étant moi-même assez spécialisé dans l’implémentation des langages. Mais il est important d’en connaître les limites.

Les limites, ce sont les limites de définition du langage. Si l’on veut utiliser le C comme un langage raisonnablement portable, et que l’on s’en tient à la norme, on hérite par la même occasion de contraintes normées, plus fortes que celles imposées par la plateforme pour laquelle on développe.

Concrètement, cela signifie que sur une machine donnée, votre beau C portable ne pourra pas recourir aux mêmes astuces que l’implémentation d’un langage de plus haut niveau (qui, elle, n’est pas portable). Prenez par exemple les variables de Scheme, ou tout autre langage dynamique. Dans ces langages, une variable peut pointer sur un objet, ou contenir une valeur numérique unboxed. En profitant de la représentation des pointeurs au sein du système hôte, et du fait que la mémoire n’y est jamais allouée que sur un alignement de 2, on peut utiliser un bit pour déterminer la nature de l’objet (boxed ou unboxed).^α C’est malin comme tout, et vieux comme le monde. Mais inapplicable en C. Question de portabilité. En effet, on n’a même pas la garantie que les pointeurs soient convertibles en entiers !

Mais, mais, me direz-vous, en Scheme non plus, on n’a pas cette garantie ! Oui… mais en Scheme, il n’y a pas de pointeurs comme en C ! Autrement dit, le programmeur s’en contrefiche : il utilise simplement son langage, et c’est au compilateur de décider comment telle ou telle fonctionnalité est traduite au niveau de la machine ; du point de vue du langage, on a perdu…

α : Ce n’est pas un article sur l’implémentation des langages, voyez la page Wikipédia sur l''unboxing', si vous n’êtes pas à l’aise avec ces notions.

La solution ?

Mais on n’a qu’à implémenter des solutions spécifiques en plus de la version générale moins efficace ! C’est en effet une possibilité.

Par exemple, pour les objets dynamiquement polymorphes pointeurs / entiers, on pourrait se définir un petit jeu de macros dans ce genre-là :

#include <stdint.h>

#if UINTPTR_MAX && HAVE_2ALIGNPTRS

typedef uintptr_t VariantInt;
typedef uintptr_t Variant;

#define ISINT(x) ((x) & 0x1)
#define INTVAL(x) ((x) >> 1)
#define PTRVAL(x) ((void *)(x))
#define SETINT(x, y) ((x) = (y) << 1 | 0x1)
#define SETPTR(x, y) ((x) = (uintptr_t)(y))

#else

#if UINTPTR_MAX
typedef uintptr_t VariantInt;
#else
typedef long VariantInt;
#endif
typedef struct {
        union {
                VariantInt _int;
                void *_ptr;
        } _val;
        unsigned _isint: 1;
} Variant;

#define ISINT(x) ((x)._isint)
#define INTVAL(x) ((x)._val._int)
#define PTRVAL(x) ((x)._val._ptr)
#define SETINT(x, y) ((x)._val._int = (y), (x)._isint = 1)
#define SETPTR(x, y) ((x)._val._ptr = (y), (x)._isint = 0)

#endif

Bref, un truc du genre. Pas le plus beau jeu de macros du monde, mais vous comprenez le principe.

Et vous vous attendez sans doute maintenant à ce que je réfute cet argument… et bien non ! En réalité, c’est une manière parfaitement viable d’étendre un peu le langage. Cependant, elle requiert quelques précautions.

Elle demande d’être méthodique, en cela qu’il faut patiemment écrire une macro (ou une fonction) pour abstraire chaque opération affectée par le changement d’implémentation. Cela peut être long, fastidieux, et si l’on teste plus une implémentation qu’une autre, on court le risque de se laisser biaiser, et d’oublier d’isoler des fonctionnalités qui devraient l’être.
Elle tend à faire basculer les meilleurs programmeurs du côté obscur de la non-portabilité. :-° En effet, certains hacks marchent tellement biens que l’on est vite tenté de se dire qu’il ne sert à rien de maintenir une version générique, sous-optimale, mais conforme à la norme. Et c’est là un gros risque ! Parfois, on peut effectivement se laisser aller…
C’est une question subjective, et je ne peux certainement pas décider à votre place. Je ne peux que vous offrir une règle générale que je m’applique de manière plus ou moins stricte :
Plus le code se veut général (bibliothèques, composants réutilisables), plus il est important de maintenir une version standard, portable, de l’implémentation.
Un avantage de cette stratégie est que vous pouvez en toute tranquillité utiliser l’implémentation simple, non optimisée, par défaut, et doucement migrer les différents systèmes, au cas par cas, vers votre code spécialisé, au fur et à mesure de vos tests (ou de ceux de vos utilisateurs !).
Mais bien sûr, il ne faut pas se focaliser sur la portabilité, qui, de toute manière, est toute relative. En effet, si, par exemple, votre application dépend déjà fortement d’une bibliothèque tierce, telle que la GLib, qui elle-même fait certaines hypothèses sur l’implémentation, il peut être raisonnable de vous appuyer dessus.

Que retenir de tout ça ?

Au final, je dirais, pas grand chose, si ce n’est que j’essaierai, pour ma part, d’être précis quant aux implications des méthodes que je décris. Ce n’est pas (seulement) pour être pédant ; je pense qu’il est réellement important de comprendre (pour mieux ignorer, dirons certains) les limites des définitions et des standards que l’on accepte, parfois sans le dire.

À bientôt donc, pour de nouvelles aventures ! :)

Cohérence des effets de bord

2010-01-22T22:59:16+01:00

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.

Pourquoi attacher tant d'importance au typage ?

2009-12-30T13:34:33+01:00

La réponse, enfin dévoilée ! Bluestorm Origins: The Typing Mystery, maintenant dans les blogs (well, le nôtre du moins :-°). —rz0

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.

α : On pourrait croire à une circularité ici : si les types parlent du langage tout en en faisant partie, alors les types parlent des types et le monde s’écroule. En réalité, la plupart des langages de types ne sont pas suffisamment expressifs, et ne parlent que d’une partie restreinte du langage (qu’on appelle souvent les valeurs). Mais il existe effectivement des langages (par exemple Coq) dans lesquels les types ont eux aussi un type, qui a à son tour^β un type… Il peut bien sûr exister un nombre infini de types différents, bien qu’un programme donné ne les utilise pas tous en même temps.

β : « Turtles all the way down ! » ;-)

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

γ : En fait, PLT Scheme permet aussi la vérification des types ; je suis impressionné par cette implémentation de Scheme.

δ : Je parle ici de la sémantique du langage, c’est à dire d’une définition un peu abstraite du comportement (ou sens) des programmes. Ce n’est pas une question d’implémentation : si on crée un compilateur pour un langage avec cette séparation, on peut très bien choisir de faire des optimisations en raisonnant sur le type des variables, par exemple en changeant leur représentation mémoire (boxing, etc.), du moment que cela crée aucune différence de comportement du programme observable par le programmeur.

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.

ε : Limitation qui n’en est pas toujours une : on peut faire des choses très intéressantes avec des langages non Turing-complets (par exemple les expressions régulières/rationnelles, quand elles le sont vraiment, ou Coq).

ζ : Jacques Guarrige, Code reuse through polymorphic variants

The idea for this example originally comes from a post by Phil Wadler on the Java-Genericity mailing list W+98, in which he proposed a solution to the Expression Problem, that is the problem of extending a variant type with new constructors without recompiling code for old ones. A similar problem and solution can be found in KFF98, but untyped. It appeared later that Wadler’s solution, which already supposed an extension of Generic Java, itself an extension of Java, could not be typed. Didier Rémy, Jérôme Vouillon and myself finally came up with a typable solution in an object-oriented extension of the 3rd order typed lambda-calculus, which was later checked correct by Haruo Hosoya in F-omega- sub-rec. On the other hand, I could provide a much shorter solution in about 15 lines of Objective Label using polymorphic variants, which were merged later in Objective Caml. The solution used only standard ML-polymorphism, which is a weakened 2nd order typed lambda-calculus, and can be inferred automatically.

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.

η : Rz0 me signale que cette « meilleure compréhension » n’a pas du tout affecté la pratique des programmeurs qui, sur le terrain, utilisent des effets de bords, et qu’il est donc un peu « osé » de présenter les monades comme une réussite de ce point de vue. C’est en effet un peu plus compliqué que ça : notre compréhension théorique des effets de bords s’est améliorée, mais on a aussi découvert que les monades sont des outils trop généraux, qu’elles s’appliquent à beaucoup de choses qui ne sont pas considérées habituellement comme des effets de bords, et qu’elles ne sont pas toujours assez précises.

Pour la gestion de la mémoire par exemple, une monade ne peut pas raisonner, au niveau du typage, sur l’étendue des zones mémoires affectées par un programme : la monade saura dire de deux programmes qu’ils modifient la mémoire, mais pas si les zones de mémoire qu’ils utilisent sont disjointes ou s’il y a des interactions entre les deux. On a besoin de ces propriétés plus fines, et on est en train de développer des outils plus spécialisés et plus complexes, comme les systèmes d’effets et les logiques de séparation.

Enfin, même si ces idées mettent du temps à sortir de leur cadre théorique pour atterrir dans la boîte à outils des programmeurs, elles restent présentes dans l’industrie, avec par exemple les outils d’analyse statique de programmes, qui suivent d’assez près les progrès de la recherche dans ce domaine. L’arrivée du concept dans un langage de programmation grand public est la dernière étape (après l’entrée dans les langages expérimentaux comme DDC ou ATS), qui se fera plus tard, ou peut-être pas du tout, si l’on constate que les bénéfices de ces méthodes ne compensent pas l’ajout en complexité.

η´ : Et puis d’abord, si l’exemple des monades ne vous plaît pas, en voici un autre : les continuations. Le comportement dynamique de call/cc est bien connu, mais l’étude de son lien avec le typage et la logique classique est au moins aussi intéressante.

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.

θ : Voir par exemple les travaux de Greg Morrisset ou George Necula sur les assembleurs fortement typés.

La réaction de rz0 de sujet souligne un autre aspect du problème :

À mon avis, un point intéressant, et pas du tout développé dans la plupart des visions « haut niveau » de l’assembleur, c’est les contraintes sur les adresses ou la mémoire : représentation, décalage, facteur, taille, alignement, granularité, etc. Je considère que c’est du typage aussi, et c’est du typage « utile », dans le sens où si les données fournies aux opérandes sont mal typées, soit ça n’assemble pas (p.ex. parce qu’il n’y a pas assez de bits pour représenter l’adresse entièrement), soit ça balance une exception au runtime (si on passe un registre et que sa valeur ne vérifie pas les conditions de typage). Bref, je trouve que ce n’est pas « rien à dire ».

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.

ι : Un anglicisme qui désigne le « moment de l’exécution », à nuancer de compile-time ou parse-time, et dont j’ai beaucoup de mal à me débarrasser.

κ : C’est ce que j’ai utilisé dans Macaque ; j’avais besoin d’une méthode sûre pour traiter la perte de typage des données passant par le serveur SQL (qui n’utilise que des chaînes de caractères), et je me retrouvé, sans m’en rendre compte au départ, avec du typage dynamique fait maison.

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

On peut remarquer que cette approche (construction automatique, par le langage directement, de la description runtime de type) brise la propriété de séparation, que j’ai évoquée précédemment, entre la phase de typage et la phase d’exécution.

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.

λ : Même si vous seriez sans doute surpris par la quantité de chose qu’on peut présenter sous forme d’un typage, ou en relation avec le typage : sécurité, performances, invariants de structures de données, etc.

En bref

2009-11-16T11:23:15+01:00

Et non, le blog n’est pas mort, ahem, enfin. bluestorm et moi sommes juste très occupés. Mais, au détour d’une discussion IRC, il m’a convaincu de dire deux mots sur le nouveau machin de Google (Go). Je peux en profiter pour dire deux mots sur le pas-si-nouveau-que-ça machin d’OS X (GCD). Et oui, que voulez-vous, on n’est pas vraiment in sync with da hype.

Honnêtement, je n’ai pas grand chose à dire, là-dessus. Globalement, comme presque toujours, je suis sceptique (not impressed), surtout pour Go. Pour citer bluestorm, « la syntaxe ne casse pas de briques ». En fait, je ne vois pas l’intérêt de la nouvelle syntaxe ; la rationale est franchement faiblarde et l’intérêt que je vois à maintenir une certaine compatibilité avec les autres descendants syntaxiques du C (Java, C#, etc.) aurait largement justifié de ne pas dévier à ce point. Mais pourquoi s’attarder sur la syntaxe, après tout… bah parce que du reste, je ne suis pas franchement convaincu par la nouveauté de ce langage, qui n’est pas sans rappeler, à mon avis, Alef, pour le côté « on rajoute des machins au C pour gérer la concurrence et quelques types de données pratiques ». Bref, à mon avis, les vieux gurus risquent un peu trop leur peau, du moins leur réputation, en jouant à ce jeu-là.

Le machin d’Apple est sans doute plus rigolo, et ça a l’avantage d’être déployé, et blah et blah. Je n’ai rien contre le principe : on a vraiment besoin d’outils pratiques pour faire de la concurrence en C… par contre je conchie ((c) conno) la syntaxe des blocs de clang. Je trouve que ça ne ressemble pas à du C, et que l’on aurait pu utiliser une syntaxe dérivée des littéraux composés du C99 (quelque chose comme (T (args)){ ... }), quitte à ajouter un qualificateur particulier (fat ? :p) pour les pointeurs de blocs (après tout, ils le font déjà pour les variables lexicalement accessibles de manière imbriquée). Pourquoi ? Parce qu’avec une syntaxe comme celle qui est actuellement implantée, aussi distante du C classique, je vois mal comment on pourrait voir ce genre de fonctionnalités devenir ne serait-ce que vaguement standard un jour ! J’ai toujours voulu avoir des fermetures lexicales en C… et je pense que les idées sous-jacentes ne sont pas dégueulasses, mais je prie pour que cette syntaxe-là ne devienne jamais quelque chose que l’on pourrait appeler, en toute bonne foi, du C.

…et pendant ce temps-là, au p^W^W blue, lui, se touche plutôt sur ATS. Ne m’en demandez pas trop, je n’ai pas vraiment eu le temps de regarder en détail, mais à vue, c’est hum, un nouveau langage avec une syntaxe fonctionnelle et une théorie sous-jacente probablement trop-bien-et-tout-aussi-compliquée.

Voilà, voilà, à bientôt, pour de nouvelles aventures !

L'innocence est un mythe : les programmes fonctionnels nécessairement impurs

2009-08-21T16:49:00+02:00

Tut tut tut, deuxième réaction de bluestorm dans les bacs. Après ses aventures avec la petite Emily, notre héros nous revient en terrain familier et, par ce discours nouveau, introduit la jeunesse à une des dures réalités de la vie d’un guerrier fonctionnel, dans sa quête éternelle de la meilleure conception, chassant les belles factorisations… tak tak.

Mais je vais éviter de m’imposer davantage sur son billet de peur de le vexer, puisque j’ai déjà pris la liberté d’amender son titre originel tout meugnon.

—minh

Cette réaction n’est pas la deuxième sur ma liste : c’est la quatrième, et je l’ai choisie parce que c’est un sujet qui me tentait plus. C’est un papier sur les programmes et langages de programmation, qui repose sur un arrière-plan théorique complètement inaccessible (pour moi en tout cas), mais qui cache toutes ces difficultés et qui est orienté vers une certaine forme de pratique.

Le papier explore un fait qu’il considère comme « surprenant » : il existe des fonctions qui respectent la transparence référentielle, mais qu’on ne peut pas écrire dans un langage de programmation pur ; autrement dit, il parle de la programmation fonctionnelle qu’on ne peut faire que dans un langage (un peu) impératif. Il donne des exemples de ces fonctions, se demande à quoi elles peuvent bien servir, donne des cas d’utilisation et discute de leurs avantages et inconvénients par rapport aux fonctions écrites dans un langage pur, d’une part, et aux fonctions générales d’autre part.

Il aborde aussi de façon relativement tangente deux points que je trouve intéressants :

parfois, pour qu’une fonction ait de bonne propriétés, il faut lui faire perdre une partie des informations qu’elle donne, en fournissant pour cela un travail supplémentaire ;
l’écriture dans un style fonctionnel pur peut poser des problèmes de modularité.

When is a functional program not a functional program
Citeseer (PDF, PS), 7 pages
John Longley

Ce n’est pas un papier révolutionnaire dans le sens où les techniques présentées ne changeront pas fondamentalement votre vision de la programmation, mais ça reste une lecture agréable et à placer dans la catégorie "exercices mentaux de programmeurs ML".

Le reste de cette réaction est une explication plus détaillée et plus verbeuse de tous les points que j’ai évoqués jusqu’ici. C’est donc une paraphrase de l’article, avec des choses en moins, mais je pense que c’est plus accessible : ce qui dans l’article constitue une petite allusion d’une ligne (« the familiar recursive type », « in the obvious way », « in the usual sense »…) sera un peu plus détaillé et donc normalement plus accessible au lecteur qui ne connaît pas le sujet, même si je ne ferai sans doute pas de miracles. En pensant aux gens qui n’ont pas envie d’entrer trop dans les détails, j’ai retiré une partie de mes digressions et les ai mis en annexe ; ça casse un peu le flot naturel du discours, mais vous pouvez très bien ne pas les lire, ou les lire seulement à la fin si vous voulez des détails. C’est même ce que je vous conseille : lisez-les quand vous aurez terminé le corps de l’article et si vous en avez encore envie, c’est le plus simple.

Par contre, je donne des exercices dans ce billet. Si cela peut vous motiver, au milieu de mes explications à la noix vous trouverez des énoncés d’exercices pas tous évidents, qui pourront vous faire un petit challenge matinal en mangeant vos chocapics (ou pas).

Des fonctions fonctionnelles non pures

L’article se place dans le cadre de langages dont les fonctions peuvent "échouer", c’est à dire ne pas renvoyer de valeur : boucler à l’infini, renvoyer une erreur/exception, etc. C’est le cas de tous les langages Turing-complets,^α donc tous les langages que l’on manipule en général. On dit dans ce cas que la fonction diverge, ou n’est pas définie. Le bon outil mathématique pour étudier les fonctions dans ces langages est le concept de fonction partielle : une fonction partielle de A vers B (où A et B sont des ensembles au sens mathématiques du terme) est une fonction qui renvoie, pour tout élément de A, soit un élément de B, soit ⊥, qui représente l’échec, la divergence. Si on évalue une fonction (informatique) en un argument où elle n’est pas définie, l’ensemble du calcul diverge : si par exemple l’évaluation de la fonction boucle à l’infini (ne termine pas), le reste du programme n’est jamais exécuté et l’ensemble boucle à l’infini.

α : la notion de Turing-complétude permet d’étudier l’expressivité d’un langage pour écrire des fonctions de type int -> int ; comme expliqué dans l’article, on peut voir les fonctions présentées ici comme une extension de la notion Turing-like de calcul aux autres types fonctionnels.

Ce point de vue explique aussi la prépondérance du type int dans l’article. Il utilise par exemple souvent des fonctions de type int -> int alors qu’une fonction int -> 'a aurait été plus générale et plus appropriée ; j’ai choisi de respecter ce choix, ne vous étonnez pas de voir des types inutilement restreints.

En deux mots, on considère les fonctions du langage qui sont fonctionnelles, c’est à dire qu’elles se comportent vraiment comme une fonction partielle mathématique : pour chaque valeur possible en argument, elles renvoient toujours la même valeur, ou divergent toujours. On les appelle aussi séquentiellement représentables (SR) parce qu’elles englobent toutes les fonctionnelles que l’on peut définir dans un langage séquentiel, où il n’y a qu’un seul fil d’exécution. Concrètement, les fonctionnelles et les SR désignent ici les mêmes fonctions, mais quand je parle de fonctionnelle j’insiste sur le comportement mathématique (une sortie par entrée au plus), et quand je parle de SR j’insiste sur la possibilité de les implémenter dans un langage SR. De plus, on pourrait imaginer d’autres classes d’expressivité où des fonctions restent fonctionnelles mais ne sont plus SR (cas traité en annxe). Ou l’inverse (cas de la plupart des langages impératifs).

Formellement, on peut voir les fonctions partielles de A dans B comme des applications de A dans (B + {⊥}), où (+) représente la somme disjointe de deux ensembles. On peut alors définir une traduction des valeurs du langage de programmation vers des objets mathématiques : les fonctions du langage deviennent des fonctions partielles, et les types deviennent des ensembles. On note [u] l’objet mathématique représenté par le terme u, et ['a] l’ensemble qui représente le type 'a.

Les types et valeurs de base du langage sont traduits par les ensembles et éléments correspondants : [nat] = N, [bool] = {true, false}, [1] = 1, etc.
On définit ['a -> 'b] comme l’ensemble des fonctions partielles de ['a] dans ['b] qui sont implémentables dans notre langage de programmation

Plutôt qu’étudier directement les fonctions du langage, on étudiera donc les fonctions mathématiques correspondantes. Il peut y avoir de nombreuses implémentations différentes d’une fonctionnelle, mais on les considèrera toutes comme équivalentes si elles donnent les mêmes résultats pour les mêmes arguments, donc dénotent la même fonction mathématique.

Avec la définition que j’ai donnée, qui est celle du papier, les fonctions prennent en paramètre non pas un terme quelconque du langage, mais une valeur.^β Cela veut dire que les arguments doivent être évalués avant d’être passés aux fonctions, et on est donc dans un cadre d’évaluation stricte. On ne perd en fait aucune généralité, et si cela vous intéresse je parle un peu de l’évaluation paresseuse en annexe. En un mot, on peut représenter une valeur paresseuse de type t comme une valeur stricte de type unit -> t, donc cela reste dans le cadre de cette discussion.

β : par valeur on entend "terme qui s’évalue en lui-même" : valeurs immédiates (entiers, booléens), mais aussi structures et fonctions

L’intérêt de cette classe de fonction est apparent : si on sait qu’elles renvoient toujours le même résultat, on peut effectuer un grand nombre de transformations du code sans modifier sa signification, beaucoup plus que pour des fonctions qui n’ont pas cette propriété. Par exemple si un compilateur trouve le code f x + f x, où x est une valeur et f vérifie cette propriété, il peut le transformer en let y = f x in y + y. Cette optimisation correspond à une optimisation déjà effectuée par la plupart des compilateurs optimisants, la CSE (Common Subexpression Elimination) ; mais elle ne peut en générale être pratiquée que pour des expressions très simple (calculs numériques principalement) et pas pour les appels de fonctions, si leur résultat peut changer entre deux appels (certains compilateurs de langages impératifs, dont GCC, permettent cependant au programmeur d’annoter des fonctions pour préciser qu’elles sont fonctionnelles et peuvent être prises en compte par la CSE).

L’article repose en fait sur un deuxième article beaucoup plus long du même auteur, qui développe toute la partie théorique. J’ai essayé d’y jeter un coup d’oeil avant d’écrire cette réaction, et il est complètement indigeste. Exemples de mots clés : « full and faithful » (théorie des catégories), « presheaves » (algèbre), « hypercoherence » (?).

Exemple : fonction `use`

On s’intéresse à un type, que l’on notera (), qui a une seule valeur que l’on note u (type u = unit). On dénote () par un objet mathématique quelconque noté * : [u] = {*}.

Quels sont les éléments de [u -> u] ? Ces fonctions sont définies par leur valeur en le seul argument possible, *. On a donc deux possibilités :

(* -> ⊥), la fonction qui diverge, que je noterai 0
(* -> *), la fonction qui renvoie *, que je noterai 1

Cas `(u -> u) -> u`

Quels sont maintenant les éléments de [(u -> u) -> u] ? Quand on a en argument une fonction de type u -> u, on a trois possibilités :

diverger dans tous les cas : c’est la fonction [bot] : f -> ⊥,
par exemple let rec bot f : unit = bot f ;
renvoyer () dans tous les cas : c’est la fonction [top] : f -> *,
par exemple let top _ = () ;
évaluer l’argument en () puis renvoyer () : c’est la fonction [mid] : f -> f(*), par exemple let mid f = f ()
argument retour
0 ⊥
1 *
En effet, si on évalue 0(*), le calcul diverge (puisque 0 diverge), donc mid(0) est ⊥.

Il y a une quatrième fonction dans l’ensemble des fonctions partielles [u -> u] -> [u], c’est neg, qui termine pour 0 et diverge pour 1. Cette fonction n’est pas représentable,^γ car elle correspond en fait au théorème de l’arrêt : elle permettrait de "savoir" sans diverger si son argument diverge, ce qui est impossible dans tout langage Turing-complet. J’ai développé ce point en annexe.

γ : donc n’appartient pas à [(u -> u) -> u]

Cas `((u -> u) -> u) -> bool`

Nous arrivons maintenant au coeur du sujet. Quelles sont les fonctions représentables de ((u -> u) -> u) -> bool ? Ce sont les fonctions qui prennent bot, mid et top en paramètre et qui renvoient true ou false, ou divergent.

Quand on a un paramètre de (u -> u) -> u, on peut :

diverger dans tous les cas ;
évaluer en 0, puis renvoyer un booléen b :
paramètre retour
bot ⊥
mid ⊥
top b
évaluer en 1, puis renvoyer un booléen b :
bot ⊥
mid b
top b
renvoyer un booléen b dans tous les cas

Pour toutes ces fonctions, le choix du booléen b n’a pas d’importance : que ce soit true ou false, ça ne diverge pas et c’est tout ce qu’on en tire.

On peut cependant imaginer une autre fonction que l’on appellera use :

bot	⊥
mid	true
top	false

(on peut inverser true et false ici, ça ne change pas grand chose)

Cette fonction permettrait de différentier mid et top, bien qu’elles renvoient les même résultats sur la valeur où elles sont toutes les deux définies. On ne peut pas la coder dans un langage fonctionnel pur. On peut cependant l’écrire en Caml, en se basant sur l’observation suivante : il faut renvoyer true si et seulement si la fonction "utilise" la fonction u -> u qui lui est passée en paramètre.

let use f =
   let used = ref false in
   f (fun () -> used := true);
   !used

Le code utilise un effet de bord, mais la fonction est bien fonctionnelle et appartient donc à la classe SR.

Exercice (plutôt facile)
Coder use en utilisant des exceptions à la place des références.

Cet exercice, ainsi que les suivants, demande d’écrire une fonction. Vous pouvez le faire dans le langage que vous voulez. L’auteur de l’article le ferait sans doute en SML (mais tous mes exercices ne trouvent pas leur solution dans l’article), je l’ai fait en OCaml, mais vous pouvez le faire dans le langage que votre choix. Tout me va, du moment que vous savez différencier les fonctionnalités "pures" du langage des autres (qu’il ne faut pas utiliser sauf quand c’est explicitement demandé), et que vous restez dans un cadre séquentiel. Pour les exercices qui parlent d’exceptions, il est sous-entendu qu’elles ont la sémantique des exceptions ML : si votre langage n’en a pas, faites comme si, un pseudocode suffit. Si vous ne les connaissez pas, j’en ai fait un résumé rapide en annexe.

Fonction `modulo`

La fonction modulo est un exemple qu’on sent un peu plus utile de fonction SR qui n’est pas représentable dans un langage fonctionnel pur. En deux mots, modulo surveille l’utilisation d’une des fonctions qui lui est passée en paramètre, c’est à dire les arguments qu’elle reçoit au court de ses appels, et les résultats qu’elle renvoie.

Plus précisément, modulo prend une fonction q : (int -> int) -> int (comme "questions") et une fonction r : int -> int (comme "réponses"). Imaginez que l’on donne la fonction r en paramètre à la fonction q, qui doit renvoyer un entier. Les deux fonctions (comme toutes les fonctions de l’article) sont supposées fonctionnelles, donc les moyens d’action de q pour fournir son résultat sont limités : il doit poser des questions à r et, selon les réponses, décider du résultat. Il peut poser une questions, plusieurs, aucunes (c’est alors une fonction constante), poser un nombre différent de questions selon les réponses qu’il a déjà reçues, etc. On définit modulo ainsi : il renvoie l’ensemble des questions posées par q, ainsi que les réponses que r a données.

Il est facile de coder modulo en utilisant des références :

let modulo q r =
  let li = ref [] in
  let traced_r x =
    let y = r x in
    li := (x, y) :: !li;
    y in
  ignore (q traced_r);
  !li

Il y a cependant un problème : cette fonction n’est pas SR ! En effet, elle produit des résultats différents pour fun r -> r 1 + r 3 et fun r -> r 3 + r 1, qui ont pourtant le même représentant dans [int -> int] : le résultat varie selon l’ordre dans lequel les questions ont été posées (d’abord 3, après 1, ou l’inverse). Pour la même raison, on ne s’intéresse pas au nombre d’appels de chaque argument, mais juste à la présence d’au moins un appel avec cet argument.

Il est cependant facile de résoudre ce problème : au lieu d’une liste de résultats on renvoie un ensemble de résultats, en utilisant un type dédié, ou en supprimant les doublons et triant la liste :

let modulo q r =
  let li = ref [] in
  let traced_r x =
    let y = r x in
    if not (List.mem_assoc x !li) then
      li := (x, y) :: !li;
    y in
  ignore (q traced_r);
  List.sort (fun (a, _) (b, _) -> a - b) !li

Cette fonction est maintenant SR. Pourquoi ? On pourrait imaginer que deux implémentations d’une même fonction partielle, qui ne posent pas les mêmes questions. En réalité, ça n’est pas possible : si la première fonction demande un entier n que la deuxième ne demande pas, il suffit de donner une fonction (SR) qui est définie partout sauf en n pour que les deux fonctions produisent des résultats différents (car la première diverge), donc elles ne correspondent pas à la même fonction mathématique.

(moins facile) Écrire modulo en utilisant des exceptions (et sans références).

On arrive maintenant au premier point tangent. Pour rendre notre fonction SR on a du lui retirer des informations, en fournissant du travail supplémentaire. L’auteur de l’article le remarque bien et utilise une formulation poétique : « one sometimes has to do stupid extra work in order to behave functionally ». Cette idée (fournir du travail supplémentaire pour garantir de bonnes propriétés) n’est pas du tout spécifique à ce papier, et je l’ai rencontré dans des situations variées. Par exemple, dans l’excellent CTM, Peter Van Roy différencie la programmation concurrente déterministe de la concurrence non-déterministe. Il doit parfois brider certaines de ses opérations pour rester dans le cadre déterministe : ça limite un peu (voire beaucoup dans certains cas) l’expressivité, mais apporte des avantages considérables en terme de raisonnement sur les programmes, recherche des erreurs, optimisations potentielles, etc.

(moins facile) D’après l’auteur, « indeed it is easy to see how use can be defined from modulo in pure functional ML ». Définir use à partir de modulo.

(difficile) En fait, l’expressivité de modulo est équivalente à celle de use : définir modulo à partir de use. Comme précédemment, il ne faut utiliser aucune autre fonctionnalité impure. Indice : l’implémentation (ou en tout cas la mienne) est nettement moins efficace que les précédentes.

L’auteur présente rapidement quelques fonctions SR qui ne sont pas définissables à partir de use ou modulo, mais sans expliciter leur définition^ε ni justifier cette non-définissabilité. Il évoque même une SR universelle, qui permettrait d’exprimer toutes les autres, bien que très peu efficace.

ε : si quelqu’un comprend la signification du deuxième paramètre de la fonction E de l’article, je suis preneur ; je croyais l’avoir trouvée en lisant le paper la première fois, mais je m’étais peut-être trompé, et en tout cas ne l’ai pas retrouvée au moment de la présente rédaction.

Cas d’utilisation

L’auteur présente ensuite deux applications pratiques des fonctions SR. Elles restent de l’ordre du jouet, parce qu’il explique ensuite qu’on peut toujours faire mieux, soit en abandonnant la contrainte de comportement fonctionnel, soit en enrichissant l’interface des fonctions considérées, mais ça reste assez amusant à voir.

Prédicat de recherche

On définit une fonction search :

int -> ((int -> int) -> bool) -> (int -> int) list`

search n pred doit fournir la liste des permutations de [1 .. n] (représentées comme des fonctions int -> int) qui vérifient le prédicat pred.

L’implémentation naïve parcourt l’espace de recherche, qui est de taille !n. Il est possible de couper de grandes parties de l’espace de recherche en utilisant la fonction modulo sur les permutations qui ne vérifient pas le prédicat : si le prédicat ne demande que les trois premières valeurs (en 1, 2 et 3) d’une permutation avant de renvoyer une réponse négative, il est inutile de tester toutes les permutations ayant les mêmes images en 1, 2 et 3 : la réponse sera forcément négative aussi. On a donc éliminé (n - 3)! candidats potentiels.

La définition de search est assez générale pour être appliquée à des problèmes de programmation par contrainte classique, comme le problèmes des huits reines, et l’optimisation utilisant modulo la rend, d’après l’auteur, raisonnablement efficace.

Il est bien sûr possible de faire le même genre de choses en restant dans le cadre des fonctions pures : il suffit de modifier l’interface de search pour que le prédicat renvoie de lui-même les informations sur les appels qu’il a effectué.^ζ Plus généralement, on peut visiblement imiter l’effet des fonctions SR impures dans un langage pur, en ajoutant des informations aux valeurs de retour des fonctions appelées. Ce n’est cependant pas toujours possible, par exemple si le prédicat est fourni par une bibliothèque externe sur laquelle le programmeur n’a pas de contrôle.

ζ : (int -> int) -> bool * (int * int) list

Plus généralement, et c’est le second point tangent, l’idée d’enrichir l’interface va en fait à l’encontre des principes habituels de génie logiciel : il faudrait modifier la fonction pour révéler une partie plus importante de son implémentation interne, dans le but d’un usage particulier, ce qui nuit d’une part à la modularité (il faut modifier l’interface d’une fonction fondamentale dans la perspective d’une utilisation spécifique qui peut être très loin dans la chaîne de dépendances), d’autre part à l’encapsulation (on demande à une fonction d’exposer plus d’information sur son implémentation interne). Cette pratique n’est tout simplement pas praticable à grande échelle : si l’on essayait d’exposer toutes les informations potentiellement utilisables par ce genre de pratiques rendues explicites, cela reviendrait essentiellement à rendre publique l’implémentation complète de la fonction.

C’est une question que j’ai trouvé intéressante parce que d’autres outils de la programmation fonctionnelle pure, comme les monades, peuvent soulèver des problèmes similaires. Les fonctions SR sont ici des outils précieux parce qu’elles permettent d’accéder à des informations sur une fonction sans alourdir son interface. Comme dit l’auteur, elles servent en quelque sorte à "rendre la boîte noire moins opaque".

Intégration d’une fonction

Le deuxième exemple est aussi assez joli. Supposez que l’on représente un nombre réel (entre 0 et 1 par exemple) comme un flux paresseux de nombres entiers (ses décimales) : type real = int * (unit -> real).

On cherche à écrire une fonction qui intègre une fonction real -> real entre 0 et 1, à une précision donnée (le nombre de décimales exactes du résultat, passé en paramètre). On commence par demander la valeur de la fonction en 0 à une précision suffisante (au moins autant de décimales que ce qui est demandé pour le résultat final), mais on utilise une variante de modulo pour connaître le nombre k de décimales demandées par la fonction avant de renvoyer un résultat. On sait que, si on se contente de cette précision, tous les nombres réels qui ont les mêmes k premières décimales (ici tous les nombres inférieurs à 10^-k) renverront le même résultat. On peut donc approximer l’intégrale de la fonction sur tout cette intervalle avec la précision désirée, et recommencer le processus en commençant à 10^-k au lieu de 0. L’algorithme termine en un nombre fini d’étapes (l’auteur en fait la preuve), et c’est une manière astucieuse de faire de très bonnes approximations.

Conclusion

Je donnerai la solution des exercices dans un prochain billet. En attendant, n’hésitez pas à poser vos questions, proposer vos solutions, ou simplement donner votre avis en commentaires ; ils sont là pour ça !

Les commentaires risquent donc de contenir des (fragments de) solutions. Prenez garde à ne pas vous gâcher le plaisir de chercher accidentellement.

Par ailleurs. je suis tout aussi intéressé par des commentaires généraux sur la réaction : avez-vous trouvé ça intéressant ? Trop détaillé ? Pas assez détaillé ? Qu’est-ce qu’il faut changer ? Je n’ai pas encore complètement décidé de la forme que ces réactions devraient avoir, et si vous avez des conseils/demandes, c’est avec plaisir.

Appendices

Il y a quelque chose de curieux dans la définition de la relation [ ] (qui est celle de l’auteur) : on ne prend en compte pour définir les éléments de ['a -> 'b] que leur action sur les éléments définissables (tels qu’on peut écrire un bout de code qui fait exactement ça) de type 'a. Ça me dérange un peu, sachant qu’on pourrait éventuellement passer à une fonction une valeur qui n’est pas définissable à l’intérieur du langage, mais qui fait appel à une bibliothèque logicielle codée dans un autre langage. Dans ce cas il faudrait considérer l’action sur toutes les fonctionnelles, et pas seulement les fonctionnelles définissables.

Exceptions en ML

Je décris ici les expressions en OCaml, mais l’important c’est la sémantique (ce que ça fait), pas la syntaxe (comment ça s’écrit). Le but c’est que vous sachiez un peu précisément ce que vous pouvez utiliser pour les exercices qui demandent d’utiliser des exceptions : un pseudo-code suffit, mais il faut comprendre ce que vous avez le droit de faire ou pas.

L’idée de base est qu’une expression, quand elle est lancée (raise) interromp complètement le calcul qui l’entoure, sauf si elle est rattrappée par un bloc try .. with. Par exemple :

let exists predicate array =
  try
    for i = 0 to Array.length array - 1 do
      if predicate array.(i)
      then raise Exit
    done;
    false
  with Exit -> true

Le bloc try <expr> with <cases> évalue l’expression <expr>, renvoie sa valeur si aucune exception n’est levée pendant l’évaluation, et sinon réagit selon les cases <cases> (c’est un filtrage de motif, mais c’est un détail) : si l’un des cas correspond à l’expression lancée, elle est arrêtée et la branche correspondante est suivie. Ici, on teste toutes les valeurs d’un tableau, en lançant une exception si l’une d’entre elle vérifie une condition, et on renvoie "faux" sinon. En dehors de la boucle, on rattrappe l’exception en renvoyant "vrai". Cela teste l’existence d’un élément vérifiant le prédicat, en arrêtant immédiatement le parcours du tableau dans ce cas (un peu comme les instructions de contrôle break ou return des langages impératifs).

On peut aussi utiliser des exceptions qui transmettent des valeurs. Pour cela il faut déclarer une nouvelle exception (Exit est prédéfinie) :

 exception Mon_exception of mon_type

mon_type est le type des valeurs transmises par l’exception. Par exemple :

exception Position_invalide of (int * int)

... raise Position_invalide (1, 2) ...

match .. with
  Position_invalide (x, y) ->
    printf "erreur : position invalide (%d, %d)" x y

Et les langages paresseux ?

Dans un langage paresseux, les fonctions ne prennent pas des valeurs, mais des termes quelconques que la fonction évaluera éventuellement elle-même si elle en a besoin. Toute la différence pour ce qui nous concerne repose sur le fait qu’on ne sait pas encore si les paramètres vont diverger ou pas (alors qu’en évaluation stricte, on est sûr qu’ils ne divergent pas). Au lieu de fonctions de ['a] dans ['b] + {⊥}, on doit donc modéliser avec des fonctions de ['a] + {⊥} dans ['b] + {⊥}.

Un terme paresseux t est donc un terme "par encore évalué". Il suffit de le représenter dans un langage strict par le terme fun () -> t, qui n’est pas encore évalué non plus.

Plus formellement : au lieu du type 'a, on considère que le paramètre est de type u -> 'a. En effet, [u -> 'a] = {*} -> 'a + {⊥} est isomorphe à 'a + {⊥}. Donc dans un langage strict [(u -> 'a) -> 'b] = ['a]+{⊥} -> ['b]+{⊥}.

On ne gagne donc aucune expressivité en passant à un langage paresseux. Cette étude les concerne tout autant que les langages stricts, modulo une traduction des types. Les fonctions u -> u étudiées sont juste des termes de type u dans un langage paresseux, (u -> u) -> u donne u -> u, et le dernier type est (u -> u) -> bool.

Dans un cadre paresseux, mid est la fonction qui force l’évaluation de son argument. En haskell on écrirait par exemple :

mid f = seq f ()

Impossibilité de `neg`

L’auteur ne donne pas plus de précisions, mais il n’est pas du tout clair que la fonction neg : 0 -> * | 1 -> ⊥ conduise au problème de l’arrêt. Dans cette section je donne une preuve faite de mes blanches mains, mais elle est un peu compliquée (je me plonge dans une classe de fonctions plus riche), donc si vous en avez une plus simple je suis intéressé.

Le problème de l’arrêt est la question suivante : « peut-on décider sans l’exécuter de si un programme va terminer ou boucler à l’infini ? ». Plus précisément, « existe-t-il un programme qui prend un programme P en paramètre, et renvoie vrai‘ si P bouclerait à linfini s’il était exécuté, et faux sinon ? ». On sait depuis le début du siècle précédent (donc avant l’apparition du premier ordinateur) que la réponse est « Non ».

La preuve de ce « Non » est assez simple (c’est en fait un remake d’une preuve très connue en mathématiques, l’argument diagonal) : imaginons qu’il existe un tel programme H (comme Halting problem). On définit le programme B (comme "Boum") suivant :

B(P) =
  si H(P(P)), boucler à l'infini
  sinon, terminer

B prend un programme, l’applique sur lui-même (le truc pas tordu déjà) et inverse sa divergence : si le programe diverge, B s’arrête, si le programme s’arrête B diverge. On peut maintenant poser la question qui tue : quel est le comportement de B(B) ?

si B(B) s’arrête, alors par définition B(B) diverge
si B(B) diverge, alors par définition B(B) s’arrête

Boum. On est arrivé à une contradiction, donc on est parti de quelque chose de faux. La seule supposition qu’on a faite pour en arriver là est l’existence de P, donc c’est ce qui est faux : P n’existe pas.

On peut réutiliser cette preuve pour déduire de nombreuses choses sur ce qu’on sait des programmes. Il suffit de "réduire" le problème au problème d’arrêt, en montrant en gros que « monsieur, si on savait répondre à votre question, on pourrait résoudre le problème d’arrêt, you fool ».

Cas présent

Dans le cas présent, on s’intéresse à la fonction neg qui s’arrête si on lui donne 0 (la fonction divergente), et diverge si on lui donne 1. On sent bien qu’il y a un lien avec le problème de l’arrêt, le fait d’inverser les divergences, mais ça ne va pas forcément plus loin : cette fonction ne permet pas de savoir directement si l’argument diverge puisque, une fois sur deux, elle ne répond rien du tout (⊥). Par exempe la fonction voisine 0 -> ⊥ | 1 -> * existe évidemment (c’est mid) et ça n’a rien à voir avec le théorème d’arrêt.

Concrètement, dans notre cadre la fonction d’arrêt est la fonction suivante :

halt 0 = true
halt 1 = false

Peut-on écrire halt à partir de neg ? Dans SR ça n’a pas l’air commode : si on donne 0 à neg, le calcul termine et on peut renvoyer true, mais si on donne 1 on est coincé dans une boucle infinie et on ne peut pas renvoyer false.

Je m’en tire en sortant de SR, en rajoutant une primitive de parallélisme : on ajoute la primitive par : (α -> β) -> (α -> β) -> (α -> β), qui exécute en parallèle les deux fonctions passées en paramètre : quand on lui donne une valeur, elle demande à la première fonction et à la deuxième simultanément, et elle renvoie le résultat de la première des deux à terminer ; si les deux divergent, elle diverge.

Cette primitive existe : il suffit de se placer dans un langage avec multi-threading et un ordonnancement équitable, et d’exécuter les deux fonctions dans des threads séparés, ou plus simplement encore de formaliser l’exécution d’un programme comme une machine procédant étape par étape, et d’alterner une étape d’exécution de chaque fonction à tour de rôle. Cela permet d’accéder à une autre classe d’expressivité des fonctions ; si l’on définit par convenablement, on peut rester dans un cadre déterministe (il suffit de s’assurer que si on lui donne deux fonctions qui terminent, elle ne choisira pas parfois l’une, parfois l’autre mais toujours la même), par contre on sort du cadre des "fonctionnelles", car deux implémentations dénotant une même fonction mathématique pourront donner des résultats différents (si l’une est beaucoup plus lente que l’autre, elle sera moins choisie par par).

(plutôt facile, si vous avez fait le reste) Écrire halt en utilisant par, neg et sans fonctionnalités impures.

Donc, dans le cadre bien réel des "fonctions SR auxquelles ont a ajouté du parallélisme", on ne peut pas écrire neg puisqu’elle permettrait d’écrire halt. Si on ne peut pas écrire neg après avoir ajouté par, on ne pourra sûrement pas l’écrire sans ajouter par (puisqu’on peut écrire moins de chose), donc [neg] n’appartient pas à [(u -> u) -> u].

bluestorm, Emily, et les chameaux

2009-08-07T15:14:24+02:00

Il était une fois un gars sans blog, mais qui voulait publier des choses. Un autre, qui avait un blog (quoique primitif, sans commentaires, sans JavaScript et sans Flash, OMG), vint, et lui proposa astucieusement d’héberger son contenu. Shazam !

Voici donc le premier billet de bluestorm, qui relate ses aventures dans le monde merveilleux des bêbêtes sous haute sécurité (et des concepts liés, bien évidemment), avec l’exemple d’Emily, une belle chamelle s’il en est (et rien à voir avec le modèle de mes dessins). —rz0

C’est ma première réaction. Wouhou ! Je suis débutant, merci d’être indulgent. Comment choisir le paper auquel réagir le premier ? J’ai commencé par rédiger une liste des papers que j’avais envie de traiter, en me promenant au hasard dans mon répertoire ~/Papers, et maintenant je prends arbitrairement le premier de la liste pour me forcer à commencer.

Le paper est How Emily Tamed the Caml (PDF, 16 pages). Il concerne la sécurité informatique, domaine que je connais très mal, et plus précisément une approche qui me fascine : le principe du moindre privilège (POLA, Principle Of Least Authorithy), et la capability-based security.

En deux mots (je vais développer un peu plus ensuite), la question que pose l’article est la suivante : comment faut-il modifier un langage de programmation généraliste pour lui faire respecter les principes du POLA ? On prend un langage de programmation généraliste (ici OCaml), et on le domestique (tame) en lui retirant toutes les fonctionnalités qui cassent le POLA ; un programme écrit dans le langage domestiqué donne donc des garanties de sûreté nettement plus fortes.

Je connais très mal le domaine de la sécurité informatique, donc il faut prendre tout ce que je dis avec prudence. Il y a certainement des imprécisions ou des erreurs dans ce que je vais dire. Si cela vous a intéressé, n’hésitez surtout pas à laisser un commentaire (constructif si possible), mail (note d’édition : bluestorm@, chez GMail, gmail.com, pour ceux qui ne sauraient vraiment pas) ou autres.

POLA, capability-based security

Si vous connaissez déjà tout ça, pas la peine de lire mon introduction, sautez directement aux deux derniers paragraphes de cette réaction, qui résument le contenu du papier.

Privilèges, POLA

On appelle privilège la possibilité de faire quelque chose sur l’ordinateur. Un utilisateur dispose par exemple du droit de renommer ses fichiers, ou d’en ajouter de nouveaux dans son répertoire personnel. Il n’a pas forcément tous les droits, par exemple s’il n’est pas administrateur de la machine il n’a pas forcément le droit d’installer des logiciels ou changer la configuration du système.

Dans la plupart des systèmes actuels, un programme est affilié à un utilisateur (la personne qui l’a lancé) et hérite exactement des droits de l’utilisateur : il a le droit de modifier les fichiers du répertoire personnel, mais pas de modifier la configuration du système. S’il avait plus de droits que l’utilisateur, ce serait une faille de sécurité : il pourrait par exemple modifier la configuration du système pour se lancer au démarrage et se répliquer sur le réseau (c’est comme ça que fonctionnent les virus).

Quand on y pense, il n’est pas forcément normal que chaque programme lancé par l’utilisateur ait accès à tous les privilèges de l’utilisateur. Par exemple si je lance un programme pour me donner l’heure qu’il est, il n’a pas besoin du droit de supprimer des fichiers dans mon répertoire, et s’il essaie de le faire c’est sans doute une erreur de programmation, ou carrément un programme malicieux fournit par un méchant programmeur qui essaie de me faire croire qu’il affiche l’heure pour effacer mes données personnelles. Dans les systèmes d’exploitations modernes, il est donc possible de restreindre les droits de certains programmes.

Le POLA est un principe qui résume cette approche : chacun doit avoir à sa disposition exactement l’ensemble de privilèges dont il a absolument besoin pour faire son travail, et rien de plus.

Lien

Article POLA sur Wikipédia (en)

Granularité

C’est un principe enfantin qui n’est pas appliqué complètement par les systèmes d’exploitations actuels. En particulier les systèmes dérivés de UNIX utilisent des dérivés de l’approche ugo, où l’on attribue les droits selon un découpage utilisateur/groupe (certains utilisateurs ou groupes d’utilisateurs ont des droits spécifiques sur certains fichiers/programmes/outils), qui est une distinction beaucoup moins fine. Il y a eu des améliorations depuis les premiers temps d’UNIX, mais à ma connaissance aucun système grand public ne respecte vraiment les principes du POLA à un niveau suffisamment fin.

Parce que l’on peut appliquer le POLA à un grand nombre de niveau. Au niveau des utilisateurs, c’est grosso-modo ce que font les administrateurs systèmes consciencieux aujourd’hui. Au niveau des programmes, c’est déjà nettement plus délicat. On pourrait même appliquer le POLA à l’intérieur des programmes en assignant des droits différents aux différents modules et composants logiciels du programme (la couche GUI aurait des droits d’affichage, et pas le reste, par exemple). C’est ce que permettent les langages capability-based.

Il y a donc une idée de granularité : dans l’absolu tout le monde est d’accord sur le fait que le POLA est la meilleure approche de la sécurité, mais jusqu’à quel niveau de détail on peut l’appliquer ?

Capabilities

Les capabilities^α sont une autre idée qui est fortement reliée au POLA. Elles ne sont pas nécessaires pour construire un système qui respecte le POLA, mais leur élégance fait que les gens qui travaillent dans ce domaine les utilisent très souvent.

Dans les systèmes d’exploitation et les langages actuels, on fait une distinction très nette entre une action, et l’autorisation de faire cette action. Par exemple, n’importe quel programme peut exécuter la fonction qui lit le contenu d’un fichier, il suffit de donner l’adresse du fichier sur le disque. Cependant, cette fonction va parfois échouer si le programme n’a pas les droits nécessaires pour lire ce fichier, et renvoyer une erreur. Le « moyen d’accès » au fichier est son adresse, et il y a une phase de sécurité séparée.

L’idée des capabilities est que le moyen d’accès et le droit d’accès peuvent être réunis en une seule et même entité. Une capability est un objet^β qui contient à la fois la méthode pour faire une action et les droits pour l’effectuer. Si le système donne à un programme la capability « lire le fichier machin », le programme peut l’utiliser pour lire le fichier, ou bien la donner à un autre programme qui aura à son tour le pouvoir de lire le fichier. S’il n’a pas reçu cette capability, le programme n’a pas le droit de le lire, mais il n’a même pas le moyen concret d’essayer de le lire.

α : Je n’ai pas trouvé de traduction en français qui me plaise, je ne sais pas si "capacité" convient.

β : Je parle ici d’objet au sens large et ça n’a aucun rapport avec la Programmation Orientée Objet.

Lien

Article 'Capability-based security' sur Wikipédia (en)

Rôle des langages de programmation

Support par le système

On a déjà écrit des systèmes d’exploitation miniatures basés sur le concept de capabilities ; par exemple dans le projet EROS/CaprOS. C’est un noyau de système d’exploitation.

Le problème c’est que l’approche par capabilities est radicalement différente des méthodes des systèmes actuels, et il est très difficile d’assurer la compatibilité entre un système d’exploitation capability-based et un logiciel développé pour un système grand public : lui s’attend à ce qu’on lui donne des droits sur tout et n’importe quoi, et si on le fait on perd les bénéfices en matière de sécurité ; il faudrait donc ré-écrire en profondeur le logiciel pour qu’il respecte le POLA. Concrètement, ces projets de recherche ne sont donc utilisés par essentiellement personne parce qu’ils ne sont compatible avec aucun des logiciels existants, et l’effort pour les rendre utilisables serait énorme, bien supérieur au budget des équipes de recherche concernées.

Support par le langage de programmation

Il est cependant possible de mettre en place le POLA localement, au sein d’un programme. Il suffit essentiellement de restreindre l’interface entre le programme et le système d’exploitation (qui est laxiste et donne trop de droits) à une petite couche "administratrice" (qui détient tous les droits du programme), qui se charge de répartir ces droits aux autres composants du programme sans leur en donner trop.

Cela limite un peu le cadre de la chose puisque c’est le programmeur qui s’occupe de sécuriser son propre programme. On ne peut pas faire confiance par exemple à un méchant pour écrire ses programmes de cette manière, il ne va pas se tirer une balle dans le pied ! Cela peut toujours être utile dans le cas où on propose au méchant de coder quelque chose pour notre propre programme : si son code est inclus dans une partie sécurisée, et que la sécurité est vérifiée par le compilateur, il ne peut pas faire de bêtises. C’est aussi utile pour les erreurs qui ne sont pas volontaires mais accidentelles : si on a un bug dans une partie du programme, ça peut mal se passer, mais il ne fera rien qui lui est interdit. S’il y a par exemple une vulnérabilité dans une partie du code qui permet à des attaquants de faire des actions non prévues, ils seront limités par le peu de droits dont dispose cette partie du code, donc c’est très intéressant.

Pour avoir un tel support au sein du programme, il faut des langages de programmation pensés pour. Le langage le plus connu dans ce domaine est E.

Il faut d’une part que le compilateur du langage puisse vérifier que la sécurité est bien respectée (qu’une partie du code qui n’est pas censée lire le contenu de fichiers ne puissse pas quand même demander au système d’exploitation de le faire), et d’autre part que les fonctionnalités du langage ne permettent pas d’écrire du code qui casse cette protection. Par exemple, si une partie du programme peut écrire en mémoire la clé d’accès au contenu du fichier, une partie qui n’est pas censée lire de fichier mais peu lire dans la mémoire peut utiliser cette clé et outrepasser ses droits, sans que le compilateur puisse s’en rendre compte et signaler l’excès de privilège.

Lien

Article E sur Wikipédia (en)

Cas d’Emily

Ce que présente le papier cité c’est la transformation d’un langage généraliste, qui n’a pas été pensé à la base pour respecter le POLA, en un langage sécurisé. Il s’agit essentiellement de retirer toutes les fonctions « dangereuses » de la bibliothèque standard, en les remplaçant par des équivalents « sécurisés » qui rendent explicite les capabilities nécessaires. Par exemple la fonction open_out de Caml, qui permet d’ouvrir un canal en écriture vers n’importe quel fichier, est retirée et n’est plus accessible à l’ensemble du programme. Seule la petite couche d’interface avec le système peut créer des canaux à volonté, et les autres parties du programme doivent lui demander pour recevoir un canal, ou plutôt la capability correspondante, qui encapsule dans un record le canal et les fonctions d’entrée/sortie qui y sont liées.

Le papier décrit donc d’une part les modifications apportées à la bibliothèque standard OCaml, d’autre part la découpe entre la partie « toute puissante » du programme qui a tous les droits donnés par le système, et les parties sécurisées : la partie « toute puissante » doit être la plus petite et la plus simple possible pour ne pas comporter d’erreurs/failles. Il présente des exemples de programmes sécurisés, programmes en ligne de commande ou programmes avec GUI. Il discute aussi les impacts de cette transformation sur le style de programmation, ou les performances des programmes écrits de cette manière.

Pour résumer, je trouve que cet article est une bonne introduction aux problématiques de sécurité d’un langage de programmation. Il est très accessible, n’approfondit pas énormément et ennuirait sans doute un connaisseur du sujet, mais pour un inculte comme moi ça a constitué une lecture agréable.

Lien

L'article (PDF, 16 pages)

Ours & Hippy — le blog

Pourquoi le C est moins puissant que votre langage favori

Le problème

La solution ?

Que retenir de tout ça ?

Cohérence des effets de bord

Problématique

Coherent Reaction

Remarques personnelles

Pourquoi attacher tant d'importance au typage ?

Rappels

Types comme information

Le langage qui parle de lui-même

Système de typage et vérification

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

Contraintes et limitations

Pour bien typer, il faut bien comprendre

Puissance du typage et complexité du langage

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

Mélanger typage statique et typage dynamique ?

Les types ne font pas tout

En bref

L'innocence est un mythe : les programmes fonctionnels nécessairement impurs

Des fonctions fonctionnelles non pures

Exemple : fonction use

Cas (u -> u) -> u

Cas ((u -> u) -> u) -> bool

Fonction modulo

Cas d’utilisation

Prédicat de recherche

Intégration d’une fonction

Conclusion

Appendices

Exceptions en ML

Et les langages paresseux ?

Impossibilité de neg

Cas présent

bluestorm, Emily, et les chameaux

POLA, capability-based security

Privilèges, POLA

Granularité

Capabilities

Rôle des langages de programmation

Support par le système

Support par le langage de programmation

Cas d’Emily

Exemple : fonction `use`

Cas `(u -> u) -> u`

Cas `((u -> u) -> u) -> bool`

Fonction `modulo`

Impossibilité de `neg`