Le chemin vers la vérification de type de 4 millions de lignes de code Python. Partie 1

Aujourd'hui, nous portons à votre attention la première partie de la traduction du matériel sur la façon dont Dropbox traite le contrôle de type du code Python.

Dropbox écrit beaucoup en Python. C'est un langage que nous utilisons extrêmement largement, à la fois pour les services back-end et les applications clientes de bureau. Nous utilisons aussi beaucoup Go, TypeScript et Rust, mais Python est notre langage principal. Compte tenu de notre échelle, et nous parlons de millions de lignes de code Python, il s'est avéré que le typage dynamique d'un tel code compliquait inutilement sa compréhension et commençait à affecter sérieusement la productivité du travail. Pour atténuer ce problème, nous avons commencé à passer progressivement notre code à la vérification de type statique à l'aide de mypy. C'est probablement le système de vérification de type autonome le plus populaire pour Python. Mypy est un projet open source, ses principaux développeurs travaillent dans Dropbox.

Dropbox a été l'une des premières entreprises à implémenter la vérification de type statique dans le code Python à cette échelle. Mypy est utilisé dans des milliers de projets de nos jours. Cet outil d'innombrables fois, comme on dit, "testé au combat". Nous avons parcouru un long chemin pour arriver là où nous sommes maintenant. En cours de route, il y a eu de nombreuses entreprises infructueuses et des expériences ratées. Cet article couvre l'histoire de la vérification de type statique en Python, depuis ses débuts difficiles dans le cadre de mon projet de recherche, jusqu'à nos jours, lorsque la vérification de type et l'indication de type sont devenues monnaie courante pour d'innombrables développeurs qui écrivent en Python. Ces mécanismes sont maintenant pris en charge par de nombreux outils tels que les IDE et les analyseurs de code.

→ Lire la deuxième partie

Pourquoi la vérification de type est-elle nécessaire ?

Si vous avez déjà utilisé Python typé dynamiquement, vous pourriez avoir une certaine confusion quant à la raison pour laquelle il y a eu un tel tapage autour du typage statique et de mypy ces derniers temps. Ou peut-être que vous aimez Python précisément à cause de son typage dynamique, et ce qui se passe vous dérange tout simplement. La clé de la valeur du typage statique est l'échelle des solutions : plus votre projet est grand, plus vous penchez vers le typage statique, et au final, plus vous en avez vraiment besoin.

Supposons qu'un certain projet ait atteint la taille de dizaines de milliers de lignes et qu'il s'avère que plusieurs programmeurs y travaillent. En regardant un projet similaire, basé sur notre expérience, nous pouvons dire que comprendre son code sera la clé pour garder les développeurs productifs. Sans annotations de type, il peut être difficile de comprendre, par exemple, quels arguments passer à une fonction ou quels types une fonction peut renvoyer. Voici des questions typiques auxquelles il est souvent difficile de répondre sans utiliser d'annotations de type :

• Cette fonction peut-elle retourner None?
• Quel doit être cet argument ? items?
• Quel est le type d'attribut id: int est-ce, str, ou peut-être un type personnalisé ?
• Cet argument devrait-il être une liste ? Est-il possible de lui passer un tuple ?

Si vous regardez l'extrait de code annoté suivant et essayez de répondre à des questions similaires, il s'avère que c'est la tâche la plus simple :

class Resource:
    id: bytes
    ...
    def read_metadata(self, 
                      items: Sequence[str]) -> Dict[str, MetadataItem]:
        ...

• read_metadata ne revient pas None, puisque le type de retour n'est pas Optional[…].
• Argument items est une séquence de lignes. Il ne peut pas être itéré au hasard.
• Attribut id est une chaîne d'octets.

Dans un monde idéal, on s'attendrait à ce que toutes ces subtilités soient décrites dans la documentation intégrée (docstring). Mais l'expérience donne de nombreux exemples du fait qu'une telle documentation n'est souvent pas observée dans le code avec lequel vous devez travailler. Même si une telle documentation est présente dans le code, on ne peut pas compter sur son exactitude absolue. Cette documentation peut être vague, inexacte et ouverte à des malentendus. Dans les grandes équipes ou les grands projets, ce problème peut devenir extrêmement aigu.

