Ours & Hippy — le blog [caml]

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

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

Macaque

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

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

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

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

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

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

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

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

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

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

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

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

La petite histoire

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

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

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

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

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

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

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

Une toute petite modification suffit. Voyez-vous laquelle ?

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

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

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

Quel futur pour Macaque ?

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

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

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

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

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

J’aime bien l’expression problem, mais il n’est pas particulièrement utile dans la pratique logicielle de tous les jours : les langages utilisés aujourd’hui ne permettent pas en général de le résoudre de façon complètement satisfaisante, soit parce que leurs concepteurs ne se sont même pas posés la question, soit parce qu’ils ont estimé que quelque chose de plus statique mais de plus simple était préférable. Car l’extensibilité à un prix, et les solutions sont souvent compliquées ; certains langages en contiennent en fait d’assez satisfaisante, mais elles ne sont pas au cœur du langage (car on préfère se baser sur des choses sûres et éprouvées), et donc relativement de seconde zone dans la pratique des programmeurs : il faut privilégier la simplicité, donc sauf dans les cas où en a vraiment besoin, on évite d’utiliser ces constructions plus délicates.

Ce qui est intéressant, c’est que ce probème est un très bon moyen de voir les liens entre les langages fonctionnels et les langages orientés objet. Il n’est pas spécifique à un seul paradigme, et les différentes solutions révèlent des caractéristiques, à mon avis assez profondes, des différents paradigmes. En deux mots, généralement les langages fonctionnels facilitent l’ajout d’opérations au détriment de l’extensibilité des données, et les langages à objets favorisent les données plutôt que les opérations.

Produits d’opérations

On pourrait ne pas être tout à fait satisfait de la solution des types sommes extensibles : il y a pas mal de code chiant et qui a l’air inutile (on parle de code boilerplate). En effet :

• tout ce qui concerne les expressions sans multiplication est coiffé d’un constructeur supplémentaire. Ça passe mais si on fait trois extensions de suite, trois couches de constructeurs, ça commence à faire lourd ;

• pour la même raison, on ne peut pas réutiliser directement les fonctions des types étendus pour manipuler des éléments de type simple : si on a une fonction qui sait manipuler des nombres, des sommes et des produits, on ne peut pas lui donner directement un élément de expr, alors qu’elle saurait pourtant manipuler les nombres et les sommes. C’est encore plus compliqué si on voulait n’avoir que des nombres et des produits (pas de somme) sur une partie du programme, puisqu’ils ne sont pas dans un type commun ; il faudrait travailler sur expr2 en lançant une erreur si on tombe sur une somme, ce qui n’est pas très propre.

Je vous ai parlé de langages dans lesquels il était plus facile d’étendre les données que les opérations, sans modifier le code existant. Comment faire, et peut-on le faire en OCaml ? La réponse est oui, mais cela demande un changement (assez radical) de point de vue.

Actuellement, les programmes sont centrés autour des données : on définit leur type, et on exprime ensuite, a posteriori, des opérations comme des fonctions qui opèrent sur ce type : c’est aux opérations de faire le travail de tripoter les données pour en extraire un résultat.

On peut voir la situation complètement différemment en se plaçant du point de vue des opérations : on commence par définir les opérations qui nous intéressent, on en fait un type. Ensuite on exprimera des données qui feront le travail d’exploiter les opérations de leurs composants pour produire leurs opérations.

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

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

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

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

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

Voici une autre donnée. C’est à elle de faire tout le travail, elle utilise les opérations de ses composants pour construire ses opérations à elle. Parce que sans opérations, une donnée n’est rien. Vous remarquez que je l’ai ajoutée comme ça, sans rien modifier d’existant.

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

Ça marche. Mais comme on est coquet :

let eval ops = ops.eval
let print ops = ops.print

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

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

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

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

On a une surcouche avec une opération de plus. Celle-ci a de particulier qu’elle demande, pour produire son résultat, un paramètre : un buffer dans lequel est insèrera son contenu. Le sucre syntaxique (qui transforme l’accès à une donnée en fonction) nous rend ici service puisqu’il cache ce détail :

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

