Qu'est-ce qu'un type existentiel?

J'ai lu l'article de Wikipédia Types existentiels . J'ai compris qu'ils sont appelés types existentiels à cause de l'opérateur existentiel (∃). Je ne sais pas trop à quoi ça sert. Quelle est la différence entre

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

et

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

?

Quand quelqu'un définit un type universel, ∀Xil dit: vous pouvez brancher le type que vous voulez, je n'ai pas besoin de savoir quoi que ce soit sur le type pour faire mon travail, je vais seulement y faire référence de manière opaqueX .

Quand quelqu'un définit un type existentiel, ∃Xil dit: j'utiliserai le type que je veux ici; vous ne saurez rien sur le type, vous ne pouvez donc vous y référer que de manière opaqueX .

Les types universels vous permettent d'écrire des choses comme:

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

La copyfonction n'a aucune idée de ce qui Tsera réellement, mais elle n'en a pas besoin.

Les types existentiels vous permettraient 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 implémentation de machine virtuelle dans la liste peut avoir un type de bytecode différent. La runAllCompilersfonction n'a aucune idée de ce qu'est le type de bytecode, mais elle n'en a pas besoin; il ne fait que relayer le bytecode de VirtualMachine.compileà VirtualMachine.run.

Les jokers de type Java (ex:) List<?>sont une forme très limitée de types existentiels.

Mise à jour: j'ai oublié de mentionner que vous pouvez en quelque sorte simuler des types existentiels avec des types universels. Tout d'abord, enveloppez votre type universel pour masquer le paramètre de type. Deuxièmement, inverser le contrôle (cela permute effectivement la partie «vous» et «je» 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 VMWrappernotre propre appel VMHandlerqui a une handlefonction universellement typée . L'effet net est le même, notre code doit être traité Bcomme 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 d'implémentation de VM:

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);
   }
}

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

Notez que cette vue mélange les types et les valeurs. La preuve existentielle est un type et une valeur. La preuve universelle est une famille entière de valeurs indexées par type (ou un mappage des types aux valeurs).

La différence entre les deux types que vous avez spécifiés est donc la suivante:

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

Cela signifie: Une valeur de type Tcontient un type appelé X, une valeur a:Xet une fonction f:X->int. Un producteur de valeurs de type Tpeut choisir n'importe quel type pour Xet un consommateur ne peut rien savoir X. Sauf qu'il y a un exemple de celui-ci appelé aet que cette valeur peut être transformée en un inten le donnant à f. En d'autres termes, une valeur de type Tsait comment produire un en intquelque sorte. Eh bien, nous pourrions éliminer le type intermédiaire Xet dire simplement:

T = int

Celui universellement quantifié est un peu différent.

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

Cela signifie: Une valeur de type Tpeut recevoir n'importe quel type X, et elle produira une valeur a:Xet une fonction f:X->int quoi qu'il en Xsoit . En d'autres termes: un consommateur de valeurs de type Tpeut choisir n'importe quel type pour X. Et un producteur de valeurs de type Tne peut rien savoir du tout X, mais il doit être capable de produire une valeur apour n'importe quel choix de X, et être capable de transformer une telle valeur en un int.

De toute évidence, l'implémentation de ce type est impossible, car aucun programme ne peut produire une valeur de tous les types imaginables. Sauf si vous autorisez des absurdités comme nullou des bas.

Puisqu'un existentiel est une paire, un argument existentiel peut être converti en un argument universel par currying .

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

est le même que:

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

Le premier est un existentiel de rang 2 . Cela conduit à la propriété utile suivante:

Chaque type de rang quantifié existentiellement n+1est un type de rang universellement quantifié n.

Il existe un algorithme standard pour transformer les existentiels en universaux, appelé Skolémisation .

Je pense qu'il est logique d'expliquer les types existentiels avec les types universels, puisque les deux concepts sont complémentaires, c'est-à-dire que l'un est «l'opposé» de l'autre.

Je ne peux pas répondre à tous les détails sur les types existentiels (comme donner une définition exacte, lister toutes les utilisations possibles, leur relation avec les types de données abstraits, etc.) parce que je ne suis tout simplement pas assez informé pour cela. Je vais démontrer seulement (en utilisant Java) ce que cet article HaskellWiki déclare être le principal effet des types existentiels:

