Ce qui est un type existentiels ?

Question

Je lis l'article Wikipédia des types existentiels . J'ai compris qu'ils sont appelés types existentiels à cause de l'opérateur existentiel (∃). Je ne suis pas sûr du but, cependant. Quelle est la différence entre

 T = ∃X { X a; int f(X); }
 

et

 T = ∀x { X a; int f(X); }
 

?

Answer 1

Quand quelqu'un définit un type universel ∀X , ils disent: vous pourrez Vous connecter quel que soit le type que vous voulez, je n'ai pas besoin de savoir quelque chose au sujet du type d'en faire mon métier, je ne vais le consulter de manière opaque comme X.

Quand quelqu'un définit existentielle type ∃X qu'ils disent: je vais l'utiliser quel que soit le type que je veux ici; vous ne savez rien sur le type, vous ne pouvez donc le consulter de manière opaque comme X.

Universelle types vous permettent d'écrire des choses comme:

void copy<T>(List<T> source, List<T> dest) {
   ...
}

L' copy fonction n'a aucune idée de ce qu' T sera réellement, mais il n'est pas nécessaire.

Existentielle types serait vous permettent d'écrire des choses comme:

interface VirtualMachine<B> {
   B compile(String source);
   void run(B bytecode);
}

// Now, if you had a list of VMs you wanted to run on the same input:
void runAllCompilers(List<∃B:VirtualMachine<B>> vms, String source) {
   for (∃B:VirtualMachine<B> vm : vms) {
      B bytecode = vm.compile(source);
      vm.run(bytecode);
   }
}

Chaque machine virtuelle de mise en œuvre de la liste peut avoir un avis différent du bytecode type. L' runAllCompilers fonction n'a aucune idée de ce que le pseudo-code de type est, mais il n'est pas nécessaire; il n'est de relayer le bytecode d' VirtualMachine.compile de VirtualMachine.run.

Java de type de caractères (ex: List<?>) sont très limitées forme existentielle types.

Mise à jour: j'ai Oublié de mentionner que vous pouvez sorte de simuler existentielle avec des types universels. Tout d'abord, l'enveloppe de votre type universel pour masquer le paramètre de type. Deuxièmement, inversion de contrôle (cela permet de swaps de le "vous" et "I" dans les définitions ci-dessus, qui est la principale différence entre existentiels et universels).

// A wrapper that hides the type parameter 'B'
interface VMWrapper {
   void unwrap(VMHandler handler);
}

// A callback (control inversion)
interface VMHandler {
   <B> void handle(VirtualMachine<B> vm);
}

Maintenant, nous pouvons avoir l' VMWrapper appelez notre propre VMHandler qui est universellement tapé handle fonction. L'effet net est le même, notre code a pour traiter l' B opaque.

void runWithAll(List<VMWrapper> vms, final String input)
{
   for (VMWrapper vm : vms) {
      vm.unwrap(new VMHandler() {
         public <B> void handle(VirtualMachine<B> vm) {
            B bytecode = vm.compile(input);
            vm.run(bytecode);
         }
      });
   }
}

Un exemple VM mise en œuvre:

class MyVM implements VirtualMachine<byte[]>, VMWrapper {
   public byte[] compile(String input) {
      return null; // TODO: somehow compile the input
   }
   public void run(byte[] bytecode) {
      // TODO: Somehow evaluate 'bytecode'
   }
   public void unwrap(VMHandler handler) {
      handler.handle(this);
   }
}

Answer 2

Une valeur existentielle type comme ∃x. F(x) est une paire contenant un certain type x et une valeur du type F(x). Tandis qu'une valeur d'un type polymorphe comme ∀x. F(x) est une fonction qui prend un certain type x et produit une valeur de type F(x). Dans les deux cas, le type de ferme sur un certain type constructeur F.

Notez que ce point de vue les mélanges de types et de valeurs. La preuve existentielle est un type et une valeur. L'universel de la preuve est toute une famille de valeurs indexées par type (ou d'une correspondance entre les types de valeurs).

Donc, la différence entre les deux types que vous avez spécifié est comme suit:

T = ∃X { X a; int f(X); }

Cela signifie: Une valeur de type T contient un type appelé' X, une valeur en a:X, et une fonction f:X->int. Un producteur de valeurs de type T fait le choix de tout type pour X et un consommateur ne peut pas savoir tout à propos de X. Sauf qu'il y a un exemple de ce qu'il appelle a et que cette valeur peut être transformée en une int en le donnant à f. En d'autres termes, une valeur de type T sait comment produire un int en quelque sorte. Eh bien, nous pourrions éliminer les intermédiaires de type X et de dire simplement:

