Polymorphisme paramétrique - Parametric polymorphism

Polymorphisme
Polymorphisme ad hoc
Surcharge de fonction Surcharge de l'opérateur
Polymorphisme paramétrique
Fonction générique Programmation générique
Sous-typage
Fonction virtuelle Envoi unique et dynamique Double expédition Envoi multiple Envoi de prédicat
v t e

Dans les langages de programmation et la théorie des types , le polymorphisme paramétrique est un moyen de rendre un langage plus expressif, tout en conservant une sécurité de type statique complète . En utilisant le polymorphisme paramétrique , une fonction ou un type de données peut être écrit de manière générique afin qu'il puisse gérer des valeurs de manière identique sans dépendre de leur type. Ces fonctions et types de données sont appelés respectivement fonctions génériques et types de données génériques et constituent la base de la programmation générique .

Par exemple, une fonction appendqui joint deux listes peut être construite de manière à ne pas se soucier du type d'éléments : elle peut ajouter des listes d' entiers , des listes de nombres réels , des listes de chaînes , etc. Laissez la variable de type a désigner le type d'éléments dans les listes. Puis appendpeut être tapé

forall a. [a] × [a] -> [a]

où [a]désigne le type de listes avec des éléments de type a . On dit que le type de appendest paramétré par a pour toutes les valeurs de a . (Notez que puisqu'il n'y a qu'une seule variable de type, la fonction ne peut pas être appliquée à n'importe quel couple de listes : le couple, ainsi que la liste résultat, doivent être constitués du même type d'éléments) Pour chaque endroit où appendest appliqué, un la valeur est décidée pour un .

À la suite de Christopher Strachey , le polymorphisme paramétrique peut être opposé au polymorphisme ad hoc , dans lequel une seule fonction polymorphe peut avoir un certain nombre d'implémentations distinctes et potentiellement hétérogènes selon le type d'argument(s) auquel elle est appliquée. Ainsi, le polymorphisme ad hoc ne peut généralement prendre en charge qu'un nombre limité de ces types distincts, puisqu'une implémentation distincte doit être fournie pour chaque type.

Histoire

Le polymorphisme paramétrique a été introduit pour la première fois dans les langages de programmation en ML en 1975. Aujourd'hui, il existe en Standard ML , OCaml , F# , Ada , Haskell , Mercury , Visual Prolog , Scala , Julia , Python , TypeScript , C++ et autres. Java , C# , Visual Basic .NET et Delphi ont chacun introduit des "génériques" pour le polymorphisme paramétrique. Certaines implémentations du polymorphisme de type sont superficiellement similaires au polymorphisme paramétrique tout en introduisant également des aspects ad hoc. Un exemple est la spécialisation de modèle C++ .

La forme la plus générale de polymorphisme est le « polymorphisme imprédicatif de rang supérieur ». Deux restrictions populaires de cette forme sont le polymorphisme de rang restreint (par exemple, le polymorphisme de rang 1 ou prenex ) et le polymorphisme prédicatif. Ensemble, ces restrictions donnent un « polymorphisme prédicatif prédictif », qui est essentiellement la forme de polymorphisme trouvé dans ML et les premières versions de Haskell.

Polymorphisme de rang supérieur

Polymorphisme de rang 1 (prénéx)

Dans un système polymorphe prenex , les variables de type ne peuvent pas être instanciées avec des types polymorphes. Ceci est très similaire à ce que l'on appelle le "style ML" ou le "Let-polymorphism" (techniquement, le Let-polymorphism de ML a quelques autres restrictions syntaxiques). Cette restriction rend la distinction entre les types polymorphes et non polymorphes très importante ; ainsi, dans les systèmes prédicatifs, les types polymorphes sont parfois appelés schémas de types pour les distinguer des types ordinaires (monomorphes), parfois appelés monotypes . Une conséquence est que tous les types peuvent être écrits sous une forme qui place tous les quantificateurs à la position la plus externe (prenex). Par exemple, considérons la appendfonction décrite ci-dessus, qui a le type

forall a. [a] × [a] -> [a]

Afin d'appliquer cette fonction à une paire de listes, un type doit être substitué à la variable a dans le type de la fonction de telle sorte que le type des arguments corresponde au type de fonction résultant. Dans un système imprédicatif , le type à substituer peut être n'importe quel type, y compris un type lui-même polymorphe ; appendpeut donc être appliqué à des paires de listes avec des éléments de n'importe quel type, même à des listes de fonctions polymorphes comme appendelle-même. Le polymorphisme dans le langage ML est prédicatif. En effet, la prédicativité, avec d'autres restrictions, rend le système de types suffisamment simple pour que l' inférence de type complète soit toujours possible.

À titre d'exemple pratique, OCaml (un descendant ou dialecte de ML ) effectue une inférence de type et prend en charge le polymorphisme imprédicatif, mais dans certains cas, lorsque le polymorphisme imprédicatif est utilisé, l'inférence de type du système est incomplète à moins que des annotations de type explicites ne soient fournies par le programmeur.

Rank- k polymorphisme

Pour une valeur fixe k , le polymorphisme de rang- k est un système dans lequel un quantificateur peut ne pas apparaître à gauche de k ou plusieurs flèches (lorsque le type est dessiné comme un arbre).

L'inférence de type pour le polymorphisme de rang 2 est décidable, mais la reconstruction pour le rang 3 et supérieur ne l'est pas.

Polymorphisme de rang n (« rang supérieur »)

Le polymorphisme de rang n est un polymorphisme dans lequel des quantificateurs peuvent apparaître à gauche d'un nombre arbitraire de flèches.

Prédicativité et imprédicativité

Polymorphisme prédicatif

Dans un système polymorphe paramétrique prédicatif, un type contenant une variable de type ne peut pas être utilisé de manière à être instancié en un type polymorphe. Les théories des types prédicatives incluent la théorie des types de Martin-Löf et NuPRL . ${\style d'affichage \tau }$${\style d'affichage \alpha }$${\style d'affichage \alpha }$

Polymorphisme imprédicatif

Le polymorphisme imprédicatif (également appelé polymorphisme de première classe ) est la forme la plus puissante de polymorphisme paramétrique. Une définition est dite imprédicative si elle est autoréférentielle ; en théorie des types, cela permet l'instanciation d'une variable dans un type avec n'importe quel type, y compris les types polymorphes, comme lui-même. Un exemple de ceci est le System F avec la variable de type X dans le type , où X pourrait même faire référence à T lui-même. ${\style d'affichage \tau }$${\style d'affichage \tau }$${\displaystyle T=\pourtout XX\à X}$

En théorie des types , les -calculs typés imprédicatifs les plus fréquemment étudiés sont basés sur ceux du cube lambda , en particulier le Système F .

Polymorphisme paramétrique borné

En 1985, Luca Cardelli et Peter Wegner ont reconnu les avantages de permettre des limites sur les paramètres de type. De nombreuses opérations nécessitent une certaine connaissance des types de données, mais peuvent sinon fonctionner de manière paramétrique. Par exemple, pour vérifier si un élément est inclus dans une liste, nous devons comparer les éléments pour l'égalité. Dans Standard ML , les paramètres de type de la forme ''a sont restreints afin que l'opération d'égalité soit disponible, ainsi la fonction aurait le type ''a × ''a list → bool et ''a ne peut être qu'un type avec défini égalité. En Haskell , la délimitation est obtenue en exigeant que les types appartiennent à une classe de types ; ainsi la même fonction a le type en Haskell. Dans la plupart des langages de programmation orientés objet qui prennent en charge le polymorphisme paramétrique, les paramètres peuvent être contraints à être des sous - types d'un type donné (voir Polymorphisme de sous - type et l'article sur la programmation générique ). ${\displaystyle {\scriptstyle Eq\,\alpha \,\Rightarrow \alpha \,\rightarrow \left[\alpha \right]\rightarrow Bool}}$

Voir également

• Paramétrisation
• Récursion polymorphe
• Type class#Polymorphisme de type supérieur

Remarques

Les références

• Strachey, Christopher (1967), Concepts fondamentaux des langages de programmation (notes de cours), Copenhague : École d'été internationale en programmation informatique. Republié dans : Strachey, Christopher (2000). Calcul d'ordre supérieur et symbolique . 13 : 11–49. doi : 10.1023/A:1010000313106 . Manquant ou vide |title=( aide )
• Hindley, J. Roger (1969), "The principal type schema of an object in combinatory logic", Transactions of the American Mathematical Society , 146 : 29-60, doi : 10.2307/1995158 , JSTOR  1995158 , MR  0253905.
• Girard, Jean-Yves (1971). "Une Extension de l'Interprétation de Gödel à l'Analyse, et son Application à l'Élimination des Coupures dans l'Analyse et la Théorie des Types". Actes du deuxième Symposium sur la logique scandinave (en français). Amsterdam. p. 63-92. doi : 10.1016/S0049-237X(08)70843-7 .
• Girard, Jean-Yves (1972), Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur , Université Paris 7.
• Reynolds, John C. (1974), "Towards a Theory of Type Structure", Colloque Sur la Programmation , Lecture Notes in Computer Science , Paris, 19 : 408-425, doi : 10.1007/3-540-06859-7_148 , ISBN 978-3-540-06859-4.
• Milner, Robin (1978). « Une théorie du polymorphisme de type en programmation » (PDF) . Journal des sciences de l'informatique et des systèmes . 17 (3) : 348-375. doi : 10.1016/0022-0000(78)90014-4 .
• Cardelli, Luca ; Wegner, Peter (décembre 1985). « Sur la compréhension des types, l'abstraction des données et le polymorphisme » (PDF) . Enquêtes informatiques ACM . 17 (4) : 471-523. CiteSeerX  10.1.1.117.695 . doi : 10.1145/6041.6042 . ISSN  0360-0300 .
• Pierce, Benjamin C. (2002). Types et langages de programmation . Presse MIT. ISBN 978-0-262-16209-8.