Ours & Hippy — le blog [typage]

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 !

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.

À 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 rz0 l’a admirablement fait remarquer, le blog est plutôt mort ces temps-ci. Sans surprises, je suis occupé depuis le début de l’année, et le temps pour poster des billets en a diminué d’autant. Je me suis fixé l’objectif de ne pas passer plus d’une heure à écrire ce billet (écriture seulement, il y aura sans doute de la relecture ensuite), et ça me paraît un pari assez raisonnable, bien que nettement plus ambitieux que les billets précédents. La qualité en souffrira certainement, mais j’essaie de trouver un équilibre.

Je remarque d’ailleurs que je ne suis pas le seul à être occupé : tous ces gens qui avaient promis juré que oui, ils feraient des efforts pour poster des commentaires de temps en temps, histoire qu’on conserve la motivation, ils ont visiblement un travail fou. Tant pis ; de toute façon je n’ai pas les moyens (temps, motivation et envie) d’écrire de gros billets bien préparés en ce moment. Si j’écris celui-ci, c’est parce que j’ai honte de laisser cet espace tellement vide alors que rz0 a fait tant d’effort pour m’installer un petit coin bien douillet. Et j’espère aussi que ce que j’ai à vous raconter pourrait vous intéresser.

Débuts en Coq

Cette année, j’ai décidé de me lancer dans le vaste monde des assistants de preuve. En un mot, ce sont des programmes qui permettent d’écrire des preuves mathématiques, et qui les valident : ils savent dire si oui ou non, une preuve est correcte.

Je leur vois deux intérêts principaux. D’une part, ils permettent de se redonner confiance en mathématiques ; si vous connaissez le malaise de celui qui écrit un brouillon de preuve, mais sans savoir vraiment si elle est juste ou contient une erreur désagréable que vous n’aviez pas vue, vous comprendrez ce que je veux dire. Plus généralement, c’est un peu comme la différence, en informatique, entre écrire du pseudo-code, et écrire dans un vrai langage de programmation : l’avantage d’un vrai langage, c’est que vous pouvez exécuter le programme pour vérifier qu’il fonctionne (et en particulier vérifier sa syntaxe, etc. automatiquement), alors qu’on est rarement motivé pour relire avec soin un pseudo-code. L’ordinateur apporte un retour d’expérience (feedback) direct, impartial et incontestable.

D’autre part, les assistants de preuve sont essentiellement des langages de programmation. Ils se placent en effet à cheval entre la théorie des types (côté informatique) et la théorie de la démonstration (côté mathématiques) : c’est essentiellement le même domaine, vu de points de vue différents. On parle souvent de l’isomorphisme de Curry-Howard, mais ce théorème précis concerne des systèmes bien précis, et l’étendue de la correspondance est en fait beaucoup plus large ; fondamentalement, depuis le début du 20e siècle, on pense les preuves formelles comme des programmes (fonctionnels). Ces outils font donc de bons mélanges entre des preuves très formelles et des langages très fortement typés, et ça a tout pour me plaire. On peut d’ailleurs aussi utiliser ces systèmes pour prouver des choses sur les langages de programmation (tous paradigmes confondus, cette fois-ci).

Il existe plusieurs systèmes d’assistants à la démonstration. Les plus utilisés actuellement sont Coq et Isabelle (et éventuellement Twelf et HOL-Light, avec aussi des anciens couverts de lauriers (Mizar), et de jeunes qui explorent l’espace de recherche (Agda)). Ces systèmes ont des qualités et des défauts variés. J’utilise Coq. D’une part parce que c’est le système conçu en France, et donc je suis entouré de gens qui l’utilisent, l’enseignent, voire le développent.^α D’autre part, j’utilise pour apprendre les bases le livre en ligne Certified Programming with Dependent Types, qui conseille d’utiliser Coq et qui a certainement ses raisons, moi, je ne connais pas assez le domaine pour faire un choix informé.

Ces outils sont majoritairement codés dans un des langages dont le nom contient « ML » et ne commence pas par « X ». C’est une corrélation historique, puisque le langage ML (notre grand-père à tous) a été créé conjointement à l’assistant de preuve LCF.

Au passage, si vous envisagez vous-même de vous intéresser un jour au sujet, je suis assez content de ce bouquin. En particulier, il prend surtout ses exemples dans le monde des langages de programmation : dès le premier chapitre, on compile des expressions arithmétiques simples vers une machine à pile simple, en rajoutant du typage à gogo, et sera donc plus accessible qu’un livre orienté vers la logique formelle si vous vous sentez plutôt informaticien. Une connaissance (au moins des bases) de la programmation fonctionnelle est tout de même indispensable.

