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.