Alors que Python excelle dans les premières ou les étapes intermédiaires des projets, à un moment donné, les projets réussis et les entreprises qui utilisent Python peuvent être confrontés à la question vitale : « Devrions-nous tout réécrire dans un langage typé statiquement ? ».

Les systèmes de vérification de type comme mypy résolvent le problème ci-dessus en fournissant au développeur un langage formel pour décrire les types et en vérifiant que les déclarations de type correspondent à l'implémentation du programme (et, éventuellement, en vérifiant leur existence). En général, on peut dire que ces systèmes mettent à notre disposition quelque chose comme une documentation soigneusement vérifiée.

L'utilisation de tels systèmes présente d'autres avantages, et ils sont déjà tout à fait non triviaux :

• Le système de vérification de type peut détecter quelques petites (et pas si petites) erreurs. Un exemple typique est lorsqu'ils oublient de traiter une valeur None ou une autre condition spéciale.
• La refactorisation du code est grandement simplifiée car le système de vérification de type est souvent très précis sur le code à modifier. Dans le même temps, nous n'avons pas besoin d'espérer une couverture de code à 100% avec des tests, ce qui, de toute façon, n'est généralement pas réalisable. Nous n'avons pas besoin de plonger dans les profondeurs de la trace de la pile pour trouver la cause du problème.
• Même sur de grands projets, mypy peut souvent effectuer une vérification de type complète en une fraction de seconde. Et l'exécution des tests prend généralement des dizaines de secondes voire des minutes. Le système de vérification de type donne au programmeur une rétroaction instantanée et lui permet de faire son travail plus rapidement. Il n'a plus besoin d'écrire des tests unitaires fragiles et difficiles à maintenir qui remplacent les entités réelles par des simulations et des correctifs juste pour obtenir des résultats de test de code plus rapidement.

Les IDE et les éditeurs tels que PyCharm ou Visual Studio Code utilisent la puissance des annotations de type pour fournir aux développeurs la complétion de code, la mise en évidence des erreurs et la prise en charge des constructions de langage couramment utilisées. Et ce ne sont là que quelques-uns des avantages de la dactylographie. Pour certains programmeurs, tout cela est le principal argument en faveur du typage. C'est quelque chose qui profite immédiatement après la mise en œuvre. Ce cas d'utilisation pour les types ne nécessite pas de système de vérification de type séparé comme mypy, bien qu'il convient de noter que mypy aide à maintenir la cohérence des annotations de type avec le code.

Contexte de mypie

L'histoire de mypy a commencé au Royaume-Uni, à Cambridge, quelques années avant que je ne rejoigne Dropbox. J'ai été impliqué, dans le cadre de ma recherche doctorale, dans l'unification des langages typés statiquement et dynamiques. Je me suis inspiré d'un article sur le typage incrémental de Jeremy Siek et Walid Taha, et du projet Typed Racket. J'ai essayé de trouver des moyens d'utiliser le même langage de programmation pour divers projets - des petits scripts aux bases de code composées de plusieurs millions de lignes. En même temps, je voulais m'assurer que dans un projet de toute envergure, on n'aurait pas à faire de trop gros compromis. Une partie importante de tout cela était l'idée de passer progressivement d'un projet de prototype non typé à un produit fini typé statiquement testé de manière approfondie. Ces jours-ci, ces idées sont largement tenues pour acquises, mais en 2010, c'était un problème qui était encore activement exploré.

Mon travail initial de vérification de type ne visait pas Python. A la place, j'ai utilisé un petit langage "fait maison" Aloré. Voici un exemple qui vous permettra de comprendre de quoi on parle (les annotations de type sont facultatives ici) :

def Fib(n as Int) as Int
  if n <= 1
    return n
  else
    return Fib(n - 1) + Fib(n - 2)
  end
end

L'utilisation d'une langue maternelle simplifiée est une approche courante utilisée dans la recherche scientifique. Il en est ainsi, notamment parce que cela vous permet de mener rapidement des expériences, et aussi parce que ce qui n'a rien à voir avec l'étude peut être facilement ignoré. Les langages de programmation du monde réel ont tendance à être des phénomènes à grande échelle avec des implémentations complexes, ce qui ralentit l'expérimentation. Cependant, tout résultat basé sur un langage simplifié semble un peu suspect, car en obtenant ces résultats, le chercheur peut avoir sacrifié des considérations importantes pour l'utilisation pratique des langues.

