Des doutes sur le comportement de Type d'Unité dans un système de type

Question

J'ai un doute sur le Type de l'Unité dans le contexte de la Théorie des types et de son utilisation dans les différents scénarios.

Pour commencer, un Type D'Unité peut être vu comme un nullary Type de Produit, à savoir l'Unité, avec une seule valeur à terme qui est le tuple vide, ().Aussi, il existe un unique carte à partir de n'importe quel type de l'Unité.

Maintenant, il arrive que l'utilisation de l'Unité Type va au-delà de ces trivial définition, et est en fait utilisé dans la définition de Types de Données Algébriques, qui sont des Sommes de Types de Produits.Plus précisément, il est possible de représenter le concept d'un Type Énuméré à l'aide d'une Somme de Types d'Unité, par ex.dans StandardML nous pourrions avoir:

datatype suit = HEARTS | CLUBS | DIAMONDS | SPADES

où les CŒURS, trèfles, carreaux et les PIQUES sont nullary Types de Produits et, par conséquent, tous les isomorphe à l'Unité.

Mon doute est le suivant:s'il existe un seul élément de l'Unité, de quelle façon le système de type de distinguer entre les quatre différentes instances utilisées dans le Type de Somme ci-dessus (cinq cas, si l'on considère également le tuple vide...)?Je comprends qu'ils peuvent être considérés comme égaux les uns aux autres jusqu'à isomorphisme, mais ils sont extensionally différents et en fait, même en considérant uniquement la suit nous sommes censés faire correspondre à un modèle sur eux...

Answer 1

La réponse courte est que isomorphe types ne sont pas égaux, en dépit de se comporter de manière identique, et donc le système de type de pouvoir les distinguer.Dans un nominal type de système, comme celui que vous décrivez, les types sont essentiellement identifiés par leurs noms, même si elles sont structurellement équivalents.C'est le cas pour les cinq types d'unités que vous décrivez:ils sont structurellement équivalents, mais nominalement l'inégalité, et donc ils sont considérés comme distincts.

Notez que le pattern matching aspect est orthogonal:vous pouvez penser à de la cinq types d'unités existant dans l'isolement.Dans la plupart des type de théories, vous pouvez prendre la somme de deux types, même deux qui sont (théoriquement) l'égalité, par exemple Unit + Unit.Vous serez toujours tenus à motif, et disposera de deux cas:la gauche Unit et le droit Unit.La valeur nominale aspect est sans importance, bien que de nombreux langages de programmation permettra d'utiliser les noms de distinguer les différents cas de ce genre, au lieu de l'indice de la additionnées (en particulier, dans les langues où vous êtes seulement autorisé à prendre des sommes distinctes nominale types de Standard ML).