Il est temps de signaler les deux articles qu’asmanur a écrit comme une petite introduction à Coq (un passe-temps qu’il a certainement abandonné assez vite, comme tous les autres) : Voyage au bout de la logique, et sa deuxième partie. Si vous vous intéressez à la discussion sur le choix de l’assistant à la démonstration, vous pouvez aussi lire l’introduction du livre de Chiplala. Au passage, le mode Emacs qu’il recommande, Proof General, est vraiment très bien.

Programmation par contraintes

Cette fois-ci, cela tient plus de l’anecdote, mais je trouve ça assez amusant pour avoir envie de vous en parler. En plus de la logique formelle fonctionnelle typée et des hautes sphères éthérées de la théorie des catégories, je fais cette année des choses bassement matérielles qui demandent de la programmation. Évidemment, je fais tout en OCaml.

Depuis cet été, je suis assez séduit par les types fantômes. C’est un outil vraiment puissant et agréable, à tel point que je suis tenté d’en mettre un peu partout dans mes divers projets. Par exemple, je dois coder un projet de bataille navale en réseau (et d’ailleurs c’est assez ennuyeux ; je prends sur mon temps de développement pour vous écrire cet article). Ça a l’air assez trivial, mais j’ai perdu tellement de temps à refactoriser dans tous les sens pour avoir le typage le plus expressif possible que j’en suis venu à m’auto-imposer la règle suivante : « Interdiction d’utiliser les types fantômes ! »

Et vous, avez-vous des règles personnelles que vous appliquez avec cruauté, pour éviter de perdre votre temps dans des considérations, certes intéressantes, mais déraisonnables pour le projet précis sur lequel vous travaillez ?

J’en profite pour vous signaler que j’étais passé à côté jusqu’à présent, mais j’ai découvert récemment que la bibliothèque standard OCaml utilise elle aussi, des types fantômes, ma bonne dame : ça se passe dans le module le plus haut niveau de la bibliothèque, Bigarray.

Traitement d’images

Je suis, par un curieux hasard de circonstances, un cours de traitement d’images. C’est un sujet très éloigné de mes centres d’intérêt habituels, mais je ne le regrette pas. Je vois défiler beaucoup de jolies photos, et de méthodes pour les améliorer encore, parfois franchement inventives. J’ai un professeur formidable, qui est un mordu de la photographie, mais aussi un amateur de l’analyse de Fourier. Sans entrer dans les détails pénibles, il nous fait des démonstrations « avec les mains » qui sont parfois assez sympathiques, et donnent un petit coup de jeune à toutes ces choses qui sombrent lentement dans l’oubli quand on ne les utilise pas.

Au cas où ça vous intéresse, voici un exemple d’algorithme que nous avons étudié : Colorization Using Optimization. Il s’agit de donner des couleurs à des images en noir et blanc, à partir de quelques indications de l’utilisateur (des traits de couleur connue). L’idée de base, c’est de supposer que deux pixels de luminosité proche doivent être de couleur proche. On peut alors exprimer la teinte de chaque pixel en fonction de celle de ses voisins et, combiné aux conditions initiales de l’utilisateur, ça donne un gros système linéaire (une grosse matrice) qu’on fournit à une fonction de résolution et pouf, une image en couleur. Ça marche étonnamment bien.

Pour ce cours, j’ai participé à l’écriture de bindings OCaml vers des bibliothèques C (ou interfacées par l’intermédiaire du C), par exemple OpenCV ou SuiteSparse. C’est très drôle, on retrouve la joie du segfault (et c’est encore mieux à plusieurs). Je ne m’étais jamais vraiment plongé dans l’interface C-OCaml, et je peux vous dire que ce n’est pas inoubliable mais ça reste une expérience amusante. Cela m’a d’ailleurs permis de mettre mon petit grain de sel dans un tutoriel de Cacophrène à ce sujet sur le SdZ. Ça fait toujours une introduction en français à ce sujet, qui peut servir de mise en bouche, mais si un jour vous voulez vraiment coder quelque chose je vous conseille ensuite de lire conjointement le manuel officiel pour les idées, et le tutorial en anglais de François Monnier pour les exemples de code. Attention au DA-Ocaml, sur ce point il est un peu vieux.