Par contre, maintenant qu’on a changé le type des opérations, il faut redéfinir les anciennes données pour supporter cette nouvelle opération, et le sucre syntaxique correspondant aux opérations de l’ancien type.

let int n =
  { rpn = (fun buf -> bprintf buf "%d " n);
    ops = int n }

let add a b =
  let rpn buf =
    a.rpn buf; b.rpn buf;
    bprintf buf "+ " in
  { rpn = rpn;
    ops = add a.ops b.ops }

let eval ops2 = ops2.ops.eval
let print ops2 = ops2.ops.print

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

let mul a b =
  let rpn buf =
    a.rpn buf; b.rpn buf;
    bprintf buf "*" in
  { rpn = rpn;
    ops = { eval = a.ops.eval * b.ops.eval;
            print = sprintf "(%s * %s)" a.ops.print b.ops.print } }

let rpn_test =
  rpn (add (int 1) (mul (int 2) (int 3)))

Caractéristiques de l’approche produit

On a donc l’extensibilité dans les deux dimensions, comme avec les sommes ouvertes. Mais cette fois-ci, on n’a eu besoin que d’une seule itération pour trouver quelque chose de satisfaisant, et c’est relativement simple puisque ça ne demande pas de types paramétrés ni même de traitement de la récursion : la définition des données de ce problème est récursive, mais pas celle des opérations ! En changeant de point de vue on l’attaque donc selon un angle plus simple. Cette méthode a cependant deux défauts assez importants.

D’abord, La définition des données est éparpillée un peu partout, et chacune contient un peu d’information sur les opérations, ce qui rend le code moins facile à suivre (surtout pour des opérations plus complexes) : pour voir la définition d’une opération, il faut trouver ses petits morceaux dans chaque définition de donnée, il n’y a pas de vue d’ensemble.

En réalité il y a un problème symétrique dans le cas des sommes : si l’on considère l’ensemble des effets des opérations sur un cas spécifique de notre structure comme un tout, on se retrouve à devoir lire le code de chaque opérations pour y voir à chaque fois le traitement du cas qui nous intéresse : « Je m’intéresse seulement aux multiplications et pas aux additions : comment sont-elles évaluées ? Comment sont-elles affichées ? » Et les opérations sont définies en plusieurs endroits pour une même donnée, donc ça rend plus difficile la vision d’ensemble sur un cas spécifique. On observe donc vraiment les deux facettes d’une même pièce : il faut pouvoir prendre un point de vue ou l’autre, car l’un pourra être plus adapté que l’autre dans certaines situations.

D’autre part, cette écriture des opérations en fonction des opérations des composants ne marche bien que pour une certaine classe d’opérateurs, les catamorphismes (c’est en gros leur definition : opérateurs que l’on peut définir avec uniquement le résultat d’opérations sur les composants directs de notre donnée). C’est une classe plutôt générale mais certaines opérations n’en font pas partie.

Typiquement, dans le cas d’arbres comme celui qui nous intéresse (les expressions mathématiques forment un arbre dont les nombres sont les feuilles, et les opérations les noeuds), le catamorphisme va favoriser un mode de parcours de l’arbre en particulier (tu parcours chaque fils de ton noeud séparément puis tu réunis les résultats) alors que certains problèmes demandent des modes de parcours différents (par exemple une fonction dont le résultat dépend à chaque fois du père et du fils gauche, au lieu du fils gauche et du fils droit). On peut toujours tout faire rentrer à la hache dans la pensée unique du catamorphisme (qui est assez naturel donc très courant), mais dans certains cas ça donne des codes illisibles.

Dans ce cas, la meilleure solution, au lieu de chercher à accéder intelligemment aux résultats des fils dans le bon ordre, et de mettre une machinerie complexe pour faire passer les résultats dans tous les sens, est souvent de :

• reconstruire l’« arbre » correspondant à la donnée, qui est l’information la plus générale que l’on puisse obtenir, et dont la construction s’exprime comme un catamorphisme ;
• implémenter l’opération à partir de l’arbre, dans un style plus direct.

