Ours & Hippy — le blog [polymorphisme]

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 !