Les types existentiels peuvent être utilisés à plusieurs fins différentes. Mais ce qu'ils font est de «cacher» une variable de type sur le côté droit. Normalement, toute variable de type apparaissant à droite doit également apparaître à gauche […]

Exemple de configuration:

Le pseudo-code suivant n'est pas tout à fait valide 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 vous l'expliquer brièvement. Nous définissons…

• un type récursif Tree<α>qui représente un nœud dans un arbre binaire. Chaque nœud stocke a d'un valuecertain type α et a des références à des sous left- rightarborescences optionnelles et du même type.

• une fonction heightqui renvoie la distance la plus éloignée de tout nœud feuille au nœud racine t.

Maintenant, transformons le pseudo-code ci-dessus pour heighten une syntaxe Java appropriée! (Je continuerai à omettre certaines règles standard pour des raisons de brièveté, telles que l'orientation des objets et les modificateurs d'accessibilité.) Je vais montrer deux solutions possibles.

1. Solution de type universel:

La solution la plus évidente consiste simplement à rendre heightgé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 permettrait de déclarer des variables et de créer des expressions de type α à l' intérieur de cette fonction, si vous le souhaitez. Mais...

2. Solution de type existentiel:

Si vous regardez le corps de notre méthode, vous remarquerez que nous n'accédons pas ou ne travaillons pas avec quoi que ce soit de type α ! Il n'y a aucune expression ayant ce type, ni aucune variable déclarée avec ce type ... alors, pourquoi devons-nous rendre heightgénérique du tout? Pourquoi ne pouvons-nous pas simplement oublier α ? Il s'avère que nous pouvons:

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

Comme je l'ai écrit au tout début de cette réponse, les types existentiels et universels sont de nature complémentaire / double. Ainsi, si la solution de type universel devait rendre height plus générique, alors nous devrions nous attendre à ce que les types existentiels aient l'effet inverse: la rendre moins générique, à savoir en masquant / supprimant le paramètre de type α .

Par conséquent, vous ne pouvez plus faire référence au type de t.valuedans cette méthode ni manipuler aucune expression de ce type, car aucun identificateur ne lui est lié. (Le ?joker est un jeton spécial, pas un identifiant qui "capture" un type.) t.valueEst effectivement devenu opaque; peut-être que la seule chose que vous pouvez encore faire est de le convertir en caractères 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   |                  
=====================+=====================================

Ce sont tous de bons exemples, mais je choisis d'y répondre un peu différemment. Rappelez-vous des maths, que ∀x. P (x) signifie "pour tous les x, je peux prouver que P (x)". En d'autres termes, c'est une sorte de fonction, vous me donnez un x et j'ai une méthode pour vous le prouver.

En théorie des types, nous ne parlons pas de preuves, mais de types. Donc, dans cet espace, nous voulons dire "pour tout type X que vous me donnez, je vais vous donner un type P spécifique". Maintenant, puisque nous ne donnons pas beaucoup d'informations à P sur X en plus du fait qu'il s'agit d'un type, P ne peut pas faire grand-chose avec lui, 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ù Nil est le type des pointeurs nuls. Nous pouvons faire une liste de ce: List<X> = (X, List<X>) | Nil. Notez que le dernier est récursif, les valeurs de List<X>sont soit des paires où le premier élément est un X et le deuxième élément est un List<X>soit un pointeur nul.

Maintenant, en maths ∃x. P (x) signifie "Je peux prouver qu'il existe un x particulier tel que P (x) est vrai". Il peut y avoir beaucoup de tels x, mais pour le prouver, un seul suffit. Une autre façon de penser est qu'il doit exister un ensemble non vide de paires de preuves et de preuves {(x, P (x))}.

Traduit en théorie des types: un type de la famille ∃X.P<X>est un type X et un type correspondant P<X>. Notez qu'avant, nous avons donné X à P, (de sorte que nous savions tout sur X mais très peu de P) que le contraire est vrai maintenant. P<X>ne promet pas de donner des informations sur X, juste qu'il y en a une, et que c'est bien un type.

En quoi est-ce utile? Eh bien, P pourrait être un type qui a un moyen d'exposer son type interne X. Un exemple serait un objet qui cache la représentation interne de son état X. Bien que nous n'ayons aucun moyen de le manipuler directement, nous pouvons observer son effet en piquer à P. Il pourrait y avoir de nombreuses implémentations de ce type, mais vous pouvez utiliser tous ces types, quel que soit celui qui a été choisi.