Le problème est alors : quel type donner à l’arbre ? On se retrouve en fait à définir un type somme, et c’est donc le retour à la case départ : si notre type somme n’est pas extensible, les opérations qui l’utilisent ne le seront pas non plus. Si on veut garder l’extensibilité par les produits d’opérations, il faut donc sacrifier de la facilité à programmer.

POO et motifs de conception

Vous l’aurez peut-être remarqué en lisant ma dernière partie, mais elle est en fait très proche de certaines idées de la POO. L’insistance en particulier sur le fait que les opérations (« méthodes ») font parties du type que l’on définit, au point d’en faire l’élément le plus important du programme. Comme on l’a vu, cela a selon les besoins des avantages, mais aussi des inconvénients.

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

class type expr = object
  method eval : int
  method print : string
end

class int n : expr = object
  method eval = n
  method print = string_of_int n
end

class add a b : expr = object
  method eval = a#eval + b#eval
  method print = sprintf "(%s + %s)" a#print b#print
end

let test = (new add (new int 1) (new int 2))#eval

On peut remarquer que les langages OO aussi auront bien besoin de sucre syntaxique pour alléger un peu tout ça. Par contre, là où une solution objet est intéressante par rapport à notre solution à base d’enregistrements, c’est qu’on peut étendre les opérations avec le mécanisme d’héritage :

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

On peut alors appeler directement les méthodes eval et print sur des objets vérifiant l’interface expr2, sans devoir passer par une couche d’indirection (le .ops de la solution produit). De notre point de vue c’est presque un détail syntaxique, et la première méthode a aussi ses mérites puisqu’elle correspond à la relation de composition qui est souvent considérée par les programmeurs POO comme plus adaptée que l’héritage dans un grand nombre de cas.

Approche somme en POO

J’ai présenté cette vision POO du problème, qui correspond au motif Composite. C’est la méthode la plus naturelle pour un programmeur OO (qui est donc sans le savoir un descendant de la solution produit), mais il est aussi possible d’effectuer un changement radical de point de vue, dans le but de retrouver une approche avec des sommes. Ça correspond au motif Visiteur : au lieu de mettre les opérations dans les méthodes, on met les données.

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

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

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

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

let eval = object (self)
  method int n = n
  method add a b = a#accept self + b#accept self
end

let test_eval =
  let expr = add (int 1) (int 2) in
  expr#accept eval

Cette solution est donc l’analogue OO des types sommes; on peut de plus profiter de la "récursion ouverte" des objets pour obtenir l’analogue de la "somme ouverte" : pas besoin de paramétrer les objets de départ pour les enrichir ensuite, le mécanisme d’héritage suffit. Elle est cependant beaucoup plus difficile à typer (c’est pourquoi elle est plus souvent utilisée dans des langages à typage dynamique qui ne se posent pas la question).

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

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

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

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

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

Types, opérations et extensibilité

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

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

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

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

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

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

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

Expression problem

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

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

type nouveau_type =
  | Ancien_cas of ancien_type
  | Nouveau_cas of nouvelles_informations

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

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

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

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

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

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

Fil conducteur

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

Avec des types somme

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Types somme ouverts

Examinons le code suivant.

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

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

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

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

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

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

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

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

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

type expr = Fix of expr _expr

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

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

let rec eval (Fix expr) = _eval eval expr

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Comme promis, voici la suite, et fin, de mon billet précédent : Singeries appliquées en OCaml : Polymorphisme d’ordre supérieur (1/2). Contrairement à ce que j’avais dit, je ne parlerai pas de la restriction syntaxique sur le polymorphisme explicite : j’ai remplacé cette partie par une rapide présentation d’une publication (paper) qui est à l’origine de l’introduction de ce polymorphisme d’ordre supérieur dans le langage OCaml.

Autre utilisation du procédé

