Nous avons abordé dans le deuxième billet la relation entre le système de types d’un langage de programmation et la manière dont il était exécuté. Deux principaux points sont à retenir:

• les langages statiques (compilés avant exécution) utilisent les annotations de type pendant la compilation pour détecter d’éventuelles erreurs et optimiser le code traduit ;
• les langages dynamiques (interprétés) n’ont pas besoin d’annotations de type puisque la validité du code est vérifiée à l’exécution uniquement.

Mais vous l’avez sûrement remarqué, le système de types de C++ ne ressemble pas du tout à celui de mypy (version typée de Python). Cet article va dégager deux axes de différenciation pour classifier les systèmes de types, et donner quelques éléments pour comprendre la manière dont le typage marche.

Le typage explicite

C’est la manière la plus simple d’implémenter un système de types. C’est aussi celle utilisée par la majorité des langages statiques : C, C++, Java, Go, etc. Le principe de ce typage est très simple : lorsque l’on déclare une variable ou une fonction, on l’annote par son type. Par exemple en C :

float inverse(float x) {
    if (x == 0.0)
        return 0.0;
    else {
        float inv = 1/x;
        return inv;
    }
}

Tous les types sont ici annotés : l’argument de la fonction, ce qu’elle retourne, la variable intermédiaire inv, etc. Pour vérifier si nos annotations de type sont correctes, il suffit de:

• vérifier que le type de ce qui est retourné par return correspond au type de retour de la fonction ;
• vérifier que les fonctions sont appelées avec des arguments du bon type ;
• vérifier que les opérateurs (+, ==, /) opèrent sur des valeurs du bon type.

L’avantage du typage explicite est que la vérification effectuée par le compilateur est assez simple, et permet de remonter des messages d’erreur explicites à l’utilisateur. Par exemple, Erreur de types : (+) à la ligne 186 est appelé avec float et int, qui sont incompatibles. Néanmoins, la déclaration systématique de tous les types est lourde pour l’utilisateur. Elle est même parfois redondante : C++ a introduit dans C++11 le mot-clé auto qui permet de déduire le type d’une variable lors de son initialisation par un expression.

Ceci nous pose la question suivante : à quel point ces déclarations de type sont-elles redondantes ? Quelle est le nombre minimal de déclaration de types à faire pour que le compilateur puisse déduire le type de toutes les autres variables ? Les mécanismes de typage implicite fournissent une réponse à ces questions.

Le typage implicite

Tout d’abord, il est nécessaire de dissiper un malentendu : Python ou Javascript ne sont pas typés implicitement. Python et Javascript ne sont pas typés, ou plutôt toutes les variables en Python ou Javascript ont un unique type, le type de tout et n’importe quoi. Comme précisé dans le deuxième billet, cela se paye par de nombreuses vérifications lors de l’exécution. Il existe néanmoins une catégorie hybride et récente de systèmes de type, à mi-chemin entre typage explicite et absence de typage. Dans cette catégorie rentrent Typescript ou mypy. En effet, même si le principe dans ces langages est de déclarer une partie seulement des types, ce n’est pas du typage implicite pour autant. Car le compilateur fonctionne de la manière suivante:

• losrque le compilateur dispose des informations de type pour vérifier quelque chose, il le vérifie et renvoie un message d’erreur si erreur il y a ;
• lorsque le type des variables n’est pas spécifié, le compilateur ne vérifie rien du tout.

Le vrai typage implicite se fait par un mécanisme plus sophistiqué appelé inférence de types. L’algorithme le plus célèbre d’inférence de type s’appelle Hindley-Milner, mais le décrire complètement va au-delà du niveau de ce blog. Par contre, il est possible d’avoir une intuition de comment il marche. Pour cela, prenons un exemple de programme en OCaml :

let increment l = List.map (fun a -> a + 1) l

Ceci est la définition de la fonction increment qui prend en argument la variable l dont le type n’est pas explicitement déclaré. Néanmoins, à la compilation, OCaml va pouvoir déterminer le type de l avec précision, et nous allons voir comment. Tout d’abord, OCaml va assigner des types inconnus aux variables du programme : X à l et Y à a. Cela donne :

let increment (l : X) = List.map (fun (a : Y) -> a + 1) l

Puis OCaml va examiner le type de la fonction List.map, qui est ('a -> 'a) -> 'a list -> 'a list. Pour ceux qui ont oublié le sens de cette notation, il est expliqué dans le billet sur la programmation fonctionnelle. Ici, 'a est un peu comme X, un type arbitraire. Cela veut dire que la fonction List.map ne se soucie pas du type des éléments de la liste ; il faut juste que ce soit une liste. En analysant les arguments de List.map dans increment, il va alors déduire les égalités suivantes : X = 'a list et Y = 'a. Puis, OCaml analyse l’expression a + 1 et en déduit que a a le même type que 1 (pour pouvoir être additionné), c’est à dire int: Y = int. Des trois égalités déduites, on peut avoir Y = int et X = int list, ce qui détermine bien les types de toutes les variables de notre programme:

let increment (l : int list) = List.map (fun (a : int) -> a + 1) l