Une petite réaction pour finir ?

Que serait mon billet mensuel sans une référence, ou du moins une allusion, à un petit papier à se mettre sous la dent ? J’en ai survolé une bonne poignée depuis la rentrée, mais les derniers que j’ai croisés sont des articles de Gilad Bracha. C’est un type qui a commencé ses exploits en codant un système Smalltalk avec annotations optionnelles de typage très performant^γ, pour aller ensuite réutiliser ses compétences en travaillant sur Java, sa spécification et sa VM chez Sun pendant quelques temps, avant de repartir construire un nouveau langage dynamique, Newspeak.

J’ai jeté un coup d’oeil à la bête. Comme vous imaginez, les langages très dynamiques ne sont pas forcément ceux qui me tentent le plus, mais ça fait du bien de voir ce qui se fait ailleurs de temps en temps. J’ai aussi lu deux de ses papiers au hasard : Executable Grammars in Newspeak, et Pluggable Type Systems.

Le premier papier présente une façon possible de créer une bibliothèque de parsing combinators dans un langage dynamique. Comme l’annonce l’auteur d’entrée de jeu, c’est plutôt le point fort des langages fonctionnels (l’étalon dans le domaine étant le très bon Parsec de Haskell). Il promet que les fonctionnalités nouvelles de son langage, ainsi que son fort dynamisme, permettront d’en faire une traduction « objet dynamique » adaptée. Je n’ai pas été émerveillé par le résultat (en particulier, comme toutes les approches « DSL internes au langage », la syntaxe n’est au final pas si géniale que ça), mais ça reste une lecture intéressante. Il discute aussi de la facilité ou non à typer ces opérations dans un langage statique, mais le référentiel semblant être celui de Java, on en apprend plus sur l’état des systèmes de types mainstream que sur le fond du problème.

Le deuxième article n’est pas vraiment un article scientifique, mais plutôt une prise de position de l’auteur. Il voudrait qu’on envisage les systèmes de type non pas comme une donnée fondamentale du langage de programmation, à laquelle tout programme dans ce langage doit se soumettre, mais comme une étape supplémentaire, optionnelle. C’est une idée très séduisante, mais assez délicate à mettre en place en pratique (la plupart des avantages théoriques des systèmes de types actuels venant justement de leur capacité à (presque) tout contrôler).

Il voudrait aussi que l’inférence soit optionnelle/désactivable, en un mot « pluggable », ce qui est un point de vue intéressant (et trouve des échos chez les théoriciens^δ). Il voudrait même pouvoir faire cohabiter plusieurs systèmes d’inférence pour « choisir le meilleur selon les situations », et là je ne suis franchement pas convaincu : ça mène à une situation où le type repose sur beaucoup d’heuristiques diverses que le programmeur ne maîtrise pas en général, et cela pourrait à mon avis poser plus de problèmes que ça n’en résoud. Ça reste une lecture intéressante, c’est agréable de voir que les universitaires grisonnants ne sont pas les seuls à se poser la question.

Pour amadouer mes lecteurs potentiels les plus revêches, je dois signaler que cet article cite explicitement les essais d’ajout (partiel) d’un typage statique au langage Erlang.

P.S. : Mon pari de temps n’a pas été tenu, j’ai plutôt mis une heure et demie, mais c’est toujours agréable d’écrire. Ma bataille navale avance assez bien : les clients peuvent se connecter, lancer des parties et placer leurs bateaux, et je vais bientôt être obligé de coder la partie où ils tirent les uns sur les autres. Heureusement, j’ai glissé des variantes polymorphes pour que le type des fonctions reflète le protocole de communication.

Il est arrivé une bonne chose à mon dernier billet : des gens m’y ont répondu en commentaire. Je les remercie tous chaudement. Ce n’est pas complètement rationnel, mais je trouve ça vraiment appréciable, et ça m’a motivé pour retenter l’expérience de ces billets « en bref ». Mais pas pour cette fois : c’est intéressant quand on a différentes choses à dire, et il vaut mieux que ce ne soit pas trop souvent, sinon ils deviennent de plus en plus vides et répétitifs.

Dans les commentaires, que j’ai lus avec intérêt (j’ai même répondu à certains, c’est fou les blogs), se trouve une question qui m’a donné envie d’en faire un billet à part entière. C’est le commentaire de robocop :