Pour répondre directement à votre question:

Avec le type universel, les utilisations de Tdoivent inclure le paramètre type X. Par exemple T<String>ou T<Integer>. Pour les utilisations de type existentiel de Tn'incluez pas ce paramètre de type car il est inconnu ou non pertinent - utilisez simplement T(ou en Java T<?>).

Informations complémentaires:

Les types universels / abstraits et les types existentiels sont une dualité de perspective entre le consommateur / client d'un objet / fonction et le producteur / implémentation de celui-ci. Lorsqu'un côté voit un type universel, l'autre voit un type existentiel.

En Java, vous pouvez définir une classe générique:

public class MyClass<T> {
   // T is existential in here
   T whatever; 
   public MyClass(T w) { this.whatever = w; }

   public static MyClass<?> secretMessage() { return new MyClass("bazzlebleeb"); }
}

// T is universal from out here
MyClass<String> mc1 = new MyClass("foo");
MyClass<Integer> mc2 = new MyClass(123);
MyClass<?> mc3 = MyClass.secretMessage();

• Du point de vue d'un client de MyClass, Test universel car vous pouvez remplacer n'importe quel type Tlorsque vous utilisez cette classe et vous devez connaître le type réel de T chaque fois que vous utilisez une instance deMyClass
• Du point de vue des méthodes d'instance en MyClasssoi, Test existentielle car elle ne connaît pas le type réel deT
• En Java, ?représente le type existentiel - donc lorsque vous êtes à l'intérieur de la classe,T c'est fondamentalement ?. Si vous souhaitez gérer une instance de MyClasswith Texistential, vous pouvez déclarer MyClass<?>comme dans l' secretMessage()exemple ci-dessus.

Les types existentiels sont parfois utilisés pour masquer les détails d'implémentation de quelque chose, comme indiqué ailleurs. Une version Java de ceci pourrait ressembler à:

