Typage statique et dynamique

Le typage statique vérifie les types avant l'exécution d'un programme, tandis que le typage dynamique les vérifie pendant l'exécution ; le typage graduel vise à combiner les deux au sein d'un même langage.

Definition

Le typage statique vérifie les contraintes de type à la compilation afin que les programmes bien typés soient acceptés avant l'exécution ; le typage dynamique reporte les vérifications de type à l'exécution, générant des erreurs lorsque des opérations sont appliquées à des valeurs de type inapproprié.

Scope

Ce sujet couvre l'éventail des moments et des modalités de la vérification des types : la vérification statique qui rejette les programmes mal typés à la compilation, la vérification dynamique qui détecte les erreurs de type à l'exécution, et le typage graduel ou optionnel qui permet aux deux de coexister. Il aborde les garanties, la flexibilité et les implications en termes de performances de chaque approche, ainsi que la solidité de la discipline de vérification des types.

Core questions

• Quelles classes d'erreurs la vérification statique prévient-elle et que la vérification dynamique ne peut pas anticiper ?
• Quelle flexibilité le typage dynamique offre-t-il, et à quel prix ?
• Comment le typage graduel peut-il mélanger de manière cohérente du code typé et non typé ?
• Comment la solidité d'une discipline de typage statique est-elle établie ?

Key theories

Typage graduel

Siek et Taha ont défini un système de types qui permet à certaines parties d'un programme d'être typées statiquement et à d'autres dynamiquement, avec une relation de cohérence régissant l'interaction sécurisée à la frontière.

Solidité du typage statique

La méthode de progression et de préservation de Wright et Felleisen montre qu'un système de typage statique solide garantit que les programmes bien typés n'atteignent jamais d'états bloqués, formalisant ainsi la sécurité de la vérification statique.

Clinical relevance

Le choix entre typage statique et dynamique influence le flux de travail des développeurs, les outils et la fiabilité. Les systèmes de typage graduel et optionnel, tels que ceux superposés aux langages dynamiques, permettent aux équipes d'ajouter des garanties statiques de manière incrémentielle à de grandes bases de code existantes.

History

Les premiers langages se sont divisés en lignées à typage statique (Algol, Pascal, ML) et à typage dynamique (Lisp, Smalltalk). À mesure que les langages dynamiques gagnaient en popularité pour leur productivité, les chercheurs ont cherché à concilier les approches ; le typage graduel de Siek et Taha en 2006 et les travaux contemporains sur les types optionnels ont conduit à des systèmes de typage graduel largement utilisés, construits sur des langages dynamiques.

Debates

Coût et solidité du typage graduel

Les chercheurs débattent si un typage graduel solide peut éviter des coûts de vérification d'exécution prohibitifs aux frontières typées/non typées, et si un typage 'optionnel' non solide constitue un meilleur compromis pratique.

Key figures

• Benjamin Pierce
• Jeremy Siek
• Walid Taha
• Matthias Felleisen

Seminal works

• pierce2002
• siek2006
• wright1994

Frequently asked questions

Le typage statique est-il toujours meilleur que le typage dynamique ?

Aucun n'est universellement supérieur ; le typage statique détecte davantage d'erreurs précocement et facilite l'outillage, tandis que le typage dynamique offre flexibilité et prototypage plus rapide. Le choix approprié dépend donc des besoins du projet en matière de fiabilité et d'agilité.

Qu'est-ce que le typage graduel ?

Le typage graduel permet à un même programme de mélanger des portions typées statiquement et dynamiquement, en insérant des vérifications à l'exécution aux frontières afin que le code typé conserve ses garanties tandis que le code non typé reste flexible.