Un autre exemple pour enfoncer le clou en vous montrant encore de petits exemples de polymorphisme d’ordre supérieur. Il n’est pas tiré de Macaque, et c’est de l’orienté objet. On veut écrire une classe de « collections », qui proposent l’interface suivante :

• ajouter un objet à la collection ;

• aggréger la collection, c’est à dire calculer une valeur en prenant en compte l’ensemble des éléments : on prend en paramètre une fonction à qui on donne la liste des éléments de la collection, pour faire son calcul.

Le type de la collection dépend du type de ses éléments : on va avoir des int collection, etc. On commence donc par le code suivant :

class ['a] collection = object
  val mem = []
  method add (x : 'a) = {< mem = x :: mem >}
  method aggregate : ('a list -> 'c) -> 'c =
    fun f -> f mem
end

Mais ça ne marche pas : The method aggregate has type ('a list -> 'c) -> 'c where 'c is unbound. Le problème ici c’est que 'c n’est pas un paramètre de type spécifique à la méthode : c’est l’objet qui dans son ensemble a le type

< add : ...; aggregate : ('a list -> 'c) -> 'c >

Implicitement, le quantificateur sur le type 'c est placé au début du type de l’objet, donc c’est un paramètre global à la classe, et OCaml se plaint qu’on ne l’ait pas renseigné dans les paramètres de la classe. On pourrait effectivement dire class ['a, 'c] collection = .., mais c’est un peu idiot : on aura les collections d’entiers qui peuvent calculer des booléens, et les collections d’entiers qui peuvent calculer des flottants, et ce seraient des types différents ? La « bonne » solution, pour ne pas laisser le paramètre 'c s’échapper, est d’utiliser le polymorphisme d’ordre supérieur :

method aggregate : 'c . ('a list -> 'c) -> 'c = ...

Ainsi, on a replacé le quantificateur au bon endroit : au début du type de la méthode aggregate. Le compilateur est content et on peut utiliser aggregate, au sein d’un même objet, avec des types de retour différents.

Pourquoi dit-on « ordre supérieur » ?

On parle de « polymorphisme d’ordre supérieur » par opposition à la pratique dans le typage ML classique, qui est du « polymorphisme de premier ordre » : grosso modo, on compte l’ordre en fonction du nombre de couches de quantificateurs imbriquées. Dans les types habituels, sans quantificateurs explicites, on considère qu’ils sont tous placés au début du type, donc il n’y a qu’un seul niveau, c’est le premier ordre. type t = (∀ 'b. (∀ 'a . 'a -> 'b) -> 'b) est un type du second ordre, et (∀ 'c . (t -> 'c) -> t -> 'c) du troisième (à cause des quantificateurs implicites de t).

Avec la possibilité de mettre des quantificateurs dans les records, on peut en fait mettre autant de couches qu’on veut, donc c’est « à l’ordre qu’on veut ». On parle alors d’ordre supérieur.

Le concept d’ordre revient souvent quand on essaie de décrire la puissance expressive d’un système. Ici on parle de l’ordre du polymorphisme (des types), mais il y a aussi un concept d’ordre des fonctions : dans certains langages, les fonctions ne peuvent prendre en paramètre et renvoyer comme valeur de retour que des types de base, non fonctionnels, du langage (entiers, flottants, tableaux, structures, etc..). Ce sont des fonctions de premier ordre. Il y a aussi des langages qui peuvent prendre en paramètre des types de base, ou des fonctions du premier ordre (qui ne prennent que des types de base) : c’est le deuxième ordre. On peut imaginer un troisième, quatrième ordre, etc., mais en pratique les langages sont souvent conçus pour déclarer des fonctions d’« ordre supérieur » : les fonctions peuvent prendre en paramètre et retourner des fonctions de n’importe quel type (des fonctions de fonctions de fonctions de … de fonctions des types de base).

Évasion du parser universel et perennité de la méthode

J’ai expliqué qu’un des intérêts de demander une fonction qui dépend du parser universel, plutôt que de divulger le parser universel dans l’interface de Macaque, était de le « cacher » à l’utilisateur. En fait ce secret est purement stylistique (« c’est pas dans l’interface donc tu touches pas ») et n’augmente pas la « sécurité » (commme si l’utilisateur était un délinquant) de l’interface. En effet :

let pirate : univ_parser =
  let captured_parser = ref None in
  let fake_builder = fun prey_parser ->
    captured_parser := Some (prey_parser);
    object (* fake table object *) end
  in ignore (Sql.table (* ... *) fake_builder);
  match !captured_parser with
    | None -> failwith « failed to capture the flag! »
    | Some univ_parser -> univ_parser

Démoniaque non ? On fait semblant de vouloir construire une table, dans la fonction, au moment où il nous donne le parser, on le capture en le mettant dans une référence qu’on avait déclarée au préalable. Cette technique ne marche que si l’implémentation de Sql.table utilise vraiment la fonction pour obtenir le parser, en lui donnant vraiment le parser universel en paramètre, mais à priori c’est ce qu’elle fait (sinon elle n’aurait pas accès au parser et il faudrait tout recommencer).

Cette astuce repose sur la présence d’un effet de bord qui permet au paramètre de s’évader hors de la fonction, sans passer par la valeur de retour. Elle pose aussi problème quand on veut implémenter des fonctions du style with_open_file : (input_channel -> 'a) -> 'a. On n’aurait pas ce problème dans un langage pur, qui empêche totalement les effets de bords (ce n’est pas le cas en Haskell qui a unsafePerformIO), mais pour l’instant les restrictions que ça apportent sont énormes, ça ne vaut tout simplement pas le coup de faire ça dans le seul but de pouvoir garantir qu’aucune variable ne se sauve. On peut aussi s’en sortir avec un système de typage plus expressif (closure & effect typing), il y a des systèmes expérimentaux qui font ça (par exemple le langage Discipline lié à Haskell), mais encore une fois ils sont bien trop lourds à l’utilisation pour que leur coût soit compensé par leurs bénéfices dans la grande majorité des situations (où la sûreté est importante, mais la productivité du programmeur l’est encore plus).

Je tiens aussi à vous donner, en toute honnêteté, la nouvelle la plus triste du billet : le type univ_parser est décédé. Quelques temps après sa naissance, j’ai rajouté des fonctionnalités, ce qui a induit de nouveaux besoins, et quand j’ai refactorisé, je me suis retrouvé à devoir publier le parser universel dans l’interface, et ai donc supprimé le type spécifique. C’est triste, mais c’est la vie : quand on code il faut parfois, souvent même, supprimer des choses qu’on a faites avec, même si on les trouve tout à fait intéressantes. Du reste, une valeur de type ('a sql_type -> 'a parser) dans mon interface est toujours plus simple à comprendre pour les gens qu’un polymorphisme d’ordre supérieur, donc ce n’est pas forcément une perte pour la lisibilité de mon programme.

Une publication à se mettre sous la dent

Ce billet n’est pas une réaction, mais il me paraît tout de même pertinent de citer l’article des gens qui ont mis en place le polymorphisme d’ordre supérieur en Caml : Extending ML with Semi-Explicit Higher-Order Polymorphism (.ps.gz), par Jacques Garrigue et Didier Rémy.

Le papier est, dans sa plus grande partie, trop technique pour moi, mais si vous avez envie d’essayer, voilà l’histoire en deux mots. Les auteurs étudient des compromis entre le système de typage ML (polymorphisme de premier ordre seulement, mais inférence des types) et le Système F (polymorphisme d’ordre supérieur,^א pas d’inférence de types).

Le système F est un langage plus expressif que ML, mais aussi nettement plus lourd à utiliser (syntaxiquement). En particulier, le polymorphisme y est introduit et appliqué explicitement : quand on veut écrire un terme polymorphe, on écrit un terme qui « prend un type en paramètre », et quand on veut l’utiliser on lui « applique » le type particulier avec lequel on l’utilise. On note par exemple Λα. λx:α. x la fonction identité (on prend un type α en paramètre, puis une variable x de type α, et on renvoie x), et si t est de type τ, on écrira id τ t pour l’identité de t : on commence par donner à la fonction le type du paramètre, puis le paramètre lui-même.

Les gens^ב qui ont travaillé sur l’ajout de polymorphisme d’ordre supérieur à ML se sont en général inspirés de l’approche Système F. L’originalité de la publication de Garrigue et Rémy, c’est qu’ils demandent des annotations explicites pour l’introduction de polymorphisme d’ordre supérieur (la syntaxe 'a . foo est équivalente au Λα . foo), mais pas pour son utilisation.

Je ne parlerai presque pas de l’article, mais quand même une remarque : pour avoir un système qui ne fait pas de choses étranges, les auteurs de l’article décident de respecter le polymorphisme indiqué par les annotations des programmeurs, mais de ne pas laisser le système en ajouter lui-même; ils utilisent pour cela un système basé sur (encore une fois) le polymorphisme, qu’on peut considérer comme l’équivalent en théorie des types d’un joli hack.

Comme vous le savez peut-être, mon temps de développement cet été est principalement accaparé par Macaque, un sous-langage spécialisé dans les bases de données (DSL SQL) pour OCaml.

Le sujet n’est pas trivial : il s’agit de permettre d’écrire des requêtes SQL de façon à la fois expressive, composable et typée. Cela recèle tout un tas de problèmes qui me font m’arracher les cheveux, et surtout ça me pousse à sortir des sentiers battus où j’ai mon petit confort, et mettre en place des techniques de programmation un peu plus osées que d’habitude.

Dans ce billet je compte vous présenter une technique parmi celle que j’ai eu l’occasion de mettre en place dans Macaque : le polymorphisme d’ordre supérieur. L’idée est de profiter d’un exemple pratique pour la décrire de façon un peu moins théorique que d’habitude.

Pour profiter du contenu technique de ce billet, vous devez connaître un langage fonctionnel typé. Sinon, vous n’en retiendrez sans doute qu’un discours un peu longuet sur les types abstraits et le choix d’une interface pour des fonctions qui ne sont pas complètement innocentes, mais c’est déjà ça de pris.

Trois remarques avant de commencer. D’une part, évidemment, je ne prétends pas avoir inventé quoi que ce soit : ce sont des techniques^α bien connues des spécialistes en programmation fonctionnelle depuis un certain temps, et je n’y aurai sans doute pas pensé si je ne les avait pas déjà vues en application dans d’autres cas. Mais justement, en voir des applications peut être intéressant pour savoir éventuellement l’utiliser soi-même ensuite, donc je veux partager mon expérience.

D’autre part, ce billet n’est pas un billet de présentation de Macaque (mais je pourrais envisager d’en écrire un; est-ce que ça vous intéresserait ?) : je ne donnerai pas beaucoup de détails d’ensemble, mais juste les informations contextuelle qui permettent de comprendre chaque exemple.

Enfin, vous l’avez sans doute constaté dans ma réaction précédente, j’aime bien développer des points précis dans un second temps, en annexe. Développer… en longueur, et c’est bien le problème : on m’a fait remarquer, et à raison, que mes billets étaient trop longs. J’ai donc choisi de couper celui-ci : je me tiendrai au fil principal dans un premier temps, et je posterai plus tard un second billet pour approfondir des points secondaires. Cela me permettra aussi d’y traiter des questions qui seraient éventuellement apparues en commentaire.^β

Décrire les tables d’une base de données

Ce point ne concerne pas une question d’implémentation directement, mais plutôt une question d’interface. Je m’intéresse à une des fonctions de l’interface publique de Macaque (sql.mli), la fonction table. Cette fonction est utilisée dans la partie de Macaque qui permet de décrire des tables d’une base de données; l’utilisateur doit lui donner des informations sur les champs de la table, qui permettront derrière à Macaque d’en construire une représentation adaptée à ses besoins. Elle renvoie une valeur abstraite (l’utilisateur ne voit pas son contenu) qui représente la table, et quand l’utilisateur voudra utiliser cette table ensuite (pour effectuer des requêtes dessus par exemple), il devra donner cette valeur aux fonctions qui la demandent. De son point de vue, cette valeur de retour de la fonction table joue donc le rôle de certificat, ou témoin : « oui, j’ai bien déclaré la table machin, cette valeur en témoigne ».

Les informations que Macaque demande pour construire la table sont variées, mais celle qui nous intéresse ici est le parser : l’utilisateur doit fournir la fonction qui servira à lire les chaînes de caractères vomies par le serveur SQL quand on lui demande des lignes de cette table, pour en construire de jolies valeurs typées que Macaque pourra ensuite donner à l’utilisateur avec le sourire.

Si Macaque demande à l’utilisateur de lui fournir le parseur, c’est parce qu’il serait difficile de le construire automatiquement : ça voudrait dire utiliser les valeurs caml passées en paramètre à la fonction pour construire un parser; mais alors le type du résultat du parseur dépendrait de ces valeurs, et avoir une fonction qui renvoie un type différent selon les valeurs qu’on lui donne n’est pas possible dans le système de typage Caml, il faudrait des outils théoriques plus puissants. Il y a toujours moyen de s’arranger, mais demander à l’utilisateur de faire le travail reste la solution la plus simple.

Un parser qui renvoie un élément de type 'a est de type 'a parser, qui est un type de macaque ressemblant à string -> 'a, avec un peu plus d’informations. L’utilisateur doit donc écrire une fonction du genre :

let parse_user input =
  object
    method id = parse_id input
    method nom = parse_nom input
  end

En réalité, ce n’est pas lui qui l’écrit, mais une macro qui fait le travail à sa place, mais du point de vue de l’interface de Macaque c’est la même chose. Le problème c’est qu’il ne sait pas comment parser id et nom : les valeurs qu’il faut renvoyer ne sont pas de simples entiers et chaines de caractères, mais des valeurs d’un type interne à Macaque qui contiennent toutes les informations dont il a besoin (type, nullabilité (est-ce que la valeur peut valoir NULL), etc.). Bien sûr, la définition de ce type n’est pas accessible à l’utilisateur : sinon, il pourrait faire n’importe quoi avec, construire de fausses valeurs (qui ne respectent pas les invariants implicites de la structure) et détruire l’univers.

Ce que l’utilisateur a à sa disposition, ce sont des valeurs abstraites qui décrivent le type de ses champs. Il a une valeur de type int sql_type et une valeur de type string sql_type (abstraits, bien sûr), qui contiennent les informations de typage utiles à Macaque, et en particulier la méthode nécessaire pour parser ces valeurs.

Décrire le parser de sa table

Macaque, en interne, sait produire un parser à partir d’un élément de type 'a sql_type; la fonction qui construit ce parser spécialisé à partir de la description du type est ce que j’appelle un parser universel. Mais voilà le problème : je n’ai pas envie d’exposer ce parser universel à l’utilisateur, parce qu’il n’en a normalement pas besoin. Je pourrais la mettre dans l’interface en précisant que l’utilisateur n’a normalement pas besoin de s’en servir (seule ma macro de description de tables l’utilise), mais tant qu’à faire je préfère éviter : un peu de prudence ne peut pas faire de mal. Il ne s’agit pas de l’en empêcher à tout prix : de toute façon au final l’utilisateur peut toujours bidouiller pour faire ce qu’il veut, mais de ne pas l’y encourager.

L’idée, c’est de demander à l’utilisateur : « Bon, d’accord, tu n’as pas accès aux fonctions de parsing des composants de ta table, mais si c’était le cas, comment ferais-tu pour construire le parser de la table entière ? ». On lui demande de construire une fonction témoin avec un type du genre :

universal_parser -> table_parser

S’il produit une fonction de ce type là, on sait qu’il peut parser la table, et on peut prendre la fonction, et ensuite en interne (derrière les coulisses) lui donner un parser universel, pour récupérer le parser de table qui nous intéresse.

Le typage du parser universel coince

C’est là qu’on arrive enfin au sujet promis : le polymorphisme d’ordre supérieur. Quel est le type de la fonction témoin ? On est d’abord tenté de lui donner le type ('a sql_type -> 'a parser) -> 't parser (où 't est le type objet représentant une ligne de la table).

On aurait donc un type pour table (en oubliant les autres paramètres) :

val table : (('a sql_type -> 'a parser) -> 't parser) -> 't table

Mais ça coince vite quand on essaie d’écrire :

let parse_user univ_parser input =
  object
    method id = univ_parser int_type input
    method nom = univ_parser string_type input
  end

On suppose que l’utilisateur a déjà reçu d’autres fonctions les valeurs int_type : int sql_type et string_type : string sql_type. Quand on essaie de compiler notre code, catastrophe : il souligne la valeur string_type et nous répond : Error: This expression has type string T.sql_type but an expression was expected of type int T.sql_type.

Soucis : let-polymorphism et value restriction

Le problème vient du fait que le 'a dans le type de notre fonction doit être "le même" à chaque fois qu’on l’utilise. Si on l’utilise à chaque fois comme une fonction polymorphe, elle reste polymorphe, mais dès qu’on l’utilise sur un type particulier, OCaml infère qu’elle est de ce type là, et nous empêche de l’utiliser sur un autre.

Une autre manière de voir le problème est de considérer la variable de type 'a comme une façon de dire « le type a, quel qu’il soit » : on peut introduire explicitement des quantificateurs (comme en logique), et lire le type

(('a sql_type -> 'a parser) -> 't parser) -> 't table

Comme la formule :

∀ a, ∀ t, ((a sql_type -> a parser) -> t parser) -> t table

Comme le type dont on est parti ne contient aucune information sur la position des quantificateurs, on l’a mis à l’endroit le plus naturel : au début de la fonction. Le problème vient justement de cette position : cela correspond à dire que pour chaque application de la fonction, on fixe 'a et 't au départ : on peut en choisir un différent à chaque mais à l’intérieur du type ils sont fixés, et en particulier la fonction ('a sql_type -> 'a parser) ne peut être appelée plusieurs fois avec un 'a différent.

Polymorphisme d’ordre supérieur en OCaml

On voudrait en fait le type suivant :

∀ t, ((∀ a, (a sql_type -> a parser)) -> t parser) -> t table

J’ai déplacé le quantificateur à l’intérieur de la fonction : à chaque application de la sous-fonction, on peut avoir un nouveau type 'a.

Comment faire comprendre ça à OCaml ? Il faut un moyen de rajouter des informations sur la position des quantificateurs. C’est possible en OCaml, mais seulement^γ pour déclarer deux types de valeurs : les enregistrements et les objets.

On déclare donc le type de notre parser universel, dans un enregistrement :

type univ_parser = { of_type : 'a . 'a sql_type -> 'a parser }

Notez la différence de taille par rapport au type classique

type 'a univ_parser = { of_type : 'a sql_type -> 'a parser }

Le type ne prend pas de paramètre. En effet j’ai placé le quantificateur à l’intérieur (la syntaxe 'a . avant le type), donc le type ne "dépend plus" de 'a, il n’est pas fixé au niveau du type mais à l’intérieur, dans le champ of_type.

Je peux ensuite coder ma fonction, heureux :

let parse_user (parser : univ_parser) input =
  object
    method id = parser.of_type int_type input
    method nom = parser.of_type string_type input
  end

Le type est maintenant :

val table : .. -> (univ_parser -> 't parser) -> 't table

Le quantificateur sur 'a est placé à l’intérieur du type univ_parser, et plus au début de la fonction. Happy end !

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 :

1. 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 ;

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

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.

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 :

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

2. (* -> *), 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 :

1. diverger dans tous les cas : c’est la fonction [bot] : f -> ⊥,
   par exemple let rec bot f : unit = bot f ;

2. renvoyer () dans tous les cas : c’est la fonction [top] : f -> *,
   par exemple let top _ = () ;

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

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 :

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

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.

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.

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.

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.

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 !

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

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.

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

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