On voit ici que lorsque l’utilisateur fait une erreur dans son programme, cela se traduit par des égalités de type qui se contredisent entre elles : par exemple ou aurait pu avoir X = int et X = float. Dans ce cas, le compilateur doit se débrouiller pour renvoyer à l’utilisateur un message d’erreur le plus clair possible, mais cela est difficile car les bouts de programmes qui donnent X = int et X = float peuvent être éloignés les uns des autres. C’est pour cette raison que les messages d’erreurs renvoyés par les compilateurs de langages avec inférence de type sont réputés cryptique, même s’ils se sont beaucoup améliorés ces dernières années.

On voit donc que le typage implicite est totalement compatible avec un langage statique, et que c’est justement là où il est le plus pertinent. La plupart des langages fonctionnels (OCaml, Haskell) ou récents (Swift, Rust) sont typés implicitement et utilisent l’inférence de type pour déterminer ce que l’utilisateur n’a pas spécifié. Néanmoins, implémenter un algorithme d’inférence de type est assez complexe, et nécessite de formaliser mathématiquement le système de type de son langage. Car la théorie du typage est avant tout un sous-ensemble de la théorie de la logique en mathématique.

Typage fort ou faible : une dénomination marketing

À des fins de marketings, des langages comme Javascript se sont proclamés « faiblement typés », en contraste avec des langages comme Python qui se veulent « fortement typés ». Cette distinction très répandue est en fait source de confusion et n’a pas vraiment de base logique : dissipons une fois encore les malentendus. Les tenants de la disctinction faiblement/fortement typé désignent par ces appellations le comportement du langage de programmation lorsque l’utilisateur entre un programme typé incorrectement. En effet, dans un langage « faiblement typé » comme Javascript, il est possible d’écrire quelque chose comme 3 + 4 + "5" qui donne "75", alors que 3 + 4 + +"5" donne 12. Ceci est traditionnellement mis en opposition avec un Python qualifié de « fortement typé », parce qu’en Python "5" + 6 soulève dynamiquement l’erreur TypeError: Can't convert 'int' object to str implicitly. Il convient de rappeler que Python n’est pas un langage typé car purement dynamique (du moins sans mypy) ; il respecte cependant une certaine logique à l’exécution.

Un langage « faiblement typé » prend donc le parti de donner du sens à des expressions qui seraient normalement incorrectes. Les défenseurs de cette philosophie mettent en avant une certaine flexibilité, car le langage respecte l’esprit du code même lorsque celui-ci est incorrect. Évidemment, débogguer une application de plusieurs milliers de lignes dans un langage faiblement typé devient vite un cauchemar, par exemple lorsque le programme renvoie des résultats apparemment aléatoires à cause d’une conversion implicite qui a mal tourné quelque part dans le code.

Les langages « faiblement typés » poussent donc jusqu’à l’extrême la philosophie de programmation évoquée dans le deuxième billet et qui consiste à donner une priorité absolue à la facilité de programmation, au détriment de la logique et de la cohérence. Encore une fois, si cela est pratique pour un petit script, développer une application professionnelle avec un tel langage est la promesse de la catastrophe industrielle. Ce n’est pas pour rien que Facebook, codé à l’origine en PHP et en Javascript, investit massivement dans le développement de Hack et Reason, pendants « fortement typés » de ces deux langages. Ou que mypy, extension typée de Python, est développée par Dropbox, dont la base de code est en Python.

Néanmoins, cette opposition entre conversion implicites facilitées et système de type cohérent n’existe même pas. Il est possible d’avoir le beurre et l’argent du beurre : en Rust, ces conversions sont implicites dans la syntaxe mais bien prises en compte par le système de type (trait Into). Un trait est similaire à une interface Java (voir le billet sur la programmation orientée objet). Une fonction peut avoir un argument de type Into<i32> (i32 est un entier 32 bits), ce qui veut dire que l’on peut passer à la fonction n’importe quel objet qui implémente la fonction into() -> i32, même si l’objet n’a pas le type i32.

La terminologie « fortement typée » n’a donc pas de sens précis, et est utilisée à tort et à travers pour qualifier des systèmes de types qui présenteraient une certaine logique. Or il est possible de définir formellement cette notion de « cohérence logique entre le système de types et l’exécution du programme ». Lorsque l’on est capable de formaliser mathématiquement son langage de programmation et son système de type, on peut prouver des théorèmes sur son langage. Le théorème faisant office de Saint-Graal des concepteurs de langages de programmation est la sûreté du typage (type safety), qui garantit que tout programme valide (c’est à dire bien typé) va s’exécuter correctement, c’est à dire qu’à tout moment pendant l’exécution les valeurs calculées auront un type bien défini, et que ladite exécution pourra toujours se poursuivre selon les règles jusqu’à arriver au résultat final du programme (ou entrer dans une boucle infinie). En conclusion, au delà des appellations marketings, il existe des concepts formels pour classifier les systèmes de types dont j’espère vous avoir donné un petit aperçu à travers ce billet.

Pour aller plus loin

• Comment renvoyer des messages d’erreur compréhensibles par l’utilisateur avec un compilateur de plus en plus complexes est un sujet de recherche contemporaine, en témoigne cet article de 2016 de François Pottier sur les messages d’erreurs dans son parseur, Menhir.
• Pour les plus courageux qui veulent comprendre comment formaliser un langage de programmation et prouver des théorèmes dessus, je conseille vivement la lecture de Foundations of Programming Languages qui construit tout l’édifice théorique à partir des fondations.