Il y a quelque chose qui ressort quand même pas mal dans nombre de tes articles, c’est l’importance que tu attaches aux types. J’ai la facheuse impression d’être passé à coté de quelque chose de fondamental, pour moi, les types ce n’est qu’une vérification supplémentaire qui est fait à la compilation et ou à l’interpretation, mais à la façon dont tu en parles, le système de type semble le cœur même d’un langage de programmation.

Si comme je le pressens, je loupe vraiment quelque chose, pourrais-tu disserter rapidement là-dessus ?

En une phrase : pourquoi, parmi toutes les caractéristiques d’un langage de programmation, attacher autant d’importance à son système de typage ?

J’ai été surpris de ne pas pouvoir répondre à cette question sur le moment. J’ai pris du temps pour y réfléchir, et je pense avoir maintenant une réponse satisfaisante (mais pas rapide).

J’ai apprécié les commentaires de la carotte qui, avant l’ours, a relu ce texte et m’a permis de l’améliorer.

Rappels

Je ne compte pas expliquer dans ce billet les divers avantages et inconvénients, existants ou fantasmés, des différents systèmes de typage ; ce n’est pas le sujet. Je me contenterai ici d’un bref rappel de deux notions qui reviennent souvent quand on discute les systèmes de typage, et dont je reparlerai par la suite :

typage statique

désigne les systèmes de typage qui vérifient les types dans un programme avant de l’exécuter, typiquement au moment de la compilation. Les erreurs de typage, s’il y en a, sont signalées pendant cette phase et le programme n’est pas exécuté tant qu’il n’est pas correctement type. En général, à l’exécution, on n’a plus à se soucier des types et on peut raisonner comme s’ils n’existaient plus.

typage dynamique

désigne les systèmes de typage qui vérifient les types pendant l’exécution du programme. Avant chaque opération que le programme doit exécuter, il vérifie que les types des données sont correctes ; cela implique que le programme a accès à ces types quelque part : ils sont stockés dans la mémoire du programme pendant son exécution.

Ce sont deux méthodes très différentes qui ont un but commun : empêcher l’ordinateur d’effectuer des opérations mal typées (« mélanger des patates et des carottes »). Chaque façon de faire a ses adeptes, et les deux camps se livrent des guerres terribles, depuis plusieurs générations de langages de programmation — et, bientôt, d’informaticiens. Le point important ici est que les langages mettant en place l’une ou l’autre de ces méthodes ont un système de typage. Il sera plus ou moins bien défini, selon la précision de la définition du langage lui-même, mais dans tous les cas on peut s’y intéresser.

J’ai déjà parlé du typage dans un article publié sur le SdZ : Le typage, présentation thématique et historique. Je n’en suis pas complètement satisfait : je le trouve trop jeune et un peu naïf, et j’essaierai peut-être de le reprendre quand je saurai mieux ce que je veux dire.
Pour les débats autour du choix d’un système, j’aime bien l’article What To Know Before Debating Type Systems. Il est peut-être un peu biaisé en faveur des systèmes statiques, et un peu trop technique, mais il apporte une vue d’ensemble assez intéressante. C’est une bonne base si vous voulez vous lancer dans le débat : statique ou dynamique ?

Cependant, ce que je voudrais discuter ici, ce n’est pas le choix de telle ou telle méthode de typage, mais plutôt la place du typage au sein d’un langage de programmation, relativement aux autres aspects du langage.

Types comme information

Imaginez que vous voulez écrire un petit morceau de programme dans le langage de votre choix, qui soit réutilisable par d’autres programmeurs. Vous devez leur décrire ce que vous avez fait. Vous commencez par leur dire ce que fait ce bout de programme (« c’est une compression selon le codage de Huffman »), et vous allez décrire la manière dont ils doivent interagir avec ce bout de programme pour profiter de ses bienfaits : « on lui donne un texte, et il le renvoie compressé, avec le dictionnaire de compression ». Avec cette simple phrase, vous avez déjà transmis des informations de typage : on lui fournit un texte, donc en général une chaîne de caractère. S’il a besoin de plus d’informations (par exemple sur la nature du dictionnaire de compression), vous donnerez une description plus précise qui contiendra autant d’informations de typage supplémentaires.

Cette façon de procéder est commune à l’ensemble des programmes et langages. Choisissez un langage que vous appréciez et qui a une documentation utilisable : elle contient (plus ou moins explicitement) des informations de typage. Par exemple, j’ai choisi une page au hasard de la documentation du langage PLT Scheme, réputé « non typé », dans laquelle on peut trouver le texte (code ?) suivant :

