Conclusion

Ce cours est loin d’être complet. Nous nous sommes concentré sur un des aspects du typage : la sécurité de l’évaluation. Pourtant dans l’introduction, nous en avions mentionnés atraits. Un aspect qui prend de plus en plus d’importance est celui de l’analyse de programmes. De nombreuses analyses de programmes, par exemple analyse de strictité, analyse de graphe d’appel, analyse du moment de liaison ont été initialement introduites avec des analyses spécialisés, mais petits à petits ces analyses sont présentées comme des typages pour un système de types particulier. Cette identifiation a bénéficier aussi bien à ces domaines particulier qu’au systèmes de types eux-mêmes. Par exemple, l’algorithme de sous typage est en partie déduit d’analyse de graphes d’appel. La plupart de ces analyses permettent une meileurs compilation des langages fortement typés.

Le typage est également à la base d’une optimisation de compilation qui consiste à représenter les valeurs de bases non boxés. Le système de typage des effets de bord à l’aide de région permet une analyse assez fine de la durée de vie des valeurs, permettant une allocation en pile plutôt que dans le tas.

Un autre domaine d’application du typage que nous avons peu exploité est de permettre des résultats sémantiques très forts. Par exemple, le noyau ML possède la propriété de paramétricité. Un tel résultat, qui se déduit directement de son système de typage garantit par exemple que la seule fonction de type ∀ α. αarα est l’identité. Les propriétés de paramétricité sont intéressantes pour l’optimisation des programmes qui manipules des structures de données. Ils valident certaines transformation sur les programmes qui permettent d’éliminer la construction de données intermédiares.

Pour en savoir plus

Nous nous contentons ici de donner des ouvrages de référence. Un ouvrage incontournable sur le λ-calcul [?].