Pourquoi attacher tant d'importance au typage ?

(Gabriel Scherer (gasche) @ 2009-12-30 13:34:33)

La réponse, enfin dévoilée ! Bluestorm Origins: The Typing Mystery, maintenant dans les blogs (well, le nôtre du moins :-°). —rz0

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.

α : On pourrait croire à une circularité ici : si les types parlent du langage tout en en faisant partie, alors les types parlent des types et le monde s’écroule. En réalité, la plupart des langages de types ne sont pas suffisamment expressifs, et ne parlent que d’une partie restreinte du langage (qu’on appelle souvent les valeurs). Mais il existe effectivement des langages (par exemple Coq) dans lesquels les types ont eux aussi un type, qui a à son tourβ un type… Il peut bien sûr exister un nombre infini de types différents, bien qu’un programme donné ne les utilise pas tous en même temps.

β : « Turtles all the way down ! » ;-)

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

γ : En fait, PLT Scheme permet aussi la vérification des types ; je suis impressionné par cette implémentation de Scheme.

δ : Je parle ici de la sémantique du langage, c’est à dire d’une définition un peu abstraite du comportement (ou sens) des programmes. Ce n’est pas une question d’implémentation : si on crée un compilateur pour un langage avec cette séparation, on peut très bien choisir de faire des optimisations en raisonnant sur le type des variables, par exemple en changeant leur représentation mémoire (boxing, etc.), du moment que cela crée aucune différence de comportement du programme observable par le programmeur.

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.

ε : Limitation qui n’en est pas toujours une : on peut faire des choses très intéressantes avec des langages non Turing-complets (par exemple les expressions régulières/rationnelles, quand elles le sont vraiment, ou Coq).

ζ : Jacques Guarrige, Code reuse through polymorphic variants

The idea for this example originally comes from a post by Phil Wadler on the Java-Genericity mailing list W+98, in which he proposed a solution to the Expression Problem, that is the problem of extending a variant type with new constructors without recompiling code for old ones. A similar problem and solution can be found in KFF98, but untyped. It appeared later that Wadler’s solution, which already supposed an extension of Generic Java, itself an extension of Java, could not be typed. Didier Rémy, Jérôme Vouillon and myself finally came up with a typable solution in an object-oriented extension of the 3rd order typed lambda-calculus, which was later checked correct by Haruo Hosoya in F-omega- sub-rec. On the other hand, I could provide a much shorter solution in about 15 lines of Objective Label using polymorphic variants, which were merged later in Objective Caml. The solution used only standard ML-polymorphism, which is a weakened 2nd order typed lambda-calculus, and can be inferred automatically.

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.

η : Rz0 me signale que cette « meilleure compréhension » n’a pas du tout affecté la pratique des programmeurs qui, sur le terrain, utilisent des effets de bords, et qu’il est donc un peu « osé » de présenter les monades comme une réussite de ce point de vue. C’est en effet un peu plus compliqué que ça : notre compréhension théorique des effets de bords s’est améliorée, mais on a aussi découvert que les monades sont des outils trop généraux, qu’elles s’appliquent à beaucoup de choses qui ne sont pas considérées habituellement comme des effets de bords, et qu’elles ne sont pas toujours assez précises.

Pour la gestion de la mémoire par exemple, une monade ne peut pas raisonner, au niveau du typage, sur l’étendue des zones mémoires affectées par un programme : la monade saura dire de deux programmes qu’ils modifient la mémoire, mais pas si les zones de mémoire qu’ils utilisent sont disjointes ou s’il y a des interactions entre les deux. On a besoin de ces propriétés plus fines, et on est en train de développer des outils plus spécialisés et plus complexes, comme les systèmes d’effets et les logiques de séparation.

Enfin, même si ces idées mettent du temps à sortir de leur cadre théorique pour atterrir dans la boîte à outils des programmeurs, elles restent présentes dans l’industrie, avec par exemple les outils d’analyse statique de programmes, qui suivent d’assez près les progrès de la recherche dans ce domaine. L’arrivée du concept dans un langage de programmation grand public est la dernière étape (après l’entrée dans les langages expérimentaux comme DDC ou ATS), qui se fera plus tard, ou peut-être pas du tout, si l’on constate que les bénéfices de ces méthodes ne compensent pas l’ajout en complexité.

η´ : Et puis d’abord, si l’exemple des monades ne vous plaît pas, en voici un autre : les continuations. Le comportement dynamique de call/cc est bien connu, mais l’étude de son lien avec le typage et la logique classique est au moins aussi intéressante.

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.

θ : Voir par exemple les travaux de Greg Morrisset ou George Necula sur les assembleurs fortement typés.

La réaction de rz0 de sujet souligne un autre aspect du problème :

À mon avis, un point intéressant, et pas du tout développé dans la plupart des visions « haut niveau » de l’assembleur, c’est les contraintes sur les adresses ou la mémoire : représentation, décalage, facteur, taille, alignement, granularité, etc. Je considère que c’est du typage aussi, et c’est du typage « utile », dans le sens où si les données fournies aux opérandes sont mal typées, soit ça n’assemble pas (p.ex. parce qu’il n’y a pas assez de bits pour représenter l’adresse entièrement), soit ça balance une exception au runtime (si on passe un registre et que sa valeur ne vérifie pas les conditions de typage). Bref, je trouve que ce n’est pas « rien à dire ».

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.

ι : Un anglicisme qui désigne le « moment de l’exécution », à nuancer de compile-time ou parse-time, et dont j’ai beaucoup de mal à me débarrasser.

κ : C’est ce que j’ai utilisé dans Macaque ; j’avais besoin d’une méthode sûre pour traiter la perte de typage des données passant par le serveur SQL (qui n’utilise que des chaînes de caractères), et je me retrouvé, sans m’en rendre compte au départ, avec du typage dynamique fait maison.

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

On peut remarquer que cette approche (construction automatique, par le langage directement, de la description runtime de type) brise la propriété de séparation, que j’ai évoquée précédemment, entre la phase de typage et la phase d’exécution.

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.

λ : Même si vous seriez sans doute surpris par la quantité de chose qu’on peut présenter sous forme d’un typage, ou en relation avec le typage : sécurité, performances, invariants de structures de données, etc.