(directory-exists? path) → boolean?
  path : path-string?

C’est tout à fait du typage : on décrit une fonction qui vérifie qu’un répertoire existe dans un système de fichier. Cette fonction accepte un chemin de type path-string, et renvoie un boolean. Les points d’interrogation soulignent un détail intéressant : les noms choisis pour décrire les types sont aussi des fonctions (prédicats) que l’on peut utiliser pour vérifier qu’une valeur est bien du type donné. Par exemple la documentation de la fonction path-string? contient :

(path-string? v) → boolean?
  v : any/c

Ces prédicats sont utilisés au sein de ces fonctions pour vérifier que l’utilisateur ne donne pas n’importe quoi, et la vérification de validité est donc effectuée à l’exécution : c’est une forme de typage dynamique.

Ce ne sont pas les seules explications concernant ces fonctions, il y a aussi du texte en langue naturelle qui explique leur usage. Certaines documentations ne mettent aucune information de typage aussi claire (je pense à Python par exemple), il faut aller la pêcher dans le texte explicatif, ou encore elle peut être implicitement contenue dans les noms des paramètres, qui respectent des conventions facilitant cette tâche.

L’idée importante c’est qu’au fond, un type c’est essentiellement une information sur une expression du langage de programmation.

Le langage qui parle de lui-même

Cette idée des types comme informations est très large, car elle doit faire cohabiter les notions de typage très différentes selon les langages. Elle est peut-être même un peu trop étendue, puisqu’elle désigne tout et n’importe quoi, et que je ne vais pas avoir de mal à vous convaincre que vous avez besoin d’informations pour coder correctement. On peut affiner un peu plus.

Quand on parle du système de typage d’un langage, on n’a pas en tête les conventions de nommage des paramètres utilisées dans sa documentation. On parle en général d’une manière de décrire ces informations qui fait partie du langage lui-même : le système de typage, c’est la partie du langage qui permet de donner des informations sur les valeurs.^α Je désigne cette partie par le terme langage de types : par exemple le langage des types du C est un sous-ensemble du langage C qui contient les types de base (int, float..), des modulateurs (unsigned), enum, struct, …, des pointeurs, tableaux, et même des types fonctionnels.

En d’autres termes, le système de typage, c’est un méta-langage, qui détient le pouvoir d’expression du langage sur lui-même. Plus le système de typage est expressif, plus on peut dire de choses sur un programme au sein de ce programme, plutôt que dans la documentation ou en commentaire.

Vous comprenez sans doute pourquoi, avec ce point de vue, j’attache tellement d’importance, quand je m’intéresse à un langage de programmation, à son système de typage : c’est une partie toute fondamentale puisqu’elle détermine la capacité des programmes dans ce langage, en plus de faire quelque chose d’utile, à transmettre des informations sur ce qu’il fait.

Il faut cependant bien remarquer que, bien que très importante, elle n’est pas non plus indispensable : on peut très bien imaginer des langages qui ne permettent de formuler aucune information sur les programmes, mais qui ont d’autres qualités qui en font des langages intéressants. Je pense par exemple à Forth, un des premiers langages à pile haut niveau.

Système de typage et vérification

La définition actuelle reste assez molle : est-ce que les prédicats de PLT Scheme constituent un système de typage ? Ils font partie du langage, mais leur utilisation est laissée au bon vouloir de l’utilisateur : il peut aussi implémenter sa fonction sans faire aucune vérification. On pense en général plutôt à des systèmes dans lesquels le typage est obligatoire, et vérifié automatiquement^γ par le compilateur. Ce qui est sûr c’est que les informations implicites de la documentation Python ne rentrent pas dans ce cadre : le typage en Python, c’est ce que le compilateur sait vérifier de lui-même et afficher dans un message d’erreur : l’appartenance à une classe, l’existence d’une méthode donnée, etc.

Quand on décrit le système de typage d’un langage, il faut donc aussi préciser la manière dont ces informations sont vérifiées, ou plus généralement exploitées par le reste du langage. Il y a d’autres distinctions que la vérification statique ou dynamique que j’ai évoquée. Par exemple, certains langages permettent des conversions implicite d’un type vers un autre, ou le choix dans une fonction d’un comportement différent selon le type des paramètres ; on parle dans ce dernier cas de polymorphisme ad-hoc, car il permet de gérer chaque cas particulier séparément.