T = int

Universellement quantifiée est un peu différent.

T = ∀X { X a; int f(X); }

Cela signifie: Une valeur de type T peut être donné à n'importe quel type X, et il va produire une valeur a:X, et une fonction f:X->int n'importe quel X est. En d'autres termes: un consommateur de valeurs de type T pouvez choisir n'importe quel type pour X. Et, un producteur de valeurs de type T ne peuvent pas savoir quoi que ce soit sur X, mais il doit être capable de produire une valeur a quelque soit le choix de l' X, et être en mesure de transformer cette valeur en int.

Évidemment, la mise en œuvre de ce type est impossible, car il n'existe pas de programme qui peut produire une valeur de tous les types imaginables. À moins que vous permettez à des absurdités comme null ou de fond.

Depuis existentielle est une paire, existentielle argument peut être converti en un universel via nourrissage.

(∃b. F(b)) -> Int

est le même que:

∀b. (F(b) -> Int)

Le premier est de rang 2 existentielle. Ceci conduit à considérer une propriété utile:

Chaque existentiellement quantifiés type de rang n+1 universellement quantifiée type de rang n.

Il existe un algorithme standard pour le tournage de existentiels dans des universaux, appelé Skolemization.

Answer 3

Je pense qu'il fait sens pour expliquer existentielle types avec universels, car les deux concepts sont complémentaires, c'est à dire l'un est la "face" de l'autre.

Je ne peux pas répondre à tous les détails à propos existentielle types (tels que de donner une définition exacte, la liste de toutes les utilisations possibles, leur relation avec les types de données abstraites, etc.) parce que je suis tout simplement pas suffisamment de connaissance pour que. Je vais démontrer (en utilisant Java) que ce HaskellWiki article les états à être le principal effet de l'existentiel types:

Existentielle types peuvent être utilisés à plusieurs fins. Mais ce qu'ils font est de "cacher" une variable de type sur le côté droit. Normalement, n'importe quel type de variable apparaissant sur le droit doit également apparaître sur la gauche [...]

Exemple:

Le pseudo-code n'est pas tout à fait valable Java, même s'il serait assez facile à corriger. En fait, c'est exactement ce que je vais faire dans cette réponse!

class Tree<α>
{
    α       value;
    Tree<α> left;
    Tree<α> right;
}

int height(Tree<α> t)
{
    return (t != null)  ?  1 + max( height(t.left), height(t.right) )
                        :  0;
}

Permettez-moi de sort pour vous. Nous sommes à la définition...

• un type récursif Tree<α> ce qui représente un nœud dans un arbre binaire. Chaque nœud stocke une value d'un certain type α et a des références à optionnel left et right sous-arbres du même type.

• une fonction height qui renvoie le plus à distance de n'importe quel nœud feuille à la racine le nœud t.

Maintenant, passons au-dessus de pseudo-code pour l' height bonne syntaxe Java! (Je vais continuer à omettre certains réutilisable par souci de concision, tels que l'orientation de l'objet et de l'accessibilité des modificateurs.) Je vais vous montrer deux solutions possibles.

1. Universal type de solution:

La plus évidente solution est de simplement faire height générique en introduisant le paramètre de type α dans sa signature:

<α> int height(Tree<α> t)
{
    return (t != null)  ?  1 + max( height(t.left), height(t.right) )
                        :  0;
}

Cela vous permettra de déclarer des variables et créer des expressions de type α à l'intérieur de cette fonction, si vous vouliez. Mais...

2. Existentielle type de solution:

Si vous regardez notre méthode, vous remarquerez que nous ne sommes pas réellement accès à, ou de travailler avec, quoi que ce soit de type α! Il n'y a pas des expressions du type, ni toutes les variables déclarées avec ce type... alors, pourquoi avons-nous les faire height générique? Pourquoi ne pouvons-nous pas tout simplement oublier α? Comme il s'avère, nous pouvons:

int height(Tree<?> t)
{
    return (t != null)  ?  1 + max( height(t.left), height(t.right) )
                        :  0;
}

Comme je l'ai écrit au début de cette réponse, existentiels et universels sont complémentaires / double dans la nature. Ainsi, si le type universel solution était de faire de height plus générique, alors nous devrions nous attendre que existentielle types ont l'effet inverse: c'est moins générique, à savoir en se cachant/retrait du type de paramètre α.