Mon vérificateur de type pour Alore semblait très prometteur, mais je voulais le tester en expérimentant avec du code réel, qui, pourrait-on dire, n'a pas été écrit dans Alore. Heureusement pour moi, le langage Alore était largement basé sur les mêmes idées que Python. Il était assez facile de refaire le vérificateur de type pour qu'il puisse fonctionner avec la syntaxe et la sémantique de Python. Cela nous a permis d'essayer la vérification de type dans le code Python open source. De plus, j'ai écrit un transpiler pour convertir le code écrit en Alore en code Python et l'ai utilisé pour traduire mon code de vérificateur de caractères. Maintenant, j'avais un système de vérification de type écrit en Python qui supportait un sous-ensemble de Python, une sorte de ce langage ! (Certaines décisions architecturales qui avaient du sens pour Alore étaient mal adaptées à Python, et cela est encore perceptible dans certaines parties de la base de code mypy.)

En fait, le langage pris en charge par mon système de type ne pouvait pas tout à fait s'appeler Python à ce stade : c'était une variante de Python en raison de certaines limitations de la syntaxe d'annotation de type Python 3.

Cela ressemblait à un mélange de Java et de Python :

int fib(int n):
    if n <= 1:
        return n
    else:
        return fib(n - 1) + fib(n - 2)

Une de mes idées à l'époque était d'utiliser des annotations de type pour améliorer les performances en compilant ce type de Python en C, ou peut-être en bytecode JVM. Je suis arrivé au stade de l'écriture d'un prototype de compilateur, mais j'ai abandonné cette idée, car la vérification de type elle-même semblait très utile.

J'ai fini par présenter mon projet au PyCon 2013 à Santa Clara. J'en ai aussi parlé avec Guido van Rossum, le bienveillant dictateur Python à vie. Il m'a convaincu d'abandonner ma propre syntaxe et de m'en tenir à la syntaxe standard de Python 3. Python 3 prend en charge les annotations de fonction, donc mon exemple pourrait être réécrit comme indiqué ci-dessous, ce qui donnerait un programme Python normal :

def fib(n: int) -> int:
    if n <= 1:
        return n
    else:
        return fib(n - 1) + fib(n - 2)

J'ai dû faire quelques compromis (tout d'abord, je tiens à souligner que j'ai inventé ma propre syntaxe pour cette raison même). En particulier, Python 3.3, la version la plus récente du langage à l'époque, ne supportait pas les annotations de variables. J'ai discuté avec Guido par e-mail de diverses possibilités de conception syntaxique de telles annotations. Nous avons décidé d'utiliser des commentaires de type pour les variables. Cela servait l'objectif visé, mais était quelque peu lourd (Python 3.6 nous a donné une syntaxe plus agréable):

products = []  # type: List[str]  # Eww

Les commentaires de type se sont également avérés utiles pour prendre en charge Python 2, qui n'a pas de prise en charge intégrée des annotations de type :

f fib(n):
    # type: (int) -> int
    if n <= 1:
        return n
    else:
        return fib(n - 1) + fib(n - 2)

Il s'est avéré que ces compromis (et d'autres) n'avaient pas vraiment d'importance - les avantages du typage statique signifiaient que les utilisateurs oubliaient rapidement la syntaxe moins que parfaite. Étant donné qu'aucune construction syntaxique spéciale n'a été utilisée dans le code Python dont le type a été vérifié, les outils Python et les processus de traitement de code existants ont continué à fonctionner normalement, ce qui a facilité l'apprentissage du nouvel outil par les développeurs.

Guido m'a également convaincu de rejoindre Dropbox après avoir terminé ma thèse de diplôme. C'est là que commence la partie la plus intéressante de l'histoire de mypy.

A suivre ...

Chers lecteurs, Si vous utilisez Python, veuillez nous indiquer l'ampleur des projets que vous développez dans ce langage.

Source: habr.com