Autres points à considérer pour son système de typage

L’expressivité et les conditions de vérification ne sont pas les seuls points à débattre d’un système de typage.

On peut s’intéresser à l’emplacement, au sein des programmes de ce langage, des annotations de typage. Certains langages demandent au programmeur très peu d’indications de typage, car ils peuvent les reconstruire à partir des informations déjà présentes dans le langage : c’est l’inférence de type. Plus le langage des types est expressif, plus cette reconstruction est difficile. Les annotations peuvent encombrer le programme si elles sont trop nombreuses, mais placées judicieusement elles peuvent augmenter la lisibilité. Plus généralement, les informations de typage, qu’elles soient produites par le programmeur ou ses outils, renforcent la documentation et la modularité entre les différentes partie du programme : donner le type des valeurs d’une bibliothèque logicielle facilite beaucoup son utilisation par d’autres programmeurs, surtout quand il est assez expressif pour traduire l’ensemble des contraintes d’utilisation de cette interface.

Un dernier exemple, plus sophistiqué, la propriété de séparation : dans certains langages (dont OCaml), le typage est une phase totalement séparée de l’évaluation, dans le sens où une fois qu’on a un programme bien typé, on peut oublier complètement tout ce qui concerne le typage, et cela ne change absolument rien au déroulement du programme.^δ Dans d’autres langages, en particulier ceux qui possèdent le polymorphisme ad-hoc, il n’y a pas cette séparation. L’avantage de cette propriété est qu’elle donne un langage plus simple à comprendre, avec des phases plus indépendantes. L’inconvénient est qu’elle est contradictoire avec certaines fonctionnalités que les concepteurs du langage peuvent avoir envie de fournir : imposer la séparation peut réduire l’expressivité. Il n’y a pas de bon et de mauvais choix dans l’absolu, cela dépend des besoins du langage, mais c’est un choix auquel les systèmes de typage sont confrontés. On peut enfin imaginer des distinctions plus fines, avec une partie du langage qui brise la séparation, mais qui est traduit dans une première phase vers un langage plus simple, bien séparé. C’est comme cela par exemple qu’on manipule les type classes de Haskell quand on veut en donner des définitions très précises (formelles).

Contraintes et limitations

Si le langage des types est peu expressif, et la vérification très rigoureuse (impossible de définir des termes non typés), le typage peut vite devenir une contrainte. Par exemple, le langage des types du C ne permet pas d’exprimer le polymorphisme paramétrique (une fonction qui marche sur tous les types ayant structure donnée) ; on fait avec, en utilisant une sorte de type-à-tout-faire, void *, qui permet d’abandonner à la fois l’information de typage et la restriction qui y est associée.

Cette limitation que l’on rencontre n’est pas seulement un artefact de systèmes pratiques, mais se trouve déjà dans la théorie des langages. Par exemple, le lambda-calcul simplement typé de base ne permet pas d’écrire des programmes qui ne terminent pas : tous les programmes bien typés terminent en un temps fini. Ça a ses avantages, mais aussi un inconvénient : ce langage n’est pas Turing-complet. En gros, il y a des fonctions qu’on ne peut pas écrire avec. On peut lever cette limitation,^ε soit en enrichissant le langage des types (polymorphisme plus types récursifs par exemple), soit en ajoutant des constructions au reste du langage (opérateur de point fixe ou définitions de fonctions récursives).

Les langages au typage dynamique ont en général un langage de type assez faible, mais ont du coup l’avantage de ne poser que très peu de contraintes : comme ils ne vérifient pas grand chose au niveau du typage (par exemple, ils ne vérifient pas le fait que les deux branches d’une condition renvoient le même type), ils ne posent pas non plus de contraintes gênantes. C’est un autre choix qui peut se justifier ; par exemple, certains motifs de conception de la programmation objet sont notoirement difficiles^ζ à typer correctement (ils demandent un langage très expressif), les langages dynamiques n’ont pas ce problème.

Pour bien typer, il faut bien comprendre

Il arrive donc assez souvent que des idées sur de nouvelles façon de programmer soient développées dans un cadre non typé, et qu’elles trouvent seulement ensuite leur place dans un système de typage, comme par exemple le transfert du langage de programmation Oz, langage dynamique qui a popularisé certains paradigmes de concurrence, à AliceML, langage typé qui reprend une partie de ces fonctionnalités.

