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

Aujourd'hui, nous vous proposons la première partie de la traduction d'un document sur la manière dont Dropbox s'occupe du contrôle des types dans le code Python.

Chez Dropbox, nous écrivons beaucoup en Python. C'est un langage que nous utilisons de manière extrêmement large, tant pour les services backend que pour les applications clients de bureau. Nous utilisons également beaucoup Go, TypeScript et Rust, mais Python est notre langage principal. Compte tenu de nos dimensions, avec des millions de lignes de code Python, il s'est avéré que la typage dynamique de ce code compliquait de manière injustifiée sa compréhension et commençait à avoir un impact sérieux sur la productivité. Pour atténuer ce problème, nous avons commencé à traduire progressivement notre code vers une vérification statique des types en utilisant mypy. C'est probablement le système de vérification des types autonome le plus populaire pour Python. Mypy est un projet open-source, et ses principaux développeurs travaillent chez Dropbox.

Dropbox a été l'une des premières entreprises à mettre en œuvre la vérification statique des types dans le code Python à une telle échelle. De nos jours, mypy est utilisé dans des milliers de projets. Cet outil a été testé des centaines de milliers de fois, ce qu'on appelle « testé en condition réelle ». Pour arriver là où nous sommes actuellement, nous avons dû parcourir un long chemin. Sur ce chemin, il y a eu de nombreux échecs et des expériences ratées. Ce document raconte l'histoire de la vérification statique des types en Python — depuis ses débuts difficiles, qui faisaient partie de mon projet de recherche, jusqu'à aujourd'hui, où les vérifications et les suggestions de types sont devenues familières à d'innombrables développeurs qui programment en Python. Ces mécanismes sont maintenant compatibles avec de nombreux outils, tels que les IDE et les analyseurs de code.

→ Lire la deuxième partie

Pourquoi est-il nécessaire d'effectuer une vérification des types ?

Si vous avez déjà utilisé Python à typage dynamique, vous pourriez être perplexe quant au récent engouement autour du typage statique et de mypy. Peut-être aimez-vous Python justement pour son typage dynamique, et ce qui se passe vous frustre simplement. La clé de la valeur du typage statique réside dans l'échelle des solutions : plus votre projet est grand, plus vous êtes enclin à opter pour le typage statique, et, finalement, plus cela devient véritablement nécessaire.

Supposons qu'un projet ait atteint des dizaines de milliers de lignes, et qu'il implique plusieurs développeurs. En examinant un tel projet, nous pouvons dire, sur la base de notre expérience, que comprendre son code sera la clé pour maintenir la productivité des développeurs. Sans annotations de type, il est parfois difficile de comprendre, par exemple, quels arguments doivent être passés à une fonction, ou quels types de valeurs une fonction peut retourner. Voici des questions typiques auxquelles il est souvent difficile de répondre sans utiliser des annotations de type :

• Cette fonction peut-elle retourner TSSAA?
• Quel type cet argument doit-il être items?
• Quel est le type de l'attribut id: int est-ce que c'est str, ou peut-être un type personnalisé ?
• Cet argument doit-il être une liste ? Peut-on y passer un tuple ?

Si l'on examine le fragment de code suivant, accompagné d'annotations de type, et que l'on essaie de répondre à de telles questions, il s'avère que c'est une tâche des plus simples :

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

• read_metadata ne retourne pas TSSAA, car le type retourné n'est pas Optional[…].
• Argument items — c'est une séquence de chaînes. On ne peut pas l'itérer dans n'importe quel ordre.
• Attribut id — c'est une chaîne d'octets.

Dans un monde idéal, on pourrait s'attendre à ce que toutes ces subtilités soient décrites dans la documentation intégrée (docstring). Mais l'expérience fournit de nombreux exemples montrant que ce type de documentation est souvent absent du code avec lequel nous travaillons. Même si une telle documentation existe dans le code, on ne peut pas compter sur son absolue exactitude. Cette documentation peut être floue, inexacte, et laisser place à de nombreuses interprétations erronées. Dans de grandes équipes ou dans de gros projets, ce problème peut devenir très aigu.

