From madore@news.ens.fr Path: eleves!not-for-mail From: madore@news.ens.fr (GroTeXdieck) Newsgroups: ens.forum.informatique.lang Subject: Reflexions sur Tunes Date: 18 Jul 1999 18:33:22 GMT Lines: 1519 Sender: madore@clipper.ens.fr Message-ID: <7mt6li$a81$1@clipper.ens.fr> NNTP-Posting-Host: clipper.ens.fr Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-Trace: clipper.ens.fr 932322802 10497 129.199.129.1 (18 Jul 1999 18:33:22 GMT) X-Complaints-To: forum@clipper.ens.fr NNTP-Posting-Date: 18 Jul 1999 18:33:22 GMT X-Newsreader: Flrn (0.4.0 - 07/99) X-Rumor: They say that when your god is angry you should try another one. X-Number-Of-The-Day: 66 Xref: eleves ens.forum.informatique.lang:159 Salut. Bon, puisque Faré refuse d'écrire Tunes, il va falloir qu'on le fasse à sa place (mais c'est vrai que Faré est un méta-programmeur donc c'est normal). Je rassemble donc ici quelques réflexions sur les langages de programmation et sur ce que devrait être un langage de programmation Ultime. Je les envoie à Faré en tant qu'Architecte Suprême de Tunes, à ¦# qui, malgré ses perversions juvéniles (le C++), a tout de même une idée de ce qu'est un beau langage, à dmonniaux pour le faire stresser, à Antoine pour l'embêter, et à Péter qui s'amusera certainement aussi. Et peut-être que je les posterai dans ens.forum.informatique.lang (pour faire râler Max un peu). Ces réflexions sont en vrac, parfois pas tout à fait achevées, obscures, voire fausses. Il faut m'excuser : avec toutes les idées qui bouillonnaient dans ma tête, si je ne me pressais pas, j'allais en oublier plein. ********************************************************************** PARTIE I : BUTS ET PRINCIPES L'un des ingrédients essentiels de la réussite c'est la simplicité du langage. Plus le langage est simple, plus il est facile à comprendre et manipuler, donc plus il est facile de raisonner dessus et de métaprogrammer. Appelons-ça l'objectif (1). Cela exclut des grosses bouzes comme le C++. Je parle là de la simplicité de l'ossature du langage et non de sa bibliothèque : celle-ci a intérêt à être plutôt riche, sinon on se retrouve dans la même situation que Scheme où un programme ne peut même pas quitter proprement parce que personne n'a cru bon de normaliser le (quit) ou le (exit) en Scheme. Autre principe général (principe (2)) : il ne faut jamais appauvrir le langage, ou rajouter du « bondage and discipline » sous prétexte de rendre le travail du compilateur plus facile. L'*interpréteur* doit être raisonablement simple. À partir de là, on a un compilateur trivialement, qui consiste à prendre le programme et à lui rajouter le code de l'interpréteur ; passer de ça à un véritable compilateur est essentiellement un travail d'optimisation statique. Décider ce qui peut se faire en statique (compile-time) plutôt qu'en run-time est un travail certes difficile, et on ne s'attend pas à ce que le compilateur soit omniscient. Il faut qu'il soit possible de lui mâcher le travail en lui donnant des indications (principe (3)), mais il ne faut pas (c'est le principe (2)) qu'on soit *tenu* de respecter des principes idiots pour l'honneur [comment on dit « for the sake » en français ?] de la facilitation des optimisations statiques. Ces principes-là sont relativement homogènes. Là où on a plus de difficulté, c'est dans ce que j'appelle le « conflit du clair-obscur », que je vais expliquer. On veut (4) que le langage soit réflexif. Entre autres, il doit avoir une forme eval. Ce serait contraire au principe (2) que d'exclure la forme eval en ce qu'elle exige d'intégrer au programme tout l'évaluateur, voire le compilateur, du langage. Bien entendu, l'optimisation d'une expression comme (eval 'a) en a est à ranger, au même titre que l'optimisation de (+ 2 2) en 4, au rang des optimisations statiques effectuées par le compilateur, et qui ne sont pas toujours possibles (comme (+ x 8) ne peut pas se simplifier). À tâche pour le programmeur de savoir maîtriser ses outils et leur coût. Non seulement le langage doit avoir une fonction eval, mais celle-ci ne doit rien avoir de « magique ». Autrement dit, l'implémentation d'eval, et donc de l'évaluateur lui-même, doit être visible et reproductible dans le langage. J'appelle ça le principe (5) du « less magic, more metacircularity ». En clair, si dans le corps de l'interpréteur on a quelque chose comme (define (eval expr env) (cond ((symbol? expr) (lookup-variable expr env)) ...)) alors il faut que lookup-variable et pas seulement eval soient des points d'entrée possible pour le langage même. Avec tout ce que cela impose, notamment la citoyenneté de première classe des expressions, environnements et fermetures. (À propos des environnements et d'eval, voir le chapitre 8, « Évaluation et réflexivité », du bouquin de Christian Queinnec, « Les Langages Lisp », pour une discussion embrouillée et mal écrite comme d'habitude dans ce livre mais néanmoins intéressante et complète.) Le principe (6) est celui de la citoyenneté de première classe de tous les objets, concepts, types, etc., manipulés par le langage. Cela résulte du principe (5) (le langage lui-même et ses éléments doivent être des citoyens de première classe), et du principe (1) (c'est un facteur de simplicité d'avoir un traitement homogène de toutes les données) assorti au principe (2) (la complexité éventuellement introduite pour la compilation ne doit pas nous faire reculer - d'ailleurs, elle n'est pas si certaine). Revenons donc au dilemme du clair-obscur. D'un côté, la possibilité de manipuler les objets avec des méthodes homogènes et unifiées (c'est le principe (6)) est demandeuse de clarté. C'est-à-dire que, principe (7), toutes les données enfermées dans un objet doivent pouvoir en être extraites, puisqu'on dispose d'énormément de méthodes pour le regarder sous toutes ses coutures. De l'autre côté, le souci d'abstraction (principe (8)) est un principe d'obscurité, consistant à cacher les entrailles des données, pour abstraire le programmeur des détails de l'implémentation. Prenons un exemple, le type fonction. Le principe (7) de clarté voudrait que le corps de la fonction, sa liste de paramètres formels, et ainsi de suite, fussent accessible de l'extérieur. Cela permet, entre autres, de véritablement métaprogrammer (d'utiliser une fonction autrement qu'en l'appliquant). Le principe (8) d'obscurité demande que ces détails soient cachés. Il y a là deux aspects : l'un conceptuel (« data abstraction ») qui veut qu'on ne retienne d'une fonction que ce qu'elle fait et non comment elle le fait. L'autre pratique, à savoir qu'il est pour le moins désagréable qu'un compilateur soit systématiquement obligé de garder de toute fonction deux formes, l'une symbolique et l'autre compilée. Par ailleurs, dans un système de sécurité basé sur des tokens (dont il sera question plus loin), le principe d'obscurité peut être, au-delà d'une satisfaction esthétique ou d'une question d'efficacité, un des fondements mêmes de la sécurité du système. Il y a deux aspects à l'obscurité : obscurité en écriture et obscurité en lecture. Par exemple, pour le type symbole, l'obscurité en écriture serait la demande qu'il n'existe pas de coercion string->symbol : cela permet ainsi au système de manipuler les symboles sous une forme entièrement différente de la forme littérale, celle-ci étant purement syntactique et transformée en autre chose (p.e. une hash value) au moment de la compilation (même avant : du lexage). L'obscurité en lecture serait la demande qu'il n'existe pas de coercion symbol->string. Cela permet par exemple au système de ne retenir qu'une partie du nom du symbole (si la norme le permet) - à vrai dire, cet exemple est assez mauvais et en vérité dans le cas du type symbole je ne vois pas trop l'intérêt de maintenir l'obscurité en lecture si on n'exige pas l'obscurité en écriture. Dans le cas du type fonction, on voit peut-être mieux les choses. De manière générale, je suis plutôt favorable à une clarté en écriture et une obscurité en lecture. Autrement dit, que les différents objets et types soient fabricables par une large bande de constructeurs, mais qu'une fois l'information enfermée dedans elle ne soit accessible que par des méthodes bien précisées. Attention toutefois : dès lors qu'un type possède un prédicat d'égalité strict, la clarté en écriture donne naissance à suffisamment de pouvoir d'observation pour qu'il soit vain de chercher à maintenir l'obscurité en lecture (c'est l'exemple du type symbole). On peut aussi imaginer que la clarté ou l'obscurité en lecture soit précisée pour l'objet au moment où il est créé. D'ailleurs, on peut systématiser ça : il suffit de créer un type qui se projette naturellement sur le type obscur (opaque), mais qui possède des informations supplémentaires pour garantir la clarté en lecture, et de créer selon le cas les objets dans ce type clair ou directement dans le type opaque. Et on peut rendre la création de tels types systématique. Mais ce n'est qu'une idée au passage. ********************************************************************** PARTIE II : SYNTAXE ABSTRAITE, FORMES SPÉCIALES Revenons à nos moutons. Il y a une chose que je désire (9) limiter au maximum dans le langage, et même éviter complètement, ce sont les « formes spéciales ». En Scheme, par exemple, lambda est une forme spéciale et non une fonction, puisqu'elle n'évalue pas ses arguments ; ou, comme le fait remarquer Péter, elle les évalue de manière totalement différente de la manière habituelle ; si on veut respecter le principe (4) de réflexivité, il faut rendre cette forme accessible au langage comme point d'entrée ordinaire. En Scheme, si f est une fonction, on peut remplacer f par (if #t f) ; cela fait partie de la citoyenneté de première classe. Par exemple, on peut réécrire l'expression ((lambda () (* 6 7))) en ((lambda () ((if #t *) (if #t 6) (if #t 7)))) en revanche, on ne peut pas écrire (((if #t lambda) () (* 6 7))) car la forme lambda non seulement n'évalue pas ses arguments comme d'habitude mais en plus se reconnaît syntaxiquement. Il faut noter que ces deux points sont différents et bien séparés si on accepte d'imposer l'ordre d'évaluation (en Unlambda par exemple, d est une forme spéciale, mais qui peut être produite par une évaluation, par exemple ``idr s'évalue de même que `dr). Il y a moyen de contourner ça si on décide de jouer à fond avec la réflexivité. Par exemple, je peux définir, en Scheme, (define (functional-lambda formals . body) (eval `(lambda ,formals . ,body))) et alors écrire (functional-lambda '(foo bar) 'foo) à la place de (lambda (foo bar) foo). Institutionnalisons ça et on a viré une forme spéciale, et on peut toutes les virer comme ça. Le fait de comprendre (functional-lambda '(foo bar) 'foo) comme (lambda (foo bar) foo) est de même calibre que celui de comprendre (+ 2 2) comme 4, c'est une optimisation au compile-time. Et, direz-vous, que fait-on des quotations ? Ne sont-ce pas des formes spéciales ? À quoi sert-il d'écrire (functional-lambda '(foo bar) 'foo) si c'est pour que '(foo bar), soit (quote (foo bar)) soit une nouvelle forme spéciale ? Aha ! Mais c'est que (quote (foo bar)) peut encore s'écrire (list 'foo 'bar). Et 'foo peut encore s'écrire (string->symbol "foo"). Plus de forme spéciale. Encore que "foo" en soit une d'une certaine manière... Mais elle peut s'écrire (list->string (list #\f #\o #\o)), et #\f peut encore s'écrire (integer->char 102). Et d'ailleurs 102 est encore une forme spéciale, mais ça ne fait rien elle peut s'écrire (* 2 3 17), et 2 s'écrire (+ 1 1), et il suffit qu'il y ait une variable one qui soit bindée à 1 pour que j'aie démontré qu'on pouvait tout faire à partir de variables et d'applications, exploit sans intérêt. Qu'est-ce que j'essaye de dire ? Qu'il faut décider quels types peuvent apparaître dans le résultat du parsing d'un programme. Je m'explique. En Scheme, un programme (méta-expression) se représente comme une liste (symbolic expression). Ça a du bon, mais ça a aussi ses dangers. En ML, il n'y a pas de réflexion, pas de représentation des programmes dans les programmes. Prenons une position intermédiaire et imaginons une représentation des programmes (i.e. de leur syntaxe abstraite) par un type abstrait en simili-ML. L'idée c'est que le parsing produit un objet avec un type program avec : type value = INT of int | STRING of string | ... and program = VAL of value | APPLY of program * program | ... ;; et dans le eval on a quelque chose comme let rec eval = function VAL v -> fun env -> v | APPLY (rator,rand) -> fun env -> apply (eval rator env) (eval rand env) | ... and apply = ... ;; Il faut bien noter qu'eval et apply sont les fonctions du langage sous-jacent, et qu'elles seront directement accessible par l'intermédiaire de fonctions primitives. À ce moment-là, le type program fait partie des types (« de première classe ») manipulables dans le langage et je dois ajouter type value = INT of int | STRING of string | PROGRAM of program | ... ... et les types value et program sont mutuellement récursifs. Si je veux un entier, je peux écrire quelque chose comme 42, et le lexer va convertir en VAL (INT 42) dans son résultat (de type program). En fait, je pourrais avoir uniquement du APPLY, comme noté précédemment, et la possibilité de mettre directement des valeurs (VAL) self-evaluating est une commodité dans un programme. Les entiers d'un programme peuvent donc être directement à l'intérieur d'un programme sous forme de VAL, ou bien provenir de l'évaluation d'un programme. D'où proviennent les données de type PROGRAM ? Il faut naturellement qu'il y ait des fonctions permettant de les manipuler, et de les créer (pas d'obscurité en écriture) ; il peut également être commode de disposer d'un moyen d'introduire des VAL PROGRAM directement dans le programme au niveau du lexing. Ça s'appelle la quotation, et de même que pour la quotation (le VAL) des entiers, c'est une commodité, mais une commodité bien pratique. Il faut bien entendu une syntaxe pour cela, et en lisp on a choisi le ' (le quote). Comme le lisp représente tout sous forme de listes, ce qui est certes élégant mais ce qui impose quelques contorsions tout de même ; et que le ML ne représente pas les programmes, les gens ont fini par avoir les idées assez embrouillées. Quant aux fonctions, d'où sortent-elles ? Il y a essentiellement trois solutions : soit (a) un VAL FUNCTION (où FUNCTION est, bien entendu, un constructeur du type value) soit (b) un LAMBDA, soit (c) par application et lookup ordinaires. Prenons cela à l'envers. Par (c) application et lookup ordinaires, cela veut dire que eval renverra occasionnellement un type value construit par FUNCTION en réponse à soit un lookup de variable qui est une fonction (donc prédéfinie parce que tel quel le programme ne peut pas construire de fonctions) ou bien en valeur de retour d'une fonction justement. ===longue digression=== Voici par exemple un évaluateur d'un langage assez simplissime (sans environnements pour le moment, on aura assez d'emmerdes avec ça plus tard). type symbol = string and value = INT of int | STRING of string | SYMBOL of symbol | PROGRAM of program | FUNCTION of (value -> value) and program = VAL of value | APPLY of program * program | VAR of symbol ;; exception Unbound_variable of symbol;; exception Wrong_type_to_apply;; exception Miscellaneous_error;; let rec eval = function VAL v -> v | APPLY (rator,rand) -> apply (eval rator) (eval rand) | VAR s -> lookup s and lookup = function "k" -> FUNCTION (fun x -> FUNCTION (fun y -> x)) | "s" -> FUNCTION (fun x -> FUNCTION (fun y -> FUNCTION (fun z -> eval (APPLY(APPLY(VAL x,VAL z), APPLY(VAL y,VAL z)))))) | s -> raise (Unbound_variable s) and apply = function FUNCTION f -> fun rand -> f rand | _ -> raise Wrong_type_to_apply ;; À part que je n'ai jamais su indenter un programme en ML, ça devrait être assez clair. Et notamment le fait que, attendu que le parseur ne produit que des APPLY, des VAL INT, des VAL STRING, et des VAR, mais pas de VAL FUNCTION, la seule façon de créer une fonction est d'utiliser les lookups et les applications des fonctions primitives "k" et "s". Si on a un mécanisme de quotation permettant de créer du VAL SYMBOL et du VAL PROGRAM, alors pour peu qu'on oublie momentanément une petite difficulté avec les environnements, on peut concevoir une fonction "functional-lambda" ou "make-function". À ce moment-là, il faut des environnements. Voilà une tentative dans un langage à scoping (portée) dynamique ou statique au choix : type symbol = string and binding = symbol * value and environment = binding list and value = UNIT | INT of int | STRING of string | SYMBOL of symbol | PROGRAM of program | FUNCTION of (value -> environment -> value) and program = VAL of value | APPLY of program * program | VAR of symbol | PROGN of program * program ;; exception Unbound_variable of symbol;; exception Wrong_type_to_apply;; exception Wrong_argument_type;; exception Miscellaneous_error;; let rec eval = function VAL v -> fun env -> v | APPLY (rator,rand) -> fun env -> apply (eval rator env) (eval rand env) env (* dynamic scoping here *) | VAR s -> fun env -> lookup s env | PROGN (primus,pares) -> fun env -> eval primus env; eval pares env and lookup = fun s -> function [] -> raise (Unbound_variable s) | (b,v)::l -> if s=b then v else lookup s l and apply = function FUNCTION f -> fun rand -> fun env -> f rand env | _ -> raise Wrong_type_to_apply ;; let initial_environment = [("make-fun/ls", (* lexically scoped *) FUNCTION (function SYMBOL s -> fun def_env -> FUNCTION (function PROGRAM body -> fun bod_env -> FUNCTION (fun rand -> fun app_env -> eval body ((s,rand)::def_env)) | _ -> raise Wrong_argument_type) | _ -> raise Wrong_argument_type)) ; ("make-fun/ds", (* dynamically scoped *) FUNCTION (function SYMBOL s -> fun def_env -> FUNCTION (function PROGRAM body -> fun bod_env -> FUNCTION (fun rand -> fun app_env -> eval body ((s,rand)::app_env)) | _ -> raise Wrong_argument_type) | _ -> raise Wrong_argument_type))] ;; Je me suis amusé à lui trouver une syntaxe concrète, et à implémenter le tout, avec lexeur et parseur. Voici d'ailleurs la description du parseur : %token UNITVAL %token INTVAL %token STRVAL %token TOK %token LPAREN RPAREN %token SLASH %token QUOTE %token SEMICOLON %token EOF %start main %type main %% main: expr EOF { $1 } expr: simple_expr { $1 } | expr simple_expr { APPLY($1,$2) } | expr SEMICOLON expr { PROGN($1,$3) } simple_expr: LPAREN RPAREN { VAL(UNIT) } | INTVAL { VAL(INT $1) } | STRVAL { VAL(STRING $1) } | TOK { VAR($1) } | SLASH TOK { VAL(SYMBOL $2) } | QUOTE simple_expr { VAL(PROGRAM $2) } | LPAREN expr RPAREN { $2 } ; Ce qui est important, ce n'est pas la description elle-même, mais ce que la syntaxe est capable de générer. En l'occurrence, des APPLY, des PROGN, des VAR et certaines VAL : UNIT, INT, STRING, SYMBOL et PROGRAM, mais pas FUNCTION. (Notons que le langage distingue un VAL SYMBOL d'un VAL PROGRAM VAR, alors que le Scheme ne le distingue pas : ici, ils sont notés /x et 'x respectivement, alors qu'en Scheme tous deux sont 'x ; comparer au /x et {x} du PostScript.) Finalement, qu'est-ce qu'une forme spéciale ? C'est un des constructeurs du type program - au sens large, c'est-à-dire que VAL UNIT ou VAL INT sont considérés comme des formes spéciales - disons plutôt une forme qui peut être produit par le parseur. En Scheme les choses sont quelque peu obscures puisque comme on tient à identifier les types program et list, et que ce dernier n'a que deux constructeurs (cons et nil), on est obligé de faire des choses pas jolies-jolies, et on a des formes spéciales comme (begin ...) qui ressemblent furieusement à des applications. Ça, je n'aime pas trop. Une chose importante : dans le langage ci-dessus, on peut produire des données de type PROGRAM, en utilisant la forme spéciale QUOTE qui produit du VAL PROGRAM. Cependant, si on veut que PROGRAM soit vraiment un type possédant une clarté en écriture, il faut qu'il existe des fonctions élémentaires qui puissent produire des résultats de type PROGRAM. Par exemple : make-val prenant un objet x quelconque et renvoyant le programme VAL x (ce qui permet d'ailleurs de construire des VAL FUNCTION) qui s'évalue en x ; make-apply prenant deux programmes rator et rand et renvoyant le programme APPLY(rator,rand) ; make-var prenant SYMBOL(s) et renvoyant VAR(s) ; et make-progn qui fait ce qu'on devine. Il faut aussi des environnements de première classe, des fonctions eval, lookup et apply qui donnent accès aux trois points d'entrée de l'évaluateur (naturellement, on peut se contenter d'un seul et implémenter les autres avec, par exemple lookup = (make-fun/ls /var '(make-fun/ls /env '(eval (make-var var) env))) puisque chercher var dans un environnement revient à évaluer le programme 'var ; mais autant toutes les avoir). Par ailleurs, je note que le type symbol, telles que les choses sont, n'est pas obligé d'être une chaîne : une clé de hachage peut convenir. Cela reste vrai tant qu'on garantit l'obscurité à la fois en écriture et en lecture de SYMBOL. ===fin longue digression=== Revenons à nos fonctions. Tout ceci était une longue discussion sur ce qu'on peut faire dans le cas (c) de l'alternative mentionnée plus haut, c'est-à-dire le cas où les fonctions peuvent être produites, dans un sens très fort, par d'autres fonctions, et donc qu'on se passe de la forme spéciale LAMBDA. Le Scheme, le ML et autres, préfèrent le choix (b). C'est-à-dire ajouter une nouvelle forme spéciale au langage : and program = VAL of value | APPLY of program * program | LAMBDA of symbol * program | ... ;; Et un branchement dans l'eval : let rec eval = function VAL v -> fun env -> v | APPLY (rator,rand) -> fun env -> apply (eval rator env) (eval rand env) | LAMBDA (s,body) -> fun env -> make_function s body env | ... et make_function peut être à peu près quelque chose comme fun s body env -> FUNCTION (function v -> eval body ((s,v)::env)) (ici on est de nouveau dans un langage à portée purement lexicale). Cette approche de l'abstraction par une forme spéciale lambda simplifie nettement le travail des compilateurs puisque l'examen du corps du lambda peut se faire au moment de la compilation, il est toujours disponible statiquement (alors que dans le langage que j'avais présenté dans la digression, si on écrit (make-fun/ls /x b), il se peut bien que le b ne soit pas déterminable statiquement au moment de la compilation (par exemple, il peut provenir d'une entrée de l'utilisateur). En vertu du principe (2), cet argument doit être rejeté. De toute manière, en présence de eval (sous-entendu, eval comme *fonction*), j'ai déjà noté que la forme spéciale lambda ou la fonction make-fun/ls sont essentiellement équivalentes. Cependant, il n'est pas pour autant *défendu* de garder LAMBDA dans le langage, tant qu'on fournit *également* une autre approche par de pures applications (de même qu'on pourrait se passer des VAL INT mais qu'il est tout de même agréable de les avoir). Que dire de l'approche (a) ? Elle n'est possible (je pense) que dans un langage à portée dynamique, car dans de tels langages les fonctions n'ont pas besoin d'être associées à un environnement (elles n'ont pas de fermeture), et elles peuvent donc être entièrement décrites au moment de la compilation (du parsing même). On verra plus bas un exemple ou FUNCTION et PROGRAM coïncident et où on se trouve dans ce cas. En résumé de cette partie : les « formes spéciales » d'un langage sont les différentes constructions susceptibles d'être produites par le parseur (les constructeurs de sa syntaxe abstraite), et qui correspondent essentiellement à des cas dans le switch principal de l'eval. On peut toujours se passer de toutes les formes spéciales hors du APPLY (application fonctionnelle) et du VAR (lookup de variable), mais ce n'est pas nécessairement une bonne idée pour autant... En revanche, il est de mauvais goût (selon le principe (2)) qu'une forme de valeurs ne soit accessible que par une forme spéciale, c'est-à-dire que tous les cas du switch doivent, si on veut un langage agréablement réflexif (mais en contrepartie difficile à compiler), être accessibles depuis des fonctions. ********************************************************************** PARTIE III : ENVIRONNEMENTS ET PORTÉE La portée « lexicale » se réfère au cas où la valeur d'une variable référencée dans le corps d'une fonction est recherchée dans l'environnement en vigueur au moment où la fonction a été définie, tandis que la portée « dynamique » se réfère au cas où cette valeur est recherchée dans l'environnement en vigueur au moment où la fonction est appelée. L'exemple canonique pour faire la distinction est le suivant : ((lambda (a) (((lambda (a) (lambda (b) a)) 42) 18)) 1729) la fonction (lambda (b) a) est définie dans un environnement où a vaut 42, et elle est appliquée (à 18, mais peu importe) dans un environnement où a vaut 1729. Un langage à portée lexicale affectera donc à cette expression la valeur 42, tandis qu'un langage à portée dynamique l'évaluera en 1729. La portée dynamique se caractérise par le fait que la fonction apply de l'évaluateur prend non pas deux arguments (l'opérateur et l'opérande) mais trois, le troisième étant l'environnement dans lequel l'application se fait. Alors que dans un langage à portée lexicale une fonction est chargée de retenir son environnement de définition, dans un langage à portée dynamique, on lui fournit l'environnement ad hoc au moment de l'appel. Cela impose plusieurs remarques. Les langages à portée lexicale sont censément (et effectivement) plus faciles à compiler - ceci ne serait pas une raison suffisante pour les préférer s'ils n'étaient également plus facile à manipuler. Il faut cependant modérer ces réflexions. On peut ajouter du dynamique dans un langage à portée lexicale si on passe explicitement l'environnement courant en paramètre à une fonction. (La morale, et nous y reviendrons, est que dans un langage à portée dynamique, une fonction reçoit en argument non seulement ses arguments nominaux mais aussi tout ce qui se trouve dans l'environnement d'appel. C'est ce qui rend les choses difficiles et parfois incontrôlables.) Le problème est d'obtenir cet environnement courant. On ne peut pas imaginer, dans un langage à portée lexicale, une fonction (current-environment) puisque justement, l'appel d'une fonction ne reçoit pas l'environnement courant, et n'a donc pas de façon de le retourner. En revanche, on peut imaginer soit une nouvelle forme spéciale dont la valeur en tout point soit l'environnement courant, i.e. let rec eval = function VAL v -> fun env -> v | CURENV -> fun env -> ENVIRONMENT env | ... soit, ce qui est peut-être plus subtil, on peut introduire une forme spéciale non pas au niveau du eval mais au niveau du lookup (d'une variable dans un environnement) - ou, ce qui revient essentiellement au même, imposer certaines contraintes au moment de la création de n'importe quel environnement - à savoir que la variable *this* fait toujours référence à l'environnement courant. C'est essentiellement le choix fait par les langages orientés objets : bien que les méthodes statiques soient effectivement liées à la classe plutôt qu'à l'objet, elles ont néanmoins accès aux variables contenues dans l'instance. C'est là un choix valable, qui fournit la possibilité d'avoir des liaisons dynamiques, au prix de devoir passer systématiquement l'environnement d'appel quand on risque d'en avoir besoin, y compris, s'il y a imbrication de fonctions, d'une fonction à l'autre. La portée statique a du bon, le point le plus important étant celui de la transparence référentielle (le nom d'une variable, une fois la fonction définie, n'est plus important), ainsi que la possibilité de cacher des données à l'intérieur d'une fonction (dont on verra une application critique avec la sécurité par tokens). La portée dynamique a cependant aussi ses avantages. Le fait qu'une fonction puisse prendre des arguments implicitement est souvent utile ; par exemple, si on a tout un jeu de fonctions d'entrée / sortie, typiquement chacune doit prendre un port d'entrée et un port de sortie en argument, et on aimerait parfois mieux que ces arguments restassent cachés (d'autant que ça permet de ne pas savoir exactement quelles fonctions font vraiment de l'entrée / sortie, et que ça facilite les choses si on décide qu'une fonction qui n'en faisait pas doit se mettre à en faire). Pour cela, une façon de s'en tirer avec la portée statique (je ne dis pas que ce soit forcément une bonne idée) est d'officialiser la notion d'argument implicite : une fonction comme (lambda (foo (implicit bar)) (cons foo bar)) aurait l'effet que si on écrit (f 5) (f étant la fonction en question), en fait il faut comprendre (*f* 5 bar) avec *f* valant (lambda (foo bar) (cons foo bar)), c'est-à-dire que l'argument bar, de valeur la variable de nom bar est automatiquement rajouté à l'environnement construit pour l'appel de la fonction. Cela permet la plupart des choses agréables de la portée dynamique (une autre méthode sera présentée dans un instant). La portée dynamique a aussi un intérêt plus subtil, c'est celui d'assurer une meilleure réflexivité du langage. Par exemple, si on désire tracer tous les appels de la fonction f dans la fonction g, il est commode de povoir écrire ça ((lambda (f) g) replacement-f), ce qui dans un langage à portée lexicale n'a aucun effet. Or cette possibilité est tout de même un des points essentiels d'un langage réflexif. C'est là un dilemme du clair-obscur, déjà mentionné au sujet de l'opacité du corps d'une fonction, savoir s'il faut autoriser l'examen détaillé des données (potentiellement privées) d'une fonction, sachant que c'est nécessaire à la réflexivité mais que cela pose des soucis de sécurité (si ces données devaient servir à cacher des choses privées, par exemple un token de sécurité). On remarque souvent que la structure des liaisons dans un langage à portée dynamique est organisée à la manière d'une ou plusieurs piles (une pile pour l'implémentation « liaisons profondes » (deep binding) et plusieurs piles, une par variable, dans l'implémentation « liaisons superficielles » (shallow binding) - la différence étant uniquement une question d'implémentation et non de sémantique). C'est-à-dire que quand j'écris (f 42) où la fonction f prend un argument nommé foo, cela revient à empiler la liaison foo=42 pendant toute la durée du corps de f et à la dépiler à la fin. (On peut voir, dans le cas des liaisons superficielles, une pile par variable, donc ici une pile du foo ; ou bien, dans le cas des liaisons profondes, une unique pile de frames avec la convention que chaque liaison absente d'un frame donné est cherchée dans le frame antérieur dans la pile.) C'est ce qui se passe *explicitement* dans le langage postscript, où les dictionnaires, c'est-à-dire les frames, sont des objets de première classe (qu'on empile avec begin et qu'on dépile avec end) - manipulés, du reste, de manière assez indépendante des fonctions. De cette considération vient la possibilité fort amusante, dans un langage à portée dynamique, de se passer entièrement d'arguments aux fonctions. En effet, chaque fonction prend, implicitement, l'environnement d'appel comme argument, et tous les arguments qu'elle désire peuvent lui être passés comme liaisons dans l'environnement en question. Toutefois, pour que ceci puisse marcher, il faut la possibilité de créer des environnements et d'y évaluer des expressions, ce qui ne peut plus se faire par des fonctions (puisque les fonctions ne prennent plus de variables) mais ce qui impose de nouvelles formes spéciales. On obtient un langage dont la syntaxe concrète pourrait ressembler à ceci : ( print!) Ce qui signifie : enrichir l'environnement courant en rajoutant les bindings string="Hello, world!\n" et output-port=stdout, et dans cet environnement exécuter la fonction print (le point d'exclamation signifiant l'application fonctionnelle, à zéro arguments, par opposition au simple lookup de la valeur de print ; sinon, il faut utiliser la convention désagréable du PostScript où une fonction est automatiquement appliquée quand on cherche sa valeur, sauf si on utilise get pour ce faire). On se rapproche-là d'un langage à pile, à la syntaxe pas formidablement agréable : ( compare!); then:{1}; else:{( subtract!)> factorial!); multiplicator:n> multiply!)}> test!)}; n:10> factorial!) devrait calculer 10!. Ce langage a cependant un intérêt notable, comme le PostScript, c'est que les constructeurs FUNCTION et PROGRAM ne sont plus distingués : tous deux, notés par des {...} dans la syntaxe concrète ci-dessus, définissent des objets qu'on peut évaluer (ou appliquer, cela revient au même) avec !, et on est de facto dans le cas (a) de l'alternative mentionnée précédemment au sujet de la réalisation des fonctions (ici, VAL PROGRAM est identique à VAL FUNCTION, ce qui nous sauve). La différence, tout de même, avec un langage à pile, est que la pile (ou les piles, comme on voudra) n'est pas explicitement manipulable, et qu'il n'existe pas de pop ou de chose comme ça. Par exemple, on ne peut pas faire de stack underflow. Une (autre) façon de simuler la portée dynamique dans les langages à portée lexicale consiste à introduire une forme fluid-let (ou dynamic-let) : l'idée en Scheme ce serait que (fluid-let ((foo 42) (bar 1729)) expr) soit du sucre syntaxique pour (let ((old-foo foo) (old-bar bar)) (set! foo 42) (set! bar 1729) (let ((result expr)) (set! foo old-foo) (set! bar old-bar) result)) (en fait, les choses sont plus compliquées si expr peut appeler une continuation, et il faut utiliser dynamic-wind, pour garantir que les valeurs old-foo et old-bar seront rendues à foo et bar quelle que soit la méthode utilisée pour terminer expr ; mais ignorons ces difficultés techniques pour le moment). Cela revient à implémenter effectivement des piles de valeurs dans le langage à portée statique. Reprenons nos environnements. Un environnement c'est quelque chose qui a une clé associe une valeur. C'est également ce qu'on attend d'un type enregistrement. On peut donc désirer unifier les deux. Si r.a est la syntaxe utilisée pour désigner le lookup d'une variable a dans un environnement / enregistrement r, alors a revient au même que *this*.a (ou, du reste, que *this*.*this*.*this*.a). Et même, si on veut, le point peut n'être qu'une forme spéciale syntaxique du eval, c'est-à-dire que l'expression r.(+ a b) peut servir à calculer (+ r.a r.b), la somme des valeurs de a et b de l'enregistrement r - c'est essentiellement le « with » du Pascal qu'on retrouve-là. Sur ces profondes réflexions, changeons de sujet. ********************************************************************** PARTIE IV : MUTABILITÉ En ML, les variables contenues dans les environnements sont par défaut immuables. Pour obtenir une variable mutable, il faut utiliser une indirection. Cette solution me semble bonne. Car, de fait, la plupart des variables qu'on rencontre dans un programme (fonctionnellement bien écrit) sont immuables. La récursion terminale remplace souvent la mutabilité. Le fait de savoir qu'une variable sera immuable permet souvent au compilateur de faire des choses très malignes - et pourtant on ne perd rien en expressivité à imposer l'utilisation de pointeurs pour tous les objets mutables (en tout cas il ne me semble pas qu'il y ait là de contradiction flagrante avec le principe (2)). Le type pointeur posséderait donc trois méthodes principales : l'une, appelée ref, prend une valeur quelconque et renvoie un pointeur sur cette valeur. La deuxième, deref, prend un pointeur et renvoie la valeur pointée. La troisième, set, prend un pointeur et une valeur, et modifie la valeur pointée pour être la valeur fournie. En Scheme on peut implémenter ça par (define (ref foo) (cons foo '())) (define (deref foo) (car foo)) (define (set foo bar) (set-car! foo bar)) ou par (define (ref foo) (lambda (order) (case order ((deref) foo) ((set) (lambda (bar) (set! foo bar)))))) (define (deref foo) (foo 'deref)) (define (set foo bar) ((foo 'set) bar)) Il faut bien noter que le set! en Scheme est une forme spéciale (son 2e argument est une variable, non une variable quotée - comparer avec set et setq en emacs-lisp) alors que set-car! ou set-cdr!, ou encore le set que nous venons de définir, est une fonction ordinaire. D'après le principe (9), on évitera ce genre de choses. Si on possède des variables mutables, et un set!, on sera tenté d'utiliser ce fait, et tôt ou tard on va se retrouver dans la situation désagréable classique, c'est-à-dire qu'on veut modifier une variable x, mais que certaines personnes ont pu faire une copie de x, et qu'on n'a pas de façon de modifier toutes les copies de x. Avec des pointeurs, la situation est claire : si x est un pointeur, quand quelqu'un veut faire une copie, soit il prend une copie y de x, auquel cas faire (set x 42) aura l'effet que (deref y) vale 42, soit il prend une copie de (deref x), auquel cas il veut ne pas être affecté par les changements ultérieurs de x. Dans le cas des variables mutables, on ne peut pas s'arranger pour faire un aliassing, dans le cas des pointeurs on le peut, et on sait ce qu'on fait. Ce qui rend la manipulation des pointeurs désagréable en C, ce ne sont pas les pointeurs en eux-mêmes, c'est l'absence de garbage-collection. ********************************************************************** PARTIE V : TOKENS DE SÉCURITÉ, LOGIQUE ET DÉMONSTRATIONS Les tokens de sécurité, ça fait un moment que j'en parle, il serait temps d'expliquer ce que j'entends par là. L'idée de base est très simple : il s'agit d'un type de données qui possède un prédicat d'égalité bien défini, et pour lequel il existe une unique fonction constructrice, appelée create-token. create-token renvoie un token garanti unique. Voici un exemple d'utilisation en Scheme : (define give-password #f) (define return-secret #f) (let ((token (create-token))) (set! give-password (lambda (password) (if (equal? password "FOOBAR") token #f))) (set! return-secret (lambda (tok) (if (eqv? tok token) "The answer is 42" #f)))) l'idée est donc très simple : les fonctions read-password (l'autentificateur) et return-secret (la fonction protégée) partagent un environnement commun dans lequel se trouve un token créé par create-token. La seule façon d'accéder à ce token est donc d'utiliser read-password en lui fournissant le bon mot de passe. Et posséder ce token est la seule façon d'utiliser return-secret. Sauf qu'en pratique on préférerait avoir une variable globale appelée *tokens* qui serait une liste des tokens possédés par l'utilisateur. Ce qui donne donc : (define *tokens* '()) (define (add-token! tok) (set! *tokens* (cons tok *tokens*))) (define (have-token? tok) (if (memv tok *tokens*) #t #f)) et leur utilisation : (define give-password #f) (define return-secret #f) (let ((token (create-token))) (set! give-password (lambda (password) (if (equal? password "FOOBAR") (begin (add-token! token) #t) #f))) (set! return-secret (lambda () (if (have-token? token) "The answer is 42" #f)))) Bref, le token en question représente la permission d'utiliser la fonction (return-secret). Elle s'obtient en utilisant la fonction (give-password). Les tokens peuvent donc servir à définir et échangers des permissions entre fonctions / procédures utilisateur. Ils peuvent également servir à contrôler des permissions associées au système et constituer tout le mécanisme de sécurité. À ce niveau-là il faut en venir à parler de preuves et de typage. Dans un langage comme ML, le typage remplit deux fonctions disctinctes, et les remplit mal toutes les deux. La première est de mettre de l'ordre dans les pensées du programmeur et la seconde est de lui permettre d'obtenir des invariants vérifiés statiquement sur son programme et par cela de faire moins d'erreurs. Ces deux buts sont louables, mais le système de typage ne convient pas vraiment à l'un ou à l'autre. L'ennui c'est que les invariants qu'on obtient par un système de typage, étant donné que leur démonstration est automatique, ne sont jamais très profonds, et qu'il n'y a pas de moyen de les enrichir ou de les préciser. Par exemple, je peux définir en ML un type tree = Leaf of int | Node of tree*tree mais je n'ai pas le moyen de définir un type des arbres vérifiant des conditions supplémentaires précises, que je veux vérifier à tout moment dans le programme, par exemple, que l'entier associé à une feuille est toujours au plus égal à la profondeur de la feuille (je peux bien définir un prédicat goodtree = let rec g n = function Leaf k -> (k<=n) | Node (t1,t2) -> (g(n+1)t1&&g(n+1)t2) in g 0;; et je peux tester dynamiquement que ce prédicat est vérifié à tout instant, mais je ne peux pas le prouver et demander au compilateur de vérifier ma démonstration). Par ailleurs, au niveau de l'organisation mentale, ML pèche par l'absence totale de sous-typage : les types sont tous disjoints et les constructeurs sont non réutilisables, ce qui fait qu'on a souvent le choix douloureux de rajouter des constructeurs désagréablement inutiles ou bien de fusionner deux types et de perdre de la clarté mentale. Il est relativement facile d'imaginer un système de vérification de preuves. Ce qui est en fait plus difficile c'est de l'intégrer au langage. L'ennui c'est qu'on ne veut pas juste un vérificateur statique. Le principe (2) entre autres nous demande de privilégier généralement le dynamique sur le statique. Il se peut qu'un objet ne soit disponible, ainsi que des démonstrations à son sujet, qu'au cours de l'exécution d'un programme, et qu'il ne soit pas statiquement vérifiable, et ce serait une limitation abusive sur le langage que de n'autoriser (comme en ML) que des invariants statiques. D'ailleurs, le langage doit pouvoir être interprété, ce qui signifie que tous les systèmes de preuve seront alors rendus dynamiques. Le système universel dans ce domaine, c'est finalement le run-time check (on y revient tout de même). Attention ! Il ne s'agit pas simplement d'avoir une fonction abort telle que (abort foo) arrête l'exécution si foo n'est pas vrai. Parce que ça me fait une belle jambe si (abort #t) me laisse continuer mon programme - or c'est tout ce que abort verra du prédicat : un #t (ou assimilé) ou un #f. Je voudrais que, si abort me laisse passer, elle me donne en échange un certificat de bonne conduite. C'est-à-dire que si j'introduis un run-time check pour vérifier que x=42, alors je veux récupérer une certification de ce fait. Or si j'écris (abort (eqv? x 42)), tout ce que abort verra c'est #t (puisque (eqv? x 42) est évalué) et il aura bien du mal à savoir quel test j'ai effectué, et à me certifier ma valeur de x. Pour me donner un certificat, abort, s'il n'est pas une forme spéciale (revoir (9)), devra recevoir le nom de la variable sous une forme non-opaque. On peut déjà imaginer la chose suivante : (define certify-value (let ((token (create-token))) (lambda (variable value) (if (not (eqv? (lookup variable)) value) (die "Certification failed!\n") (list token variable value))))) sauf qu'il y a beaucoup à redire à cela. D'abord, le lookup n'existe pas en Scheme, et de toute manière il faudrait spécifier un environnement, et le certificat devrait contenir cet environnement. Ensuite, puisque les variables sont modifiables, tout ce que ce truc peut certifier c'est qu'à un certain moment la variable *a eu* la valeur désirée (un instant plus tard ça ne vaut plus rien) - d'où un intérêt de plus de garantir l'immuabilité des variables une fois l'environnement créé. Enfin, et c'est sans doute le plus grave ici, le certificat est trivialement pipotable, puisque la liste renvoyée est elle-aussi mutable, on peut donc en changer le 2e et le 3e éléments. À moins d'utiliser une signature PGP ou un truc du même calibre, il n'y a pas de moyen de contourner ça. On a clairement besoin de structures de données immuables ici. Mais à ceci près, l'idée y est. On peut ensuite créer une fonction plus générale, certify, telle que par exemple (certify '(~eq~ x 42)) (en fait, plutôt, (certify '(~eq~ x 42) env), où env est un environnement qui va bien) renvoie un certificat du fait que x vaut 42 (dans l'environnement en question). Sinon, il meurt (c'est-à-dire en fait qu'il soulève une exception : on peut toujours attraper l'exception, mais on ne peut pas récupérer un certificat à tort). Ces certificats constituent ce qu'on appelle des démonstrations. On peut ensuite les combiner en autres démonstrations. Par exemple, si x est une démonstration de A et y une démonstration de A=>B, alors (apply-proof y x) retourne une démonstration du fait que B (et meurt si x ou y n'a pas le bon type). Enfin, on a une fonction use-proof : si x est une démonstration de A, alors (use-proof A x) ne fait rien du tout, et sinon il meurt. Donc en gros tout ressemble à des run-time checks. Mais si le compilateur est malin il fait certaines vérifications (voire toutes si les démonstrations sont complètes) au moment de la compilation. Par exemple, si j'écris (let* ((x 42) (proof (certify '(~eq~ x 42)))) ...) il n'y a pas besoin d'être extrêmement doué pour faire la vérification en statique. Que se passe-t-il en présence d'effets de bord ? Si p est un pointeur, certifier quelque chose sur la valeur de (deref p) ne vaut pas grand-chose si c'est juste à un instant dans le temps. Il faut pouvoir associer des callbacks à chaque appel de set. Ainsi, on doit pouvoir obtenir un certificat du fait que (deref p) est toujours pair en échange de l'installation (irrévocable) d'un callback qui vérifie que l'argument val est pair et meurt (ou du moins déclenche une exception *sans* modifier la valeur) dans le cas contraire. C'est-à-dire qu'à chaque pointeur doit être associée une liste de callbacks à exécuter à chaque appel de set. On doit encore avoir la possibilité de faire des hypothèses, c'est-à-dire d'appliquer le théorème de déduction (ce qui s'appelle encore, faire des fantaisies). Ce point-là est délicat. Cela revient à ouvrir un monde virtuel dans lequel une certaine assertion A est vraie, et, de plus, dans lequel on en a une preuve x. On travaille alors avec x, et on obtient éventuellement une démonstration d'une assertion B. Quand on quitte la fantaisie, celle-ci se transforme en une démonstration de A=>B. Essentiellement, cela revient à faire (lambda (x) ) dans le sens que si on l'applique à x démo de A on obtient une démo de B. Sous Curry-Howard, et dans un langage fonctionnel pur dénué d'effets de bord, c'est la même chose ; mais là il y a quand même des choses qui clochent. J'ai les idées assez confuses, mais je pense qu'on peut faire deux choses : soit utiliser un lambda normal sans restriction, auquel cas on obtient une démonstration de A=>B mais marquée comme spécieuse, c'est-à-dire que dès qu'on fera un apply-proof dessus il faudra vraiment évaluer la fonction pour regarder cette démonstration en détail (en effet, le corps des fonctions n'est regardé qu'au moment de l'application de la fonction, pas au moment de sa définition), parce qu'elle peut être pipo, et on ne le saura qu'au moment où on aura une démonstration x de A pour l'appliquer. Par exemple, si la démo de B utilisant x introduit des run-time checks et des choses comme ça pour arriver à ses fins, on ne peut pas la vérifier avant d'exécuter effectivement le corps de la fonction, et d'avoir véritablement une démonstration de A ; c'est-à-dire qu'une fonction prenant une démonstration de A et renvoyant une démonstration de B ce n'est pas vraiment la même chose qu'une démonstration de A=>B contrairement à ce que disent les intuitionistes ; et du reste, comment savoir qu'il est vraiment retourné une démonstration de B avant d'évaluer la fonction, qui peut du reste très bien boucler et ne jamais retourner ? Bref, c'est le bordel et les choses ne sont pas claires. L'autre façon, qui me plaît mieux mais au prix d'un certain sacrifice de Curry-Howard, c'est de ne pas identifier l'abstraction fonctionnelle avec la création de fantaisies. En gros, on fait quelque chose comme (abstract '((x A)) proof), et proof est évalué dans un monde fantaisiste dans lequel x est bindé à une démonstration de A. Même si proof arrive à des absurdités, crashe le système, ou fait d'autres sottises dans le même genre, ce n'est pas grave, c'était un monde fantaisiste (ahem, revenir en arrière d'un crash système ça risque d'être technique, mais passons - les capacités de virtualisation de Tunes sont infinies). Et pour ce qui est de la méthode antérieure, si on a une fonction f prenant une démo x de A et retournant une démo de B, on peut obtenir une démo de A=>B en faisant cette fois (abstract '((x A)) '(f x)). Bref, tout cela est vaguement fumé et l'ordre applicatif d'évaluation ne se mélange pas très bien avec Curry-Howard (en évaluation paresseuse, les choses se passeraient nettement mieux). (À la limite, ce point concernant le théorème de déduction n'est pas grave. On peut s'en passer quitte à utiliser les combinateurs S et K de Hilbert.) Il faut enfin pouvoir faire des preuves sur les fonctions. Là, je suis toujours perdu. C'est à make-fun ou son équivalent de renvoyer des démonstrations en plus de la fonction formée, mais le modus operandi n'est pas clair. En gros, si f est (lambda () 42), ou, mieux, (lambda () (let ((result 42)) (certify '(~eq~ result 42)) result)), il faut que je puisse récupérer un certificat du fait que (f) vaut 42, ce qui implique que quelqu'un analyse le corps de la fonction, y voie le certify et... berk, je ne sais plus où j'en suis. Quelqu'un a une idée géniale ? -+- Danger ! Logique linéaire à l'avant ! -+- Je continue avec quelques réflexions sur la logique linéaire. Je noterai * (fois), | (par), & (avec) et + (plus) pour les quatre opérations de la logique linéaire, 1, F, T et 0 leur élément neutre, ! et ? les exponentielles, ~ la négation, et -> (avec A->B = B|~A) l'implication linéaire. Je noterai ]- pour le signe « thèse » (« ] » afin qu'il n'y ait pas de confusion possible avec « | »). Ce qui distingue la logique classique de la logique intuitionniste c'est la présence de la loi de Pierce, où ((A=>B)=>A)=>A. Or celle-ci est précisément démontrée, quand on fume assez de Curry-Howard, par la fonction call/cc (qui prend une fonction de type (A=>B)=>A et applique celle-ci à la continuation courante, de type A=>B, renvoyant A, que ce soit par appel explicite de la continuation ou par retour normal). Une démonstration en calcul des séquents s'obtient ainsi : ------ A ]- A -------- A ]- A,B ---------* ------ ]- A=>B,A A ]- A ------------------ (A=>B)=>A ]- A ----------------- ]- ((A=>B)=>A)=>A l'étape qui n'est pas valable en logique intuitionniste (si on interprète la virgue dans les conséquences comme un OU) a été notée par une astérisque à droite : c'est la règle X,A ]- B,Y ----------- X ]- A->B,Y qui n'est valable qu'à condition qu'on possède une technique de continuation (essentiellement, on prétend être de type A->B jusqu'à recevoir quelque chose de type A, auquel cas on peut appliquer la fonction de départ : si on tombe dans le type B, on est content, sinon on revient en arrière et on prétend être dans un des types Y). Soit. L'ennui avec la logique classique, c'est que pour tout token de sécurité, soit j'ai ce token, soit j'ai le pouvoir de devenir root (obtenir le token faux) si je l'ai. Bref, le « ou » n'a pas vraiment un sens de « ou ». Et, accessoirement, si j'ai (A=>F)=>F alors j'ai A, parce que (define (remove-not-not f) (call/cc (lambda (k) (f (lambda (x) (k x)))))) ou même, en encore moins lisible : (define (remove-not-not f) (call/cc (lambda (k) (f k)))) voire (define (remove-not-not f) (call/cc f)) ou carrément (define remove-not-not call/cc) (en fait, ce n'est pas tout à fait (f k) mais (absurd (f k)) où absurd est de type F=>A) (en gros, quelqu'un me dit (f) que A->F c'est absurde, moi je lui réponds que j'ai un A->F et que je ne vois pas pourquoi c'est absurde, et pour me montrer que c'est absurde il est bien obligé de me donner un x:A, moment auquel je capture son x et je dis que j'ai trouvé un x:A). Bref, la logique d'un système avec call/cc, c'est-à-dire en fait avec la possibilité de revenir dynamiquement en arrière ou en avant dans le flot de contrôle (ou encore, d'explorer différentes possibilités) est forcément une logique dans laquelle ~~A = A. Ce qui nous laisse la possibilité de la logique classique ou de la logique linéaire. Cette dernière a l'avantage que la logique intuitionniste en est un fragment (un théorème dû à Girard). La logique linéaire est pour plusieurs raisons une logique naturelle pour l'informatique. Un simple exemple : la fonction exit est une fonction qui termine le thread courant. Elle a donc pour type 1->F. En logique classique, ça fout *légèrement* la m***e. (Évidemment, on peut arguer que de toute façon les logiques associées à n'importe quel langage non trivial (i.e. *pas* coq) sont contradictoires puisque par exemple let rec f = function () -> f ();; démontre unit -> 'a, c'est-à-dire justement ce 1->F ; mais boucler et quitter ce n'est pas exactement la même chose et on voudrait que la logique le reflétât.) En logique linéaire, 0 permet de montrer n'importe quoi, mais pas F (d'ailleurs, F n'a à peu près aucune conséquence remarquable). La logique linéaire, disais-je, avec peut-être un axiome supplémentaire assez sympathique, à savoir !(1|1). Au cas où ça ne vous paraîtrait pas parfaitement clair, 1|1 est le type de la fonction fork, qui permet de créer deux threads parallèles à partir d'un. D'ailleurs, 1|1 ]- A*B->A|B, ce qui se démontre comme ceci : ---- ---- A]-A B]-B ------ ------ 1,A]-A 1,B]-B -------------- 1|1,A,B ]- A,B -------------- 1|1,A,B ]- A|B -------------- 1|1,A*B ]- A|B --------------- 1|1 ]- A*B->A|B et on peut préférer voir la fonction fork comme ayant type A*B->A|B (si j'ai deux objets A et B alors je peux les paralléliser). Accessoirement, un (fork x1 ... xn) peut se voir comme ayant type A1|...|An où A1,...,An sont les types de x1,...,xn. Dans ce cas, (fork) tout seul équivaut à (exit) (création de zéro threads pour remplacer le thread en cours) et il a bien pour type le par de rien du tout, c'est-à-dire F. Plutôt qu'un fork, le par désigne en fait un amb, fonction qui retourne un de ses arguments de manière non déterministe. Cela expliquerait que la réciproque A|B->A*B ne soit certainement pas vraie (il suffit de l'appliquer à 0 et T, ce qui donne 0|T->0*T, soit T->0, pour se rendre compte que si elle est vraie, les choses ne sont *vraiment* pas jolies-jolies), alors qu'on pourrait naïvement le croire (si j'ai deux threads A et B, je peux bien attendre dans A le retour de B et mettre ensemble les deux résultats, non ?). Bref, faut-il essayer de forcer un système ayant une logique linéaire ? Entre autres, faut-il imaginer des variables qui disparaissent sitôt qu'on les utilise ? Pour des tokens de sécurité, ça peut être intéressant (on peut me donner le choix entre deux droits, ce qui n'est pas pareil que me les donner tous les deux en même temps). Pour de la programmation générale, je ne crois pas trop, mais on ne sait jamais. -+- Danger ! Logique linéaire à l'arrière ! -+- ********************************************************************** PARTIE VI : ÉVALUATION PARESSEUSE La base de l'incorporation de l'évaluation paresseuse dans un langage utilisant l'évaluation hâtive, c'est une fonction (ou forme spéciale) delay, qui prend une expression (directement si c'est une forme spéciale, quotée - i.e. sous forme de VAL PROGRAM - si c'est une fonction) et qui retourne une promesse d'évaluer cette expression. C'est-à-dire qu'il s'agit d'un eval retardé. En Scheme, le fait de forcer la promesse se fait manuellement avec la fonction force. En Unlambda, c'est automatique lorsqu'on applique la promesse (créée avec la forme spéciale d) à quelque chose. En rétrospect, il apparaît plus raisonnable, lorsqu'on effectue une opération sur une promesse (par exemple, la passer en argument à une fonction) de retourner une promesse de faire cette opération plus tard. Par exemple, (+ (delay 2) 2) devrait renvoyer une promesse de calculer 4 (en ajoutant 2 au résultat de la promesse précédente). Dans ces circonstances, une promesse comme (delay (* (+ x 1) 7)) peut encore s'écrire (* (+ (delay x) 1) 7) (il y aurait des différences importantes, par exemple, entre (+ (delay x) (foo)) et (delay (+ x (foo))) en ce que dans le premier cas la fonction foo est appelée au moment où la promesse est formée et dans le second cas au moment où elle est forcée - naturellement dans un langage fonctionnel pur, cela ne change rien), et il s'agit de la promesse de calculer 7(x+1). De quel x s'agit-il ? Autrement dit, si on écrit (let ((x 1729)) (force (let ((x 42)) (delay x)))), quelle est la valeur retournée ? Si on croit à l'évangile de la portée lexicale, la réponse est naturellement 42 (en tout cas, c'est le cas en Scheme). Autrement dit, les promesses sont des fermetures, et gardent la mémoire de l'environnement dans lequel elles ont été créées. Ce point de vue a l'avantage de distinguer deux choses normalement associées dans la construction d'une fonction : le binding des paramètres (bêta-réduction) et le retard à l'évaluation du corps, ce dernier n'existant pas dans un pur lambda-calcul. D'ailleurs, on peut même trouver que cette association est contre nature et qu'elle est une insulte à la face divine de Curry-Howard. Car, quand un langage comme le ML utilise des types genre unit -> 'a pour indiquer que la fonction a un effet de bord, et qu'on retarde celui-ci jusqu'à ce qu'on lui fournisse un objet de type unit, cela viole la conception fondamentale d'unit suivant laquelle unit -> 'a et 'a sont en tout point isomorphes (et 'a -> unit isomorphe à unit). Dans un langage à ordre d'évaluation normal (call-by-name, par opposition à l'ordre d'évaluation hâtif ou call-by-value) un appel de fonction (f a (b 6) c) commence par effectuer la bêta-réduction de tête, c'est-à-dire celle de l'expression tout entière, plutôt que celle de (b 6) (ni même que le lookup des variables). (Le call-by-need, ou évaluation paresseuse, ne diffère de cela qu'en ce qu'une mémoïsation est rajoutée pour éviter l'évaluation multiple d'une même expression.) En toute logique, on ne doit pas interdire non plus d'effectuer des évaluations à l'intérieur d'un lambda, puisque le lambda-calcul le permet bien ; par exemple, (lambda (a) (print "Foobar!\n")) devrait afficher Foobar! (mais le lambda lui-même ne sera évalué que si son tour vient, ainsi ((lambda (ignore) 'nothing) (lambda (a) (print "Foobar!\n"))) n'a aucun effet). Un langage fonctionnel pur se combine mal avec les effets de bord (on ne sait pas trop quand ceux-ci vont avoir lieu, et le simple lookup d'une variable peut produire des effets de bord). Une solution à envisager, et dont je ne sais pas trop ce qu'elle donne, est d'utiliser d'une part la logique linéaire (pour savoir précisément combien de fois chaque chose est appelée) et d'autre part de l'essence pour produire les effets de bord, c'est-à-dire que le programmeur a à sa disposition une variable de type !Fuel et que les fonctions qui produisent un effet de bord sont de type Fuel->1 (sous-entendu ici que la fonction ne renvoie rien). ********************************************************************** PARTIE VII : DYNAMIQUE DU LANGAGE Le simple traitement des exceptions ne nous suffit pas, et on exige une fonction call/cc digne de ce nom. Partant de là, on peut s'étendre dans différentes directions. Au niveau des valeurs, de même qu'une fonction peut prendre plusieurs arguments (en fait, dans la vision « purement paresseuse » évoquée ci-dessus, il vaudrait mieux dire : qu'une expression peut avoir plusieurs variables libres), il serait agréable qu'une fonction pût retourner plusieurs valeurs. Les fonctions values et call-with-values du Scheme (introduites dans le R5RS je crois) sont une approche timide vers cette destination. Cela dit, un langage dans lequel serait entièrement respectée la dualité entrée / sortie de la logique linéaire, cela pourrait être passablement impressionnant et beau (mais très difficile à programmer) - les arguments d'une fonction, notamment, sont constitués en environnement et reçoivent des noms, il devrait donc en aller de même des résultats produits. Toujours est-il que, très pragmatiquement, je suis assez fâché du manque de traitement des valeurs produites en Scheme lorsque j'ai une fonction disons (foobar) (de zéro arguments) qui retourne une liste de trois valeurs et que je veux binder ces valeurs à des variables : il semble que la façon la plus simple soit (define a #f) (define b #f) (define c #f) (let ((triple (foobar))) (set! a (car triple)) (set! b (cadr triple)) (set! c (caddr triple))) Au moins en ML on peut utiliser le pattern-matching et écrire let (a,b,c) = foobar ();; - il y a là un début de traitement correct des valeurs retournées, mais pas encore très satisfaisant (confusion, par exemple, des opérations * et |). Cela concerne donc les continuations prenant plusieurs valeurs en paramètres (typiquement, les continuations produites par le call-with-values du Scheme). Il y a aussi la question du nombre de continuations. Dans un langage logique tel que le Prolog, chaque expression a deux continuations : une continuation de succès et une continuation d'échec. Les deux opérations booléiennes, avec eval AND(expr1,expr2) succ_cont fail_cont = eval expr1 (fun _ -> eval expr2 succ_cont fail_cont) fail_cont eval OR(expr1,expr2) succ_cont fail_cont = eval expr1 succ_cont (fun _ -> eval expr2 succ_cont fail_cont) permettent de gérer les exceptions avec parfois assez d'élégance ; c'est un embryon de cela qu'on voit dans certaines écritures en perl ou en shell, comme open foobar or die "Can't open foobar"; (bien sûr, le lecteur perspicace aura sans doute remarqué qu'il n'y a pas de différence essentielle entre avoir deux continuations et avoir une continuation qui prend des valeurs dans un type union, comme c'est, de facto, le cas dans l'exemple perl ci-dessus, avec soit Faux soit un descripteur de fichier comptant pour le Vrai). À partir du moment où on se permet deux continuations, pourquoi ne pas s'en permettre trois, quatre, autant qu'on veut : on s'achemine là-encore vers un langage peut-être très élégant mais difficile à manipuler sans faire des graphes affreux dans tous les sens (un langage graphique ? serait-ce Delphi ?). Les continuations de première classe (montantes et descendantes) c'est joli et en plus ce n'est pas inutile. Le plus important c'est pour le multithreading. Si j'ai plus de processus que de processeurs, vous vous imaginez peut-être que je vais m'amuser à sauvegarder ma pile avec des instructions de bas niveau, et autres horreurs du même calibre ? Que nenni ! Le multi(tâche|threading) se fait au moyen de continuations appelées cycliquement par un scheduler. (Naturellement, les appels de continuations pourront être implémentés en termes de task state segments, ou je ne sais quelle autre gimmick le processeur fournit - mais cela ne nous concerne pas vraiment, c'est au compilateur de faire l'abstraction nécessaire.) Chaque tâche doit avoir, en privé, un peu plus que sa simple pile. Par exemple, chaque tâche a sa liste de token à elle. Une commutation des tâches, effectuée par le scheduler, doit restaurer tous les tokens de la tâche destination. Il ne s'agit pas de penser naïvement qu'il y a une variable *tokens* par tâche : cela ne convient pas à un langage à portée lexicale (les fonctions du système, et donc celles qui vérifient les tokens disponibles, verront la variable *tokens* qui était dans l'environnement où elles ont été définies, donc ce doit bien être une variable globale et non une variable locale à la fonction principale du thread qui est en cours d'exécution). On peut repousser le problème en déclarant que *tokens*, comme quelques autres variables du même accabit, font partie d'un descripteur de tâche, accessible par la variable *current*. Encore faut-il que celle-ci soit bien positionnée. C'est au scheduler de le faire. Mais plutôt que de le faire manuellement il vaut mieux que les contextes dynamiques d'exécution puissent être entourées de colle dynamique, c'est-à-dire d'un prélude et d'un postlude, tels qu'implémentés par la fonction Scheme dynamic-wind : (dynamic-wind pre body post) évalue (body), avec la garantie que (pre) (qui est censé être un thunk) sera évalué avant toute entrée dans body et (post) après toute sortie de body, y compris si cette entrée ou cette sortie se font par appel de continuations de première classe. Par exemple, (define x 0) (call/cc (lambda (k) (dynamic-wind (lambda () (set! x 42)) (lambda () (k x)) (lambda () (set! x 0))))) renverra 42 (la valeur de x dans le body, passée directement à la continuation de sortie), mais en gardant la valeur de x à 0 (puisque le postlude est exécuté malgré la sortie par (k x)). C'est aussi le dynamic-wind qui permet de faire fonctionner correctement le fluid-let (mentionné précédemment) dans le cas des langages possédant des continuations de première classe. (D'ailleurs, l'échantillon ci-dessus pourrait s'écrire (call/cc (lambda (k) (fluid-let ((x 42)) (k x)))) - quoiqu'ici un bête let ferait le même effet.) Revenons au scheduler. On pourrait croire que celui-ci ne peut pas s'écrire dans le langage, qu'il faut des choses mirifiques et spéciales pour écrire un scheduler. Il n'en est rien. La seule difficulté consiste à assurer le retour au scheduler depuis les tâches appelées. Pour cela, on peut envisager différentes méthodes. La plus simple et la plus portable (mais aussi la plus lente) consiste à imaginer une fonction single-step qui prend un thunk, l'exécute pendant un court moment (non spécifié - mais on imagine un seul appel d'eval) et retourne à l'appelant en renvoyant à celui-ci une continuation - de zéro arguments - permettant de continuer l'exécution (de sorte qu'appeler de nouveau single-step sur cette continuation ait l'effet de continuer l'exécution pour un nouveau pas). On peut encore imaginer une fonction alarm qui fasse le même effet après un certain quantum de temps ; il faut naturellement faire attention à ce qu'une alarme ne vienne pas interrompre le scheduler lui-même pour revenir à l'utilisateur (mais il y a différentes méthodes très faciles pour éviter ça, la plus simple étant de protéger la fonction alarm par un token et de donner aux utilisateurs une nouvelle fonction alarm gérée par le scheduler lui-même). Notons que des fonctions de même calibre permettent de « stracer » une fonction ; par exemple, on peut imaginer une fonction trace-calls qui prenne un thunk et exécute celui-ci jusqu'au premier appel de fonction, renvoyant alors à la fois la fonction en question, ses arguments, et une continuation permettant de continuer le calcul, cette continuation prenant en argument une nouvelle fonction et de nouveaux arguments de sorte que l'on peut non seulement observer mais même modifier les appels de fonctions dans une expression ; on peut imaginer la même chose pour les lookups de variables, etc. De telles fonctions doivent naturellement être protégées par tout un système de sécurité (il serait de mauvais goût, par exemple, de se mettre à stracer les fonctions du système, et d'en récupérer des tokens importants - c'est la même chose qui fait que les programmes setuid sous Unix ne peuvent pas être stracés). Elles constituent un compromis envisageable au dilemme du clair-obscur sur la lisibilité des fonctions (là, on ne peut pas lire l'intérieur d'une fonction, mais on peut le sonder étape par étape). Les détails de l'implémentation, encore une fois, sont un peu délicats mais ne nous concernent pas. Revenant au scheduler, il faut remarquer que le fait que le scheduler n'utilise aucune instruction magique ou facilité réservée (comme le passage en ring 0 dans un OS traditionnel) ouvre de nouveaux horizons. Chacun peut écrire son propre scheduler, et donc scheduler, à l'intérieur de ses quanta de temps, entre ses tâches propres. On imaginerait donc plutôt pour le système un scheduling par utilisateur que par tâches - ou bien avec une limitation sérieuse sur le nombre de tâches allouées par utilisateur - ce qui permet d'éviter les attaques DoS à la « while (1) fork(); ». Si un utilisateur veut dépasser son quota, il écrit un scheduler à lui (dans une de ses tâches à lui) qui schedulera entre un certain nombre de sous-tâches. Bref, tout cela est à la fois cause et conséquence de la réflexivité du système : Tunes sait faire tourner Tunes, y compris le scheduler de Tunes. ********************************************************************** PARTIE VIII : TYPAGE ET ABSTRACTION On a vu que le système de typage traditionnel (d'un langage comme ML), en tant que mécanisme permettant de prouver des invariants sur les programmes, devait céder la place à un système plus puissant manipulant dynamiquement des démonstrations de première classe (le typage statique n'apparaissant que comme une optimisation à la compilation du typage dynamique). Reste à considérer le cas du typage en tant que mécanisme permettant de structurer le programme. De ce point de vue-là, le Scheme et le ML sont tous deux insatisfaisants : le premier offre les outils minimaux (même si théoriquement suffisants) pour tout faire, et on est obligé de construire chaque type abstrait, laborieusement, par des méthodes ad hoc (du reste fort bien expliquées dans le Wizard Book) ; le second offre un typage plus agréable mais aussi plus restreint, avec, notamment, aucune possibilité de faire de la surcharge d'opérateurs (ce qui est possible en Scheme par un bête test à l'exécution). De ce point de vue-là, c'est encore, à mon avis, les langages orientés objets qui font ce qu'il y a de mieux, malgré leur pauvreté par ailleurs. Le mieux est cependant de rajouter le minimum au langage. En fait, il n'y a même rien à rajouter au langage, c'est à la bibliothèque de faire des efforts. Par exemple, pour permettre de surcharger +, i.e. de définir des nouveaux types numériques, sans modifier la fonction + elle-même (celle-ci est censée être immuable), il faut la possibilité d'enregistrer (par l'intermédiaire de fonctions de la bibliothèque) des nouveaux types et des callbacks qui leur sont associées : si la fonction + ne sait pas d'elle-même faire l'addition, elle va appeler les callbacks idoines pour faire le boulot. La seule chose à ajouter éventuellement au langage, c'est la possibilité de créer des records (ou même de simples listes) opaques, c'est-à-dire verrouillées par un token, et nécessitant ce token pour en examiner le contenu ou pour en créer. (On pourrait faire ça avec des fonctions, puisque l'environnement de définition est censément inpénétrable, mais alors le système de typage est lui-même vulnérable à une attaque façon « man in the middle » : d'un côté on fournit au système de typage un pipo-objet et de l'autre on fournit un vrai objet à un pipo-système de typage. Chaque opération effectuée par l'un à l'autre est transmise et enregistrée par l'homme au milieu, et quelque part on récupérera bien un token. Je ne sais pas si tout cela est très clair...) ********************************************************************** PARTIE IX : BILAN ET PERSPECTIVES La principale conclusion, c'est qu'un langage parfait comme on en cherche n'est pas si impossible. La tâche la plus difficile consiste probablement à le concevoir et à le spécifier convenablement. L'implémentation, du moins tant qu'il s'agit d'un interpréteur, n'est pas si dure. Écrire un compilateur serait probablement plus chaud. Mais une fois qu'on a l'interpréteur, on peut écrire le compilateur dans le langage lui-même sans sérieux problème de bootstrap. La partie « système » est plus facile que la partie « langage », essentiellement parce que toutes les difficultés dans l'écriture des device drivers ont été négligées (si on cherche dans un premier temps à écrire un système qui tourne sous un autre, c'est logique). Encore que tout ce qui concerne la gestion des fichiers (i.e. de la mémoire, c'est la même chose) n'a pas été envisagé puisqu'on considérait qu'on se basait sur celle du langage dans laquelle l'interpréteur était écrit. En tout cas, l'écriture de Tunes, tant qu'on ne se soucie pas trop d'efficacité (parce que là j'ai quand même mes doutes) ne semble pas un but totalement inaccessible. Espérons-le.