Cela ne veut pas dire que le cadre non typé est plus fructueux : exprimer précisément une information statique sur ces nouvelles idées permet souvent de les éclairer d’un jour nouveau. Par exemple, la recherche de sémantiques statiques pour les langages à effets de bords a donné lieu à l’idée de monade, qui est utilisée en Haskell pour représenter, entre aures, les effets de bords, et qui a pour conséquence de modifier le type des programmes en y rendant ces effets explicites. On y a gagné des outils intéressant, un point de vue nouveau, et une meilleure compréhension^η de la programmation impérative.

Malheureusement, la programmation est un sujet compliqué dont nous n’avons fait qu’égratigner la surface : il y a beaucoup de choses qu’on ne sait pas encore expliquer de manière simple et précise à la fois, par exemple la concurrence, les manipulations mémoire, la communication avec les programmes extérieurs, etc. L’explication et le typage précis de manières avancées de programmer est un sujet de recherche actif, dont on espère qu’il nous apportera des réponses ; en attendant, il faut se contenter de typages correspondant à l’état des connaissances aujourd’hui, et qui ne sont pas forcément aussi expressifs qu’on le voudrait.

Puissance du typage et complexité du langage

Cette difficulté que rencontrent les concepteurs de langage de programmation se retrouve aussi, à plus petite échelle, quand un programmeur essaie de donner un type statique à son programme. Quand on code dans un langage dynamique, on ne se soucie essentiellement que d’une chose : il faut qu’au moment de l’exécution, notre programme marche. Donner un type très expressif à un programme, cela peut demander de rendre explicites plus d’informations : qu’est-ce que notre programme fait, comment le fait-il, pourquoi cette fonction est-elle correcte ? L’ordinateur peut en deviner une partie (c’est le principe de l’inférence des types), le programmeur en connaît une partie (par exemple ce qui est un entier, et ce qui est un booléen dans son programme), mais il y a parfois des programmes compliqués pour lesquels ce n’est pas aussi simple : donner un type très précis impose une bonne compréhension du programme.

Bien entendu, même dans les langages typés, un programmeur a toujours la possibilité d’utiliser des représentations moins expressives, et qui demandent donc moins de réflexion. Par exemple, au lieu d’avoir un type de donnée spécialisé pour décrire les dates (jours, mois, heure, etc.), on peut par exemple utiliser des chaînes de caractères. C’est généralement une mauvaise idée : un effort au départ pour décrire et utiliser un type plus précis permet ensuite des manipulations plus sûres et plus directes.

Il y a cependant un point à ne pas oublier quand on cherche des langages de types expressifs : ils rendent nécessairement les langages plus complexes. Quand des débutants en Ada doivent comprendre les différences entre les paramètres in, out, et in out, ils peuvent penser qu’un langage faisant moins de fioritures aurait été plus simple. On peut se demander s’il vaut mieux concevoir des langages simplifiés pour les débutants et des langages moins simples mais ayant d’autres qualités pour les experts, ou si une taille unique peut convenir à tout le monde. Cette question intéressante est encore ouverte, mais il est clair que la simplicité (réelle ou perçue) d’un langage joue dans son adoption par les programmeurs, et qu’on ne peut pas se permettre de concevoir des systèmes de typage arbitrairement compliqués en espérant qu’ils vont dominer le monde.

Tous les langages sont typés, parfois sans le savoir

Ma définition est suffisamment large pour qu’on puisse trouver un système de typage à tous les langages, même ceux qui se proclament traditionnellement « non typés ». Les cas les plus extrêmes sont les langages dont les types sont tellement pauvres qu’ils ne peuvent essentiellement rien dire d’intéressant. Par exemple, en Brainfuck, le système de typage est vide : on ne peut rien dire sur les programmes, et d’ailleurs il n’y a rien à dire puisqu’ils ne manipulent jamais rien d’autre qu’une bande mémoire dont une case est pointée.

Plus utiles, les assembleurs sont aussi des langages avec des typages très pauvres : il y a en général des registres, des valeurs immédiates et des adresses mémoires (et par exemple des labels à plus haut niveau), et des considérations de taille, alignement, etc., qui sont assez riches mais ne nous apprennent pas beaucoup sur le comportement à plus haut niveau du code, tant qu’on ne le munit pas d’un système de typage plus expressif.^θ On peut encore citer le langage de Matlab/Octave, qui ne connaît essentiellement que les matrices de scalaires, ce qui peut parfois donner de très mauvaises surprises.