Bien que Python fonctionne très bien aux premières ou intermédiaires étapes des projets, à un certain moment, les projets et les entreprises qui utilisent Python peuvent faire face à une question cruciale : « Devons-nous tout réécrire dans un langage à typage statique ? ».

Des systèmes de vérification de types comme mypy résolvent ce problème car ils fournissent aux développeurs un langage formel pour décrire les types, et vérifient que ces descriptions correspondent aux implémentations des programmes (et, en option, vérifient leur existence). En général, on peut dire que ces systèmes offrent une sorte de documentation rigoureusement vérifiée.

L'utilisation de tels systèmes présente d'autres avantages, qui ne sont pas du tout négligeables :

• Le système de vérification de types peut détecter certaines erreurs mineures (et également des erreurs plus significatives). Un exemple typique est lorsque l'on oublie de traiter une valeur TSSAA ou une autre condition particulière.
• Le refactoring du code devient beaucoup plus simple, car le système de vérification de types indique souvent très précisément quel code doit être modifié. De plus, nous n'avons pas besoin de compter sur une couverture totale du code par des tests, ce qui est généralement irréalisable. Nous n'avons pas à plonger dans les profondeurs des rapports de trace de pile pour comprendre la cause d'un problème.
• Même dans de grands projets, mypy peut souvent effectuer une vérification complète des types en quelques fractions de seconde. Alors que l'exécution des tests prend généralement des dizaines de secondes, voire des minutes. Le système de vérification des types donne aux programmeurs un retour d'information instantané et leur permet de travailler plus rapidement. Ils n'ont plus besoin d'écrire des tests unitaires fragiles et difficiles à maintenir, qui remplacent des entités réelles par des mocks et des patches juste pour obtenir des résultats de test de code plus rapidement.

Les IDE et éditeurs, comme PyCharm ou Visual Studio Code, tirent parti des annotations de types pour offrir aux développeurs des fonctionnalités d'auto-complétion de code, de mise en surbrillance des erreurs, et de support des constructions linguistiques couramment utilisées. Ce sont là seulement quelques-uns des avantages offerts par la typage. Pour certains programmeurs, tout cela constitue l'argument principal en faveur de la typage. C'est ce qui apporte des bénéfices immédiatement après sa mise en œuvre dans le travail. Cette utilisation des types ne nécessite pas l'application d'un système de vérification des types distinct, comme mypy, bien qu'il faille noter que mypy aide à maintenir la conformité entre les annotations de types et le code.

Contexte de mypy

L'histoire de mypy a commencé au Royaume-Uni, à Cambridge, quelques années avant que je ne rejoigne Dropbox. Je travaillais, dans le cadre de ma recherche doctorale, sur la question de l'unification des langages de programmation statiquement typés et dynamiques. J'étais inspiré par un article sur la typage progressive de Jeremy Siek et Valida Taha, ainsi que par le projet Typed Racket. Je cherchais des moyens d'utiliser le même langage de programmation pour différents projets — allant de petits scripts à des bases de code comptant des millions de lignes. Je voulais que, quel que soit l'échelle du projet, il n'y ait pas besoin de faire trop de compromis. Une partie importante de tout cela était l'idée d'une transition progressive d'un prototype non typé à un produit final entièrement testé et statiquement typé. De nos jours, ces idées sont largement considérées comme acquises, mais en 2010, c'était un problème qui était encore activement recherché.