En conséquence, vous ne pouvez plus consulter le type d' t.value dans cette méthode, ni manipuler des expressions de ce type, car aucun identifiant n'a été lié à elle. ( ? Générique est un jeton spécial, pas un identificateur qui "capture" d'un type.) t.value est effectivement devenu opaque; peut-être la seule chose que vous pouvez toujours faire avec il est de type jette - Object.

Résumé:

===========================================================
                     |    universally       existentially
                     |  quantified type    quantified type
---------------------+-------------------------------------
 calling method      |                  
 needs to know       |        yes                no
 the type argument   |                 
---------------------+-------------------------------------
 called method       |                  
 can use / refer to  |        yes                no  
 the type argument   |                  
=====================+=====================================

Answer 4

Ce sont tous de bons exemples, mais je choisis de répondre un peu différemment. Rappel de mathématiques, que ∀x. P(x) signifie "pour tout x, je peux prouver que P(x)". En d'autres termes, c'est un genre de fonction, vous me donnez un x et j'ai une méthode pour le prouver pour vous.

En théorie des types, nous ne parlons pas de preuves, mais de types. Donc, dans cet espace, nous dire "pour tout type de X que vous me donnez, je vais vous donner un type spécifique P". Maintenant, puisque nous ne donnons pas de P beaucoup d'informations à propos de X, outre le fait que c'est un type, P ne peut pas faire grand chose avec elle, mais il y a quelques exemples. P peut créer le type de "toutes les paires du même type": P<X> = Pair<X, X> = (X, X). Ou nous pouvons créer le type d'option: P<X> = Option<X> = X | Nil, où le Néant est le type des pointeurs null. Nous pouvons faire une liste: List<X> = (X, List<X>) | Nil. Remarquez que le dernier est récursive, les valeurs de List<X> sont soit des couples dont le premier élément est un X et le second élément est une List<X> ou bien c'est un pointeur null.

Maintenant, en mathématiques ∃x. P(x) signifie "je peux prouver qu'il existe un x tel que P(x) est vraie". Il peut y avoir beaucoup de tels x, mais pour le prouver, un seul suffit. Une autre façon de penser, c'est qu'il doit exister un non-vide ensemble de la preuve et l'épreuve des paires {(x, P(x))}.

Traduit de théorie des types: Un type dans la famille ∃X.P<X> est un type de X et d'un type correspondant P<X>. Notez que si avant nous avons donné X P, (alors que l'on savait tout à propos de X, mais P très peu) que l'inverse est vrai maintenant. P<X> ne promets pas de donner toutes les informations à propos de X, c'est juste que là il y en a un, et que c'est en effet un type.

Comment est-ce utile? Eh bien, P pourrait être un type qui a une façon d'exposer son système interne de type X. Un exemple serait un objet qui cache la représentation interne de son état X. Si nous n'avons aucun moyen de manipuler directement, nous pouvons observer son effet en poussant à P. Il pourrait y avoir de nombreuses implémentations de ce type, mais vous pouvez utiliser tous ces types de n'importe qui, en particulier, a été choisi.

Answer 5

Existentielle type est un type opaque.

Pensez à un descripteur de fichier sous Unix. Vous savez, il est de type int, de sorte que vous pouvez facilement le forger. Vous pouvez, par exemple, tente de lire à partir de la poignée 43. Si il se trouve que le programme a un fichier ouvert avec cette poignée, vous pourrez lire. Votre code n'a pas à être malveillant, tout simplement bâclée (par exemple, la poignée peut être une variable non initialisée).

Existentielle type est caché de votre programme. Si fopen retourné existentielle type, tout ce que vous pouvez faire est de l'utiliser avec certaines fonctions de la bibliothèque qui acceptent ce existentielle type. Par exemple, le pseudo-code de la compilation:

laissez exfile = fopen("foo.txt"); // Pas de type pour exfile!
lire(exfile, buf, size);

L'interface "lu" est déclarée comme suit:

Il existe un type de T tel que:

size_t lire(T exfile, char* buf, size_t taille);

La variable exfile n'est pas un int, pas un char*, et non pas une structure de Fichier--rien que vous pouvez exprimer dans le système de type. Vous ne pouvez pas déclarer une variable dont le type est inconnu et vous ne pouvez pas convertir, par exemple, un pointeur dans ce type inconnu. La langue ne vous laisse pas.