Préservation des types

Cet article est orphelin. Moins de trois articles lui sont liés (octobre 2025).

Vous pouvez aider en ajoutant des liens vers [[Préservation des types]] dans les articles relatifs au sujet.

En théorie des types, on dit d'un système de types qu'il possède la propriété de préservation des types (en anglais type preservation ou subject reduction) si l'évaluation des expressions n'entraîne aucun changement de type.

Formellement, pour un contexte de typage ${\displaystyle \Gamma }$, deux expressions ${\displaystyle e_{1}}$ et ${\displaystyle e_{2}}$ et un type ${\displaystyle \tau }$, si ${\displaystyle \Gamma \vdash e_{1}:\tau }$ et ${\displaystyle e_{1}\longrightarrow e_{2}}$ alors ${\displaystyle \Gamma \vdash e_{2}:\tau }$.

Autrement dit, si, sous le contexte ${\displaystyle \Gamma }$, ${\displaystyle e_{1}}$ est de type ${\displaystyle \tau }$ et se réduit en ${\displaystyle e_{2}}$, alors ${\displaystyle e_{2}}$ est également de type ${\displaystyle \tau }$ sous le même contexte.

Intuitivement, cette propriété indique qu'il n'est pas possible d'écrire d'expression dans un type donné (par exemple int) et d'obtenir une valeur de type différent (par exemple string) après évaluation

Avec la propriété de progrès, il s’agit d’une propriété fondamentale qu'un système doit vérifier pour établir la sûreté de ses types (en anglais type soundness).

La propriété duale d'expansion du typage s'exprime formellement ainsi : si ${\displaystyle \Gamma \vdash e_{2}:\tau }$ et ${\displaystyle e_{1}\longrightarrow e_{2}}$ alors ${\displaystyle \Gamma \vdash e_{1}:\tau }$. Cette dernière se vérifie rarement car l'évaluation peut effacer les sous-termes mal typés d'une expression et en produire une correctement typée.