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

(Gabriel Scherer (gasche) @ 2009-09-09 06:58:17)

Après le boudin, les restes. bluestorm nous offre ici une collection de petits détails alléchants pour certains, sans goût ni odeur pour d’autres, mais qui viendront en tout cas accompagner, étendre et embellir sa précédente composition (à laquelle ma présence a semble-t-il cruellement manqué), en mettant l’accent sur des aspects divers, et divers aspects : bref, à parler pour ne rien dire, j’y perds mon inspiration, moi…

–minh

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 :

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 concept d’ordre revient à la charge : je parle du Système F2, qui propose le polymorphisme d’ordre supérieur, mais donc les kinds (un niveau supplémentaire de typage) sont d’ordre 2. Il existe aussi un système F d’ordre supérieur, Fω.

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.

ב : Parmis ces joyeux lurons se trouve Odersky, qui travaillait sur ces choses-là dans les années 90, et qui est maintenant connu comme le principal auteur du langage Scala.

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.