Quelle est la différence entre le polymorphisme de ligne et le typage structurel ?

Question

Les définitions sur lesquelles je suis tombé semblent indiquer qu'elles expriment la même idée.Cela signifie que la relation entre les types d'enregistrements est déterminée par leurs champs (ou propriétés) plutôt que par leurs noms.Leurs pages Wikipédia semblent également indiquer la même idée :

UN système de type structurel (ou système de types basé sur des propriétés) est une classe majeure de système de types dans laquelle la compatibilité et l'équivalence des types sont déterminées par la structure ou la définition réelle du type et non par d'autres caractéristiques telles que son nom ou son lieu de déclaration.

Dans la théorie des types de langage de programmation, polymorphisme de ligne est une sorte de polymorphisme qui permet d'écrire des programmes polymorphes sur des types de champs d'enregistrement (également appelés lignes, d'où polymorphisme de lignes).

Y a-t-il des différences entre eux ?

Answer 1

Les systèmes de type structurel n'ont pas nécessairement quelque chose à voir avec les enregistrements.Par exemple, vous pourriez avoir un système dans lequel :

data Bool = False | True
data Two = Zero | One

sont en fait du même type, car ce sont tous deux des types avec deux constructeurs nuls.Cela ne vous dit pas non plus grand-chose sur les enregistrements, car même si les types sont déterminés par leur structure, les deux enregistrements :

{s : S ; t : T}
{s : S ; t : T ; u : U}

ne sont pas la même structure, vous pouvez donc avoir un typage structurel sans que ces deux types aient quoi que ce soit de pratique.

De même, le polymorphisme des lignes isolément ne vous dit pas grand-chose --- juste que vous pouvez quantifier les lignes et les utiliser probablement avec, par exemple.un type d'enregistrement paramétré par une ligne.Mais il existe toutes sortes de variations sur ce que vous pouvez faire avec les lignes qui spécifient réellement les capacités du système.

Habituellement, avec les enregistrements structurels, les gens veulent au moins un sous-typage.Cela vous permet de dire que mon deuxième type d'enregistrement ci-dessus est un sous-type du premier, de sorte que vous pouvez transmettre ce dernier à tout ce qui attend le premier.Une manière typique de procéder avec le polymorphisme de lignes consiste à quantifier les champs supplémentaires qui peuvent être présents et à utiliser une sorte de concaténation de lignes.

Alors peut-être qu’une question plus ciblée est de savoir quelle est la différence entre le sous-typage et les quantificateurs.La réponse à cette question est généralement que le sous-typage ne peut exprimer des types quantifiés que si la variable quantifiée n’apparaît que de manière exclusivement covariante ou contravariante.On pourrait donc dire :

(forall a. a -> T) ~= Top -> T
(forall a. T -> a) ~= T -> Bot

Mais pour un type comme forall a. a -> a, il n'y a pas un seul type à choisir a sans perdre d'informations.

Cela s'étend aux systèmes avec juste enregistrer le sous-typage vs.(approprié) polymorphisme de ligne.Cependant, si vous disposez d’un système avec sous-typage et quantificateurs, et que le sous-typage peut s’appliquer aux types quantifiés, les différences peuvent alors être beaucoup plus subtiles.Cependant, avoir à la fois des quantificateurs et un sous-typage peut devenir assez délicat (le polymorphisme des lignes n'est pas non plus facile à maîtriser).