Mélanger typage statique et typage dynamique ?

Cette idée de décrire les langages peu typés comme possédant un petit nombre de « types poubelles » ne donnant que très peu d’information peut en fait être utilisée pour mélanger au sein d’un langage le typage statique et le typage dynamique : on peut rajouter ces types poubelles à l’éventail des types du langage.

Il s’agit de permettre de « perdre » localement l’information de typage, en transformant toutes les valeurs, quelle que soit leur type, vers un même type dynamic. On peut ensuite utiliser une fonction d’extraction pour récupérer des valeurs bien typées dans les parties du programme qui n’ont pas besoin de typage dynamique. Cette idée est vieille comme le monde, il s’agit de faire un cast (conversion d’un type vers un autre) au détriment de la sûreté du typage, et elle est présente dans un grand nombre de langages de programmation.

Pour que cette méthode ne nuise pas trop à la sûreté de l’application dans son ensemble, il faut réutiliser les méthodes de vérification de typage des langages dynamiques : quand on envoie la valeur vers le type poubelle, on lui associe une autre valeur runtime^ι qui décrit son type. Ensuite, quand on convertit à nouveau la valeur dynamique vers un type plus expressif du langage, on peut insérer un test pendant l’exécution qui vérifie que le type d’arrivée est bien compatible avec le type dynamique stocké avec la valeur.

Au-delà du dynamic_cast de C++, les langages fortement typés ont fait des tentatives dans cette direction. La solution la plus simple est de demander à l’utilisateur de ces fonctions d’insertion et extraction dans le type dynamique de manipuler lui-même les types dynamiques, en utilisant une bibliothèque logicielle dédiée. On peut utiliser des fonctionnalités du langage pour simplifier cette manipulation (par exemple des macros syntaxiques, des types fantômes,^κ ou des type classes), et mettre en place des bibliothèques logicielles apportant ces facilités aux programmeurs.

Ça n’est cependant pas suffisant : si l’on se contente d’une bibliothèque logicielle à part, le langage ne garantit pas la cohérence entre l’information statique de typage dont il dispose, et les valeurs dynamiques construites par l’utilisateur ou sa bibliothèque spécialisée : même quand elle est fortement typée (les manipulations à l’extérieur de la bibliothèque sont sûres) il faut faire confiance à l’auteur de cette bibliothèque de valeurs dynamique pour n’avoir pas fait d’erreurs de conversion à l’intérieur.

Si l’on veut plus de simplicité et de sûreté, il faut intégrer cette fonctionnalité directement au sein du langage de programmation. La communauté CAML a fait partie des pionniers de ce domaine avec Dynamics in ML, une extension du langage proposant des valeurs dynamique même pour les types polymorphes. Les langages fonctionnels Clean et AliceML proposent aussi cette fonctionnalité.

Ces méthodes permet de concevoir des langages typés statiquement mais qui acceptent de « laisser la main » gracieusement quand on atteint les limites de leur expressivité. Cela permet de résoudre les problèmes des constructions trop difficiles à typer mentionnés auparavant, sans abandonner trop de typage. Malheureusement, en pratique la mise en place de tels systèmes au sein d’un langage peut compliquer sensiblement son implémentation efficace, et elles ne sont donc pas très répandues. C’est encore une fois un sujet de recherche actif. Il y a des langages qui essaient de rendre encore plus transparente la frontière entre les mondes dynamiquement et statiquement typés. Cela demande de nouvelles méthodologies de typages, et tout une zoologie se crée autour du sujet : soft typing, gradual typing, blame typing, hybrid typing, …

En attendant, les programmeurs se contentent en général de méthodes plus indirectes, en utilisant des valeurs dans des types moins expressifs mais plus souples, comme le font sans le savoir les utilisateurs de langages dynamiques.

Les types ne font pas tout

Ce billet a beaucoup parlé des types, et de pourquoi le système de typage est un ingrédient majeur d’un langage de programmation. Il ne faut pas non plus oublier que ce n’est pas le seul, et qu’une grande partie de l’intérêt des langages ne vient pas du tout de leur système de types.^λ

L’un des livres sur la programmation qui m’a beaucoup plu est le CTM : Concepts, Techniques and Models of Computer Programming. C’est un livre vraiment formidable, qui a étendu mon horizon en matière de techniques de programmation, et qui pourtant ne parle pas du tout, ou quasiment pas, de typage.