Type de raffinement - Refinement type

Dans la théorie des types , un type raffiné est un type doté d'un prédicat qui est supposé être valable pour tout élément du type raffiné. Les types de raffinement peuvent exprimer des conditions préalables lorsqu'ils sont utilisés comme arguments de fonction ou postconditions lorsqu'ils sont utilisés comme types de retour : par exemple, le type d'une fonction qui accepte des nombres naturels et renvoie des nombres naturels supérieurs à 5 peut s'écrire . Les types de raffinement sont donc liés au sous-typage comportemental . ${\ displaystyle f: \ mathbb {N} \ rightarrow \ {n \ in \ mathbb {N} \, | \, n> 5 \}}$

L'histoire

Le concept de types de raffinement a été introduit pour la première fois dans les types de raffinement pour ML de Freeman et Pfenning en 1991 , qui présentent un système de types pour un sous-ensemble de ML standard . Le système de type "préserve la décidabilité de l'inférence de type de ML" tout en "permettant toujours de détecter plus d'erreurs au moment de la compilation". Plus récemment, des systèmes de type raffinement ont été développés pour des langages tels que Haskell , TypeScript et Scala .

Voir également

• Liquide Haskell
• Types dépendants

Références

${\ displaystyle \ Gamma \ vdash x: {\ text {Int}}}$

Cet article sur la théorie du langage de programmation ou la théorie des types est un bout . Vous pouvez aider Wikipedia en le développant . v t e