Qu'est-ce que existentielle type?

Quand quelqu'un définit un type universel ∀X qu'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) {
   ...
}

La copy fonction n'a aucune idée de ce que T sera réellement, mais il n'a pas besoin d'.

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. Le 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 de VirtualMachine.compile à VirtualMachine.run.

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

Mise à jour: 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 la VMWrapper appeler notre propre VMHandler qui est universellement tapé handle fonction. L'effet net est le même, notre code a pour traiter 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);
   }
}

Je pense que cela 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 peut 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) ce cette HaskellWiki article les états à être le principal effet de l'existentiel types:

Existentielle types peuvent être utilisé à plusieurs fins différentes. Mais ce qu'ils ne 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 set-up:

Au pseudo-code n'est pas tout à fait valable Java, même s'il serait assez facile de résoudre ce problème. 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...

• récursive de type Tree<α> qui représente un nœud dans un arbre binaire. Chaque nœud stocke une value de certains type de α et a des références à l'option left et right les sous-arbres du même type.

• une fonction height qui renvoie la distance la plus longue de toute feuille de nœud à nœud racine t.

Maintenant, passons au-dessus de pseudo-code pour height dans la 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 de la 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 à tous? 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 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 paramètre de type α.

En conséquence, vous ne pouvez plus consulter le type de t.value dans cette méthode, ni manipuler des expressions de ce type, car aucun identifiant n'a été lié à elle. (Le ? 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 lancer de 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   |                  
=====================+=====================================

Existentielle type est un type opaque.

Penser à 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 de lui. 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:

let exfile = fopen("foo.txt"); //No type for exfile!
read(exfile, buf, size);

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

Il existe un type de T tel que:

size_t read(T exfile, char* buf, size_t size);

La variable exfile n'est pas un int, pas un char*, 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.

Semble que je suis venue un peu en retard, mais de toute façon, ce document ajoute un autre point de vue de ce que existentielle types sont, bien que non spécifiquement indépendant de la langue, il devrait être assez facile à comprendre existentielle types: http://www.cs.uu.nl/groups/ST/Projects/ehc/ehc-book.pdf (chapitre 8)

La différence entre un universellement et existentiellement quantifiés type peut être caractérisé par l'observation suivante:

• L'utilisation d'une valeur avec un ∀ quantifiés type détermine le type de choisir pour l'instanciation de l'quantifiés type de variable. Par exemple, l'appelant de la fonction identité “id :: ∀une.a → a” détermine le type d'opter pour le type de la variable a pour cette application particulière de l'id. Pour l'application de fonction “id 3” ce type est égal à Int.

• La création d'une valeur avec un d rond quantifiés type détermine, et les peaux, le type de la quantifiés type de variable. Par exemple, un créateur d'une “∃un.(a, a → Int)” peut avoir construit une valeur de ce type de “(3, λx → x)”; un autre créateur a construit une valeur avec le même type de “("x", λx → ord x)”. À partir d'un point de vue utilisateur, les deux valeurs ont le même type et sont donc interchangeables. La valeur a un type spécifique choisie pour la variable de type a, mais nous ne savons pas de quel type, de sorte que cette information ne peut plus être exploité. Cette valeur type spécifique de l'information a été "oubliée"; nous savons seulement qu'elle existe.

La recherche sur les types de données abstraits et se cacher de l'information a apporté existentielle types dans les langages de programmation. Fabrication d'un type de données abstrait se cache info à propos de ce type, de sorte qu'un client de ce type ne peut pas en abuser. Disons que vous avez une référence à un objet... certaines langues, vous permettent de jeter qu'un renvoi à une référence d'octets et de faire ce que vous voulez à ce morceau de mémoire. Aux fins de garantir le comportement d'un programme, il est utile pour un langage pour faire valoir ce que de vous d'agir uniquement sur la référence à l'objet via les méthodes le concepteur de l'objet fournit. Vous savez le type existe, mais rien de plus.

Voir:

Résumé des Types Existentiels Type, MITCHEL & PLOTKIN

http://theory.stanford.edu/~jcm/documents/mitch-plotkin-88.pdf

Que je comprends que c'est une des mathématiques pour décrire des interfaces/classe abstraite.

Que pour T = ∃X { X; int f(X); }

Pour C# il serait traduit en une générique de type abstrait:

abstract class MyType<T>{
    private T a;

    public abstract int f(T x);
}

"Existentielle" signifie simplement qu'il y a un type qui obéissent aux règles définies ici.