Singeries appliquées en OCaml : Polymorphisme d'ordre supérieur (1/2)

(Gabriel Scherer (gasche) @ 2009-09-07 20:13:40)

Aujourd’hui, rz0 est occupé, donc il ne peut pas faire son édito habituel. Mais comme on aime ça, il m’a demandé de faire son édito à sa place. Voici donc un pastiche de rz0-édito bluestorm-longuet :

Un billet fonctionnel de bluestorm comme on les aime : son langage l’oblige à faire des trucs oufzor-théoriques pour obtenir des abstractions simples que les gurus connaissaient déjà avant sa naissance, et il se sent obligé d’en parler comme la révolution. Vous l’aurez compris, ce billet est dédié à la "fumette" (iykwim), et là, c’est de la bonne, c’est du typage. Carnage ou garbage ?

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

α : Je mets un pluriel ici parce que j’espère secrètement écrire un ou deux autres billets de ce genre.

β : Oui, j’espère toujours avoir des commentaires, je suis quelqu’un de naturellement optimiste.

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.

γ : cette restriction paraît sans doute étrange et injustifiée, j’en parlerai dans mon prochain billet. Bavez !

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 !