Mon travail initial sur la vérification des types n'était pas axé sur Python. À la place, j'ai utilisé un petit langage « fait maison » AloreVoici un exemple qui vous permettra de comprendre de quoi il s'agit (les annotations de type ici ne sont pas obligatoires) :

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'un langage simplifié de développement interne est une approche courante en recherche scientifique. Cela est en grande partie dû au fait que cela permet de mener des expériences rapidement, et aussi parce que ce qui n'est pas pertinent pour la recherche peut être ignoré sans problème. Les langages de programmation réellement utilisés sont généralement des phénomènes complexes avec des implémentations élaborées, ce qui ralentit les expériences. Cependant, les résultats basés sur un langage simplifié semblent un peu suspects, car lors de l'obtention de ces résultats, le chercheur a peut-être sacrifié des considérations importantes pour l'utilisation pratique des langages.

Mon outil de vérification de type pour Alore semblait très prometteur, mais je voulais le tester en réalisant des expériences avec du code réel, qui, on peut le dire, n'avait pas été écrit sur Alore. Heureusement, le langage Alore était largement basé sur les mêmes idées que Python. Il a donc été suffisamment simple de réécrire l'outil de vérification de type pour qu'il puisse travailler avec la syntaxe et la sémantique de Python. Cela m'a permis de tester la vérification de type sur du code Python open source. De plus, j'ai écrit un transpileur pour transformer le code écrit en Alore en code Python et l'ai utilisé pour traduire le code de mon outil de vérification de type. J'avais maintenant un système de vérification de type écrit en Python, qui soutenait un sous-ensemble de Python, une sorte de variante de ce langage ! (Certaines décisions architecturales qui avaient du sens pour Alore s'adaptaient mal à Python, cela se remarque encore dans certaines parties de la base de code de mypy.)

En fait, le langage soutenu par mon système de types ne pouvait pas vraiment être qualifié de Python à ce moment-là : c'était une variante de Python en raison de certaines limitations de syntaxe des annotations de type de Python 3.

C'était comme 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)

L'une de mes idées à l'époque était d'utiliser des annotations de types pour améliorer les performances en compilant cette version de Python en C, ou peut-être en bytecode JVM. J'ai avancé jusqu'à la phase d'écriture d'un prototype de compilateur, mais j'ai abandonné ce projet, car la vérification des types semblait déjà suffisamment utile en soi.

Finalement, j'ai présenté mon projet à la conférence PyCon 2013 à Santa Clara. J'en ai également discuté avec Guido van Rossum, le généreux dictateur à vie de Python. Il m'a convaincu d'abandonner ma propre syntaxe et de me conformer à la syntaxe standard de Python 3. Python 3 prend en charge les annotations de fonction, de sorte que mon exemple pouvait être réécrit comme indiqué ci-dessous, produisant un programme Python valide :

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

J'ai dû faire certains compromis (je souligne d'abord que j'ai inventé ma propre syntaxe pour cette raison). En particulier, Python 3.3, la version la plus récente du langage à l'époque, ne prenait pas en charge les annotations de variables. J'ai discuté par e-mail avec Guido des différentes options de syntaxe pour ces annotations. Nous avons décidé d'utiliser des commentaires avec des indications de type pour les variables. Cela atteignait l'objectif, mais paraissait un peu encombrant (Python 3.6 nous a donné une syntaxe plus agréable):

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

Les commentaires avec types étaient également utiles pour la prise en charge de Python 2, qui n'a pas de prise en charge intégrée des annotations de types :

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 (et d'autres) compromis n'avaient en fait pas beaucoup d'importance — les avantages de la typage statique ont conduit les utilisateurs à oublier rapidement la syntaxe pas tout à fait parfaite. Comme dans le code Python où les types étaient contrôlés, aucune construction syntaxique spéciale n'était appliquée, les outils et processus existants pour le traitement du code Python ont continué à fonctionner normalement, ce qui a grandement facilité l'apprentissage de ce nouvel outil par les développeurs.

Guido m'a également convaincu de rejoindre Dropbox après que j'ai défendu ma thèse. C'est ici que commence la partie la plus intéressante de l'histoire de mypy.

À suivre...

Chers lecteurs ! Si vous utilisez Python, nous vous invitons à nous parler des projets de quelle envergure vous développez avec ce langage.

Source : habr.com