Inférence de type

L'inférence de type reconstruit automatiquement les types des expressions, permettant aux programmeurs d'omettre les annotations tandis que le compilateur calcule une typisation la plus générale.

Definition

L'inférence de type (reconstruction de type) est le processus de déduction d'un type valide et le plus général pour une expression à partir de sa structure et de son utilisation, sans exiger du programmeur qu'il fournisse toutes les annotations de type.

Scope

Ce sujet couvre les algorithmes et la théorie de l'inférence de types sans annotations explicites, centrés sur le système Hindley-Milner et l'algorithme W avec son utilisation de l'unification et du let-polymorphisme. Il aborde les types principaux, la décidabilité et la complexité, ainsi que les difficultés d'étendre l'inférence à des systèmes plus riches avec le sous-typage, le polymorphisme de rang supérieur ou les types dépendants.

Core questions

• Comment un compilateur peut-il reconstruire les types lorsqu'aucun n'est spécifié ?
• Qu'est-ce qu'un type principal, et quand en existe-t-il toujours un ?
• Comment l'unification pilote-t-elle l'inférence Hindley-Milner ?
• Pourquoi l'inférence devient-elle indécidable ou incomplète dans des systèmes de types plus riches ?

Key theories

Hindley-Milner type inference

La discipline de types polymorphes de Milner, avec l'algorithme W, infère les types pour un lambda-calcul avec polymorphisme lié par `let` en utilisant l'unification, formant la base de l'inférence dans les langages de la famille ML.

Principal type schemes

Damas et Milner ont prouvé que toute expression typable possède un schéma de type principal, le type le plus général dont tous ses types valides sont des instances, et que l'algorithme W le calcule.

Principal types in combinatory logic

Hindley a établi l'existence de types principaux pour les termes typables, un résultat antérieur qui sous-tend l'inférence de type ultérieure dans les langages de programmation.

Clinical relevance

L'inférence de type rend les langages typés statiquement beaucoup plus pratiques en supprimant la charge d'annotation tout en préservant la sécurité, et elle alimente les fonctionnalités modernes des éditeurs comme les suggestions de type et l'autocomplétion. Ses limites dans les systèmes expressifs déterminent les cas où les programmeurs doivent encore fournir des annotations.

History

Les travaux de Hindley de 1969 sur les types principaux en logique combinatoire ont anticipé l'inférence pratique. L'article de Milner de 1978 a introduit le système de types polymorphes et l'algorithme W pour ML, et l'article de Damas et Milner de 1982 a prouvé la principalité. Le système Hindley-Milner est devenu la norme pour ML, Haskell et de nombreux langages ultérieurs, avec des recherches continues étendant l'inférence à des contextes plus riches.

Debates

How much to infer versus annotate

À mesure que les systèmes de types deviennent plus expressifs, l'inférence complète devient indécidable, ce qui suscite un débat sur la quantité d'informations à inférer automatiquement par rapport à celles qui doivent être requises comme annotations explicites pour maintenir l'inférence traitable et prévisible.

Key figures

• Robin Milner
• Luis Damas
• Roger Hindley
• Benjamin Pierce

Seminal works

• milner1978
• damas1982
• hindley1969
• pierce2002

Frequently asked questions

Qu'est-ce qu'un type principal ?

Un type principal est le type le plus général d'une expression, tel que tout autre type valide pour cette expression en est une instance par substitution ; l'inférence Hindley-Milner calcule toujours un type principal lorsqu'il en existe un.

Pourquoi tous les systèmes de types ne peuvent-ils pas inférer les types automatiquement ?

L'inférence repose sur des contraintes solubles ; dans les systèmes expressifs tels que ceux avec des types de rang supérieur ou dépendants, l'inférence complète devient indécidable, de sorte que certaines annotations doivent être fournies par le programmeur.