public class ToDraw<T> {
    T obj;
    Function<Pair<T,Graphics>, Void> draw;
    ToDraw(T obj, Function<Pair<T,Graphics>, Void>
    static void draw(ToDraw<?> d, Graphics g) { d.draw.apply(new Pair(d.obj, g)); }
}

// Now you can put these in a list and draw them like so:
List<ToDraw<?>> drawList = ... ;
for(td in drawList) ToDraw.draw(td);

C'est un peu difficile de capturer cela correctement car je prétends être dans une sorte de langage de programmation fonctionnel, ce que Java n'est pas. Mais le point ici est que vous capturez une sorte d'état plus une liste de fonctions qui fonctionnent sur cet état et que vous ne connaissez pas le type réel de la partie d'état, mais les fonctions le font puisqu'elles étaient déjà associées à ce type .

Maintenant, en Java, tous les types non primitifs non finaux sont en partie existentiels. Cela peut sembler étrange, mais comme une variable déclarée comme Objectpourrait être une sous-classe de à la Objectplace, vous ne pouvez pas déclarer le type spécifique, uniquement "ce type ou une sous-classe". Ainsi, les objets sont représentés comme un bit d'état plus une liste de fonctions qui opèrent sur cet état - la fonction à appeler est déterminée au moment de l'exécution par recherche. Cela ressemble beaucoup à l'utilisation des types existentiels ci-dessus où vous avez une partie d'état existentiel et une fonction qui opère sur cet état.

Dans les langages de programmation à typage statique sans sous-typage ni casts, les types existentiels permettent de gérer des listes d'objets typés différemment. Une liste de T<Int>ne peut pas contenir de T<Long>. Cependant, une liste deT<?> peut contenir n'importe quelle variante de T, ce qui permet de mettre de nombreux types de données différents dans la liste et de les convertir tous en un entier (ou d'effectuer toutes les opérations fournies dans la structure de données) à la demande.

On peut presque toujours convertir un enregistrement avec un type existentiel en un enregistrement sans utiliser de fermetures. Une fermeture est également typée de manière existentielle, en ce que les variables libres sur lesquelles elle est fermée sont masquées à l'appelant. Ainsi, un langage qui prend en charge les fermetures mais pas les types existentiels peut vous permettre de faire des fermetures qui partagent le même état caché que vous auriez mis dans la partie existentielle d'un objet.

Un type existentiel est un type opaque.

Pensez à un descripteur de fichier sous Unix. Vous savez que son type est int, vous pouvez donc le forger facilement. Vous pouvez, par exemple, essayer de lire à partir du handle 43. S'il se trouve que le programme a un fichier ouvert avec ce handle particulier, vous le lirez. Votre code ne doit pas nécessairement être malveillant, juste bâclé (par exemple, le handle peut être une variable non initialisée).

Un type existentiel est caché de votre programme. Si fopenun type existentiel est renvoyé, tout ce que vous pouvez faire est de l'utiliser avec certaines fonctions de bibliothèque qui acceptent ce type existentiel. Par exemple, le pseudo-code suivant compilerait:

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

L'interface "lecture" est déclarée comme:

Il existe un type T tel que:

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

La variable exfile n'est pas un int, pas a char*, pas un fichier struct - rien que vous puissiez exprimer dans le système de types. 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 laissera pas.

Il semble que j'arrive un peu en retard, mais de toute façon, ce document ajoute une autre vision de ce que sont les types existentiels, bien que pas spécifiquement indépendant du langage, il devrait alors être assez facile de comprendre les types existentiels: http: //www.cs.uu .nl / groups / ST / Projects / ehc / ehc-book.pdf (chapitre 8)

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

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

• La création d'une valeur avec un type quantifié ∃ détermine et masque le type de la variable de type quantifié. Par exemple, un créateur d'un «∃a. (A, a → Int)» peut avoir construit une valeur de ce type à partir de «(3, λx → x)»; un autre créateur a construit une valeur du même type à partir de «('x', λx → ord x)». Du point de vue des utilisateurs, les deux valeurs ont le même type et sont donc interchangeables. La valeur a un type spécifique choisi pour la variable de type a, mais nous ne savons pas quel type, donc cette information ne peut plus être exploitée. Cette information de type spécifique à une valeur a été «oubliée»; nous savons seulement qu'il existe.

Un type universel existe pour toutes les valeurs du ou des paramètres de type. Un type existentiel n'existe que pour les valeurs du ou des paramètres de type qui satisfont les contraintes de type existentiel.

Par exemple, dans Scala, une façon d'exprimer un type existentiel est un type abstrait qui est contraint à des limites supérieures ou inférieures.

trait Existential {
  type Parameter <: Interface
}

De manière équivalente, un type universel contraint est un type existentiel comme dans l'exemple suivant.

trait Existential[Parameter <: Interface]

Tout site d'utilisation peut utiliser le Interfacecar tout sous-type instanciable de Existentialdoit définir letype Parameter qui doit implémenter le Interface.

Un cas dégénéré d'un type existentiel dans Scala est un type abstrait auquel on ne fait jamais référence et qui n'a donc pas besoin d'être défini par un sous-type. Cela a effectivement une notation abrégée List[_] en Scala et List<?>en Java.

Ma réponse a été inspirée par la proposition de Martin Odersky d'unifier les types abstraits et existentiels. La diapositive d'accompagnement facilite la compréhension.

La recherche sur les types de données abstraits et le masquage d'informations a introduit des types existentiels dans les langages de programmation. La création d'un résumé de type de données masque les informations sur ce type, de sorte qu'un client de ce type ne peut pas en abuser. Supposons que vous ayez une référence à un objet ... certains langages vous permettent de convertir cette référence en une référence en octets et de faire tout ce que vous voulez sur cet élément de mémoire. Dans le but de garantir le comportement d'un programme, il est utile qu'un langage impose que vous n'agissiez que sur la référence à l'objet via les méthodes fournies par le concepteur de l'objet. Vous savez que le type existe, mais rien de plus.

Voir:

Les types abstraits ont un type existentiel, MITCHEL et PLOTKIN

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

J'ai créé ce diagramme. Je ne sais pas si c'est rigoureux. Mais si ça aide, je suis content.

Si je comprends bien, c'est une manière mathématique de décrire les interfaces / la classe abstraite.

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

Pour C #, cela se traduirait par un type abstrait générique:

abstract class MyType<T>{
    private T a;

    public abstract int f(T x);
}

«Existentiel» signifie simplement qu'il existe un type qui obéit aux règles définies ici.