Was ist ein existenzieller Typ?

Ich habe den Wikipedia-Artikel Existenzielle Typen gelesen . Ich habe festgestellt, dass sie aufgrund des existenziellen Operators (∃) als existenzielle Typen bezeichnet werden. Ich bin mir jedoch nicht sicher, worum es geht. Was ist der Unterschied zwischen

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

und

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

?

Wenn jemand einen universellen Typ definiert, ∀Xsagt er: Sie können jeden gewünschten Typ anschließen. Ich muss nichts über den Typ wissen, um meine Arbeit zu erledigen. Ich werde ihn nur undurchsichtig als bezeichnenX .

Wenn jemand einen existenziellen Typ definiert, ∃Xsagt er: Ich werde hier jeden Typ verwenden, den ich will; Sie wissen nichts über den Typ, daher können Sie ihn nur undurchsichtig als bezeichnenX .

Mit universellen Typen können Sie Dinge schreiben wie:

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

Die copyFunktion hat keine Ahnung, was Ttatsächlich sein wird, muss es aber nicht.

Mit existentiellen Typen können Sie Dinge schreiben wie:

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

Jede Implementierung einer virtuellen Maschine in der Liste kann einen anderen Bytecodetyp haben. Die runAllCompilersFunktion hat keine Ahnung, was der Bytecode-Typ ist, muss es aber nicht. Alles, was es tut, ist den Bytecode von VirtualMachine.compilebis weiterzuleiten VirtualMachine.run.

Java-Platzhalter (z. B. :) List<?>sind eine sehr begrenzte Form existenzieller Typen.

Update: Ich habe vergessen zu erwähnen, dass Sie existenzielle Typen mit universellen Typen simulieren können. Wickeln Sie zuerst Ihren universellen Typ ein, um den Typparameter auszublenden. Zweitens: Invertieren Sie die Kontrolle (dies vertauscht effektiv den Teil "Sie" und "Ich" in den obigen Definitionen, was den Hauptunterschied zwischen Existentialen und Universalien darstellt).

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

Jetzt können wir VMWrapperunseren eigenen Aufruf haben, der VMHandlereine universell typisierte handleFunktion hat. Der Nettoeffekt ist der gleiche, unser Code muss Bals undurchsichtig behandelt werden.

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

Ein Beispiel für eine VM-Implementierung:

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

Ein Wert eines existenziellen Typs wie ∃x. F(x) ist ein Paar, das einen Typ x und a enthält Wert des Typs enthält F(x). Während ein Wert einer polymorphen Typ wie ∀x. F(x)eine Funktion , die irgendeine Art nimmt xund erzeugt einen Wert des Typs F(x). In beiden Fällen wird der Typ über einen Typkonstruktor geschlossen F.

Beachten Sie, dass in dieser Ansicht Typen und Werte gemischt werden. Der existenzielle Beweis ist ein Typ und ein Wert. Der universelle Beweis ist eine ganze Familie von Werten, die nach Typ indiziert sind (oder eine Zuordnung von Typen zu Werten).

Der Unterschied zwischen den beiden von Ihnen angegebenen Typen ist also wie folgt:

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

Dies bedeutet: Ein Wert vom Typ Tenthält einen aufgerufenen Typ X, einen Wert a:Xund eine Funktion f:X->int. Ein Produzent von TTypwerten kann einen beliebigen Typ auswählen, Xund ein Verbraucher kann nichts darüber wissen X. Nur dass es ein Beispiel dafür gibt aund dass dieser Wert in einen Wert umgewandelt werden kann, intindem man ihn gibt f. Mit anderen Worten, ein Wert vom Typ Tweiß, wie man intirgendwie einen erzeugt. Nun, wir könnten den Zwischentyp eliminieren Xund einfach sagen:

T = int

Das universell quantifizierte ist etwas anders.

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

Dies bedeutet: Ein Wert vom Typ Tkann einem beliebigen Typ Xzugewiesen werden und erzeugt einen Wert a:Xund eine Funktion, f:X->int egal was Xist . Mit anderen Worten: Ein Verbraucher von Typwerten Tkann einen beliebigen Typ für auswählen X. Und ein Produzent von Typwerten Tkann überhaupt nichts wissen X, aber er muss in der Lage sein, einen Wert afür jede Wahl zu produzieren und einen Xsolchen Wert in einen zu verwandeln int.

Offensichtlich ist die Implementierung dieses Typs unmöglich, da es kein Programm gibt, das einen Wert für jeden erdenklichen Typ erzeugen kann. Es sei denn, Sie erlauben Absurditäten wie nulloder Bottoms.

Da ein Existenzial ein Paar ist, kann ein existenzielles Argument durch Currying in ein universelles umgewandelt werden .

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

ist das gleiche wie:

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

Ersteres ist ein existenzieller Rang 2 . Dies führt zu der folgenden nützlichen Eigenschaft:

Jeder existenziell quantifizierte Rangtyp n+1 ist ein universell quantifizierter Rangtyp n.

Es gibt einen Standardalgorithmus zur Umwandlung von Existentialen in Universalien namens Skolemisierung .

Ich denke, es ist sinnvoll, existenzielle Typen zusammen mit universellen Typen zu erklären, da die beiden Konzepte komplementär sind, dh das eine ist das "Gegenteil" des anderen.

Ich kann nicht jedes Detail über existenzielle Typen beantworten (z. B. eine genaue Definition geben, alle möglichen Verwendungen auflisten, ihre Beziehung zu abstrakten Datentypen usw.), weil ich dafür einfach nicht gut genug informiert bin. Ich werde nur (unter Verwendung von Java) zeigen, was dieser HaskellWiki-Artikel als Haupteffekt existenzieller Typen bezeichnet:

Existentielle Typen können werden verwendet für verschiedene Zwecke. Aber was sie tun ist zu ‚verstecken‘ eine Variable vom Typ auf der rechten Seite. Normalerweise muss jede rechts erscheinende Typvariable auch links erscheinen […]

Beispielaufbau:

Der folgende Pseudocode ist nicht ganz gültiges Java, obwohl es einfach genug wäre, dies zu beheben. Genau das werde ich in dieser Antwort tun!

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

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

Lassen Sie mich dies kurz für Sie darlegen. Wir definieren ...

• Ein rekursiver Typ, Tree<α>der einen Knoten in einem Binärbaum darstellt. Jeder Knoten speichert einen valueTyp α und verweist auf optionale leftund rightTeilbäume desselben Typs.

• Eine Funktion, heightdie den weitesten Abstand von einem Blattknoten zum Wurzelknoten zurückgibt t.

Lassen Sie uns nun den obigen Pseudocode für heightin die richtige Java-Syntax umwandeln ! (Ich werde der Kürze halber weiterhin einige Boilerplate weglassen, z. B. Modifikatoren für Objektorientierung und Barrierefreiheit.) Ich werde zwei mögliche Lösungen zeigen.

1. Universelle Lösung:

Die naheliegendste Lösung besteht darin, einfach heightgenerisch zu machen, indem der Typparameter α in seine Signatur eingefügt wird:

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

Auf diese Weise können Sie Variablen deklarieren und innerhalb dieser Funktion Ausdrücke vom Typ α erstellen , wenn Sie dies möchten . Aber...

2. Existenzielle Lösung:

Wenn Sie sich den Körper unserer Methode ansehen, werden Sie feststellen, dass wir nicht auf etwas vom Typ α zugreifen oder damit arbeiten ! Es gibt keine Ausdrücke mit diesem Typ oder Variablen, die mit diesem Typ deklariert wurden. Warum müssen wir also überhaupt heightgenerisch machen ? Warum können wir α nicht einfach vergessen ? Wie sich herausstellt, können wir:

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

Wie ich ganz am Anfang dieser Antwort schrieb, sind existenzielle und universelle Typen komplementärer / dualer Natur. Wenn also die Universallösung zu machen ist height mehr generisch, dann sollten wir erwarten , dass existentielle Typen die entgegengesetzte Wirkung haben: so dass es weniger generisch, nämlich durch Verstecken / Entfernen der Typ - Parameter α .

Infolgedessen können Sie t.valuein dieser Methode nicht mehr auf den Typ von verweisen oder Ausdrücke dieses Typs bearbeiten, da kein Bezeichner daran gebunden wurde. (Der ?Platzhalter ist ein spezielles Token, kein Bezeichner, der einen Typ "erfasst".) t.valueIst effektiv undurchsichtig geworden. Vielleicht ist das einzige, was Sie noch damit machen können, eine Typumwandlung Object.

Zusammenfassung:

===========================================================
                     |    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   |                  
=====================+=====================================

Dies sind alles gute Beispiele, aber ich entscheide mich, sie etwas anders zu beantworten. Erinnern Sie sich an Mathe, dass ∀x. P (x) bedeutet "für alle x kann ich beweisen, dass P (x)". Mit anderen Worten, es ist eine Art Funktion, Sie geben mir ein x und ich habe eine Methode, um es für Sie zu beweisen.

In der Typentheorie sprechen wir nicht von Beweisen, sondern von Typen. In diesem Bereich meinen wir also "für jeden Typ X, den Sie mir geben, gebe ich Ihnen einen bestimmten Typ P". Da wir P nicht viele Informationen über X geben, außer dass es sich um einen Typ handelt, kann P nicht viel damit anfangen, aber es gibt einige Beispiele. P kann den Typ "alle Paare des gleichen Typs" erstellen : P<X> = Pair<X, X> = (X, X). Oder wir können den Optionstyp erstellen: P<X> = Option<X> = X | Nilwobei Nil der Typ der Nullzeiger ist. Wir können daraus eine Liste machen : List<X> = (X, List<X>) | Nil. Beachten Sie, dass der letzte rekursiv ist. Die Werte von List<X>sind entweder Paare, bei denen das erste Element ein X und das zweite Element ein X istList<X> oder es ist ein Nullzeiger.

Nun, in Mathe ∃x. P (x) bedeutet "Ich kann beweisen, dass es ein bestimmtes x gibt, so dass P (x) wahr ist". Es mag viele solcher x geben, aber um es zu beweisen, reicht eines aus. Eine andere Möglichkeit ist, dass es eine nicht leere Menge von Beweis-und-Beweis-Paaren {(x, P (x))} geben muss.

Übersetzt in die Typentheorie: Ein Typ in der Familie ∃X.P<X>ist ein Typ X und ein entsprechender Typ P<X>. Beachten Sie, dass, bevor wir P X gegeben haben (so dass wir alles über X außer P sehr wenig wussten), dass jetzt das Gegenteil der Fall ist.P<X>verspricht nicht, irgendwelche Informationen über X zu geben, nur dass es eine gibt und dass es sich tatsächlich um einen Typ handelt.

Wie ist das nützlich? Nun, P könnte ein Typ sein, der seinen internen Typ X offenlegen kann. Ein Beispiel wäre ein Objekt, das die interne Darstellung seines Zustands X verbirgt. Obwohl wir keine Möglichkeit haben, ihn direkt zu manipulieren, können wir seine Wirkung durch beobachten Es könnte viele Implementierungen dieses Typs geben, aber Sie könnten alle diese Typen verwenden, unabhängig davon, welcher ausgewählt wurde.

So beantworten Sie Ihre Frage direkt:

Beim universellen Typ muss die Verwendung von Tden Typparameter enthalten X. Zum Beispiel T<String>oder T<Integer>. Für die existenziellen Typverwendungen von Tenthalten Sie diesen Typparameter nicht, da er unbekannt oder irrelevant ist - verwenden Sie ihn einfach T(oder in Java)T<?> ).

Weitere Informationen:

Universelle / abstrakte Typen und existenzielle Typen sind eine Dualität der Perspektive zwischen dem Verbraucher / Kunden eines Objekts / einer Funktion und dem Produzenten / der Implementierung desselben. Wenn eine Seite einen universellen Typ sieht, sieht die andere einen existenziellen Typ.

In Java können Sie eine generische Klasse definieren:

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

• Aus der Sicht eines Kunden von MyClass, Tist universell, weil Sie jeden Typ ersetzen könnenT , wenn Sie diese Klasse verwenden , und Sie müssen die tatsächliche Art von T wissen , wann immer Sie eine Instanz verwendenMyClass
• Aus der Sicht der Instanzmethoden an MyClasssichT ist es existenziell, weil es den wirklichen Typ von nicht kenntT
• Stellt in Java ?den existenziellen Typ dar - wenn Sie sich also innerhalb der Klasse befinden, Tist dies im Grunde genommen der Fall ?. Wenn Sie eine Instanz von MyClassmit Texistential behandeln möchten , können Sie MyClass<?>wie im secretMessage()obigen Beispiel deklarieren .

Existenzielle Typen werden manchmal verwendet, um die Implementierungsdetails von etwas zu verbergen, wie an anderer Stelle erläutert. Eine Java-Version davon könnte folgendermaßen aussehen:

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

Es ist etwas schwierig, dies richtig zu erfassen, da ich vorgebe, in einer funktionalen Programmiersprache zu sein, die Java nicht ist. Der Punkt hier ist jedoch, dass Sie eine Art von Status sowie eine Liste von Funktionen erfassen, die in diesem Status ausgeführt werden, und den tatsächlichen Typ des Status-Teils nicht kennen, die Funktionen jedoch, da sie bereits mit diesem Typ abgeglichen wurden .

In Java sind nun alle nicht endgültigen nicht-primitiven Typen teilweise existenziell. Dies mag seltsam klingen, aber weil eine Variable, die als deklariert wurde, Objectmöglicherweise eine Unterklasse von sein könnteObject deklariert wurde, stattdessen nicht den spezifischen Typ deklarieren kann, sondern nur "diesen Typ oder eine Unterklasse". Objekte werden also als Statusbit plus eine Liste von Funktionen dargestellt, die mit diesem Status arbeiten. Welche Funktion aufgerufen werden soll, wird zur Laufzeit durch Nachschlagen bestimmt. Dies ähnelt stark der Verwendung von existentiellen Typen, bei denen Sie einen existenziellen Zustandsteil und eine Funktion haben, die mit diesem Zustand arbeitet.

In statisch typisierten Programmiersprachen ohne Subtypisierung und Casts ermöglichen existenzielle Typen die Verwaltung von Listen unterschiedlich typisierter Objekte. Eine Liste von T<Int>darf keine enthalten T<Long>. Eine Liste von T<?>kann jedoch eine beliebige Variation von enthalten T, sodass viele verschiedene Datentypen in die Liste aufgenommen und bei Bedarf alle in ein int konvertiert werden können (oder alle in der Datenstruktur bereitgestellten Vorgänge ausgeführt werden können).

Man kann so ziemlich immer einen Datensatz mit einem existenziellen Typ in einen Datensatz konvertieren, ohne Verschlüsse zu verwenden. Ein Abschluss wird auch existenziell typisiert, indem die freien Variablen, über die er geschlossen wird, vor dem Aufrufer verborgen sind. Mit einer Sprache, die Verschlüsse, aber keine existenziellen Typen unterstützt, können Sie daher Verschlüsse erstellen, die denselben verborgenen Zustand aufweisen, den Sie in den existenziellen Teil eines Objekts eingefügt hätten.

Ein existenzieller Typ ist ein undurchsichtiger Typ.

Stellen Sie sich ein Dateihandle in Unix vor. Sie wissen, dass der Typ int ist, sodass Sie ihn leicht fälschen können. Sie können beispielsweise versuchen, aus Handle 43 zu lesen. Wenn das Programm eine Datei mit diesem bestimmten Handle geöffnet hat, lesen Sie daraus. Ihr Code muss nicht böswillig sein, sondern nur schlampig (z. B. könnte das Handle eine nicht initialisierte Variable sein).

Ein existenzieller Typ ist in Ihrem Programm verborgen. Wenn fopenein existenzieller Typ zurückgegeben wird, können Sie ihn nur mit einigen Bibliotheksfunktionen verwenden, die diesen existenziellen Typ akzeptieren. Zum Beispiel würde der folgende Pseudocode kompiliert:

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

Die Schnittstelle "read" wird deklariert als:

Es gibt einen Typ T, so dass:

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

Die Variable exfile ist keine int-, keine char*, keine struct-Datei - nichts, was Sie im Typsystem ausdrücken können. Sie können keine Variable deklarieren, deren Typ unbekannt ist, und Sie können beispielsweise keinen Zeiger in diesen unbekannten Typ umwandeln. Die Sprache lässt dich nicht.

Scheint, als würde ich etwas spät kommen, aber trotzdem fügt dieses Dokument eine andere Ansicht der existenziellen Typen hinzu, obwohl es nicht spezifisch sprachunabhängig ist , sollte es dann ziemlich einfacher sein, existenzielle Typen zu verstehen: http: //www.cs.uu .nl / groups / ST / Projects / ehc / ehc-book.pdf (Kapitel 8)

Der Unterschied zwischen einem universell und existenziell quantifizierten Typ kann durch die folgende Beobachtung charakterisiert werden:

• Die Verwendung eines Wertes mit einem ∀ quantifizierten Typ bestimmt den Typ, der für die Instanziierung der quantifizierten Typvariablen ausgewählt werden soll. Beispielsweise bestimmt der Aufrufer der Identitätsfunktion „id :: ∀aa → a“ den Typ, der für die Typvariable a für diese bestimmte Anwendung von id ausgewählt werden soll. Für die Funktionsanwendung „id 3“ entspricht dieser Typ Int.

• Die Erstellung eines Werts mit einem ∃ quantifizierten Typ bestimmt und verbirgt den Typ der quantifizierten Typvariablen. Zum Beispiel kann ein Schöpfer eines "∃a. (A, a → Int)" einen Wert dieses Typs aus "(3, λx → x)" konstruiert haben; Ein anderer Schöpfer hat aus „('x', λx → ord x)“ einen Wert mit demselben Typ erstellt. Aus Anwendersicht haben beide Werte den gleichen Typ und sind daher austauschbar. Der Wert hat einen bestimmten Typ für die Typvariable a ausgewählt, aber wir wissen nicht, welcher Typ, sodass diese Informationen nicht mehr ausgenutzt werden können. Diese wertspezifischen Typinformationen wurden "vergessen". wir wissen nur, dass es existiert.

Für alle Werte der Typparameter existiert ein universeller Typ. Ein existentieller Typ existiert nur für Werte der Typparameter, die die Einschränkungen des existentiellen Typs erfüllen.

In Scala ist beispielsweise eine Möglichkeit, einen existenziellen Typ auszudrücken, ein abstrakter Typ, der auf einige obere oder untere Grenzen beschränkt ist.

trait Existential {
  type Parameter <: Interface
}

Entsprechend ist ein eingeschränkter Universaltyp ein existenzieller Typ wie im folgenden Beispiel.

trait Existential[Parameter <: Interface]

Jede Verwendungssite kann das verwenden, Interfaceda alle instanziierbaren Untertypen von Existentialdefinieren müssen, type Parameterwelche das implementieren müssen Interface.

Ein entarteter Fall eines existenziellen Typs in Scala ist ein abstrakter Typ, auf den niemals Bezug genommen wird und der daher von keinem Subtyp definiert werden muss. Dies hat effektiv eine Kurzschreibweise von List[_] in Scala und List<?>in Java.

Meine Antwort wurde von Martin Oderskys Vorschlag inspiriert , abstrakte und existenzielle Typen zu vereinen . Die beiliegende Folie hilft beim Verständnis.

Die Erforschung abstrakter Datentypen und das Verstecken von Informationen brachten existenzielle Typen in Programmiersprachen. Wenn Sie einen Datentyp abstrakt erstellen, werden Informationen zu diesem Typ ausgeblendet, sodass ein Client dieses Typs ihn nicht missbrauchen kann. Angenommen, Sie haben einen Verweis auf ein Objekt. In einigen Sprachen können Sie diesen Verweis auf einen Verweis auf Bytes umwandeln und mit diesem Speicherelement alles tun, was Sie möchten. Um das Verhalten eines Programms zu gewährleisten, ist es für eine Sprache hilfreich, zu erzwingen, dass Sie nur über die vom Designer des Objekts bereitgestellten Methoden auf den Verweis auf das Objekt reagieren. Sie wissen, dass der Typ existiert, aber nichts weiter.

Sehen:

Abstrakte Typen haben existenziellen Typ, MITCHEL & PLOTKIN

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

Ich habe dieses Diagramm erstellt. Ich weiß nicht, ob es streng ist. Aber wenn es hilft, bin ich froh.

Soweit ich weiß, ist es eine mathematische Art, Schnittstellen / abstrakte Klassen zu beschreiben.

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

Für C # würde es in einen generischen abstrakten Typ übersetzt:

abstract class MyType<T>{
    private T a;

    public abstract int f(T x);
}

"Existenziell" bedeutet nur, dass es einen Typ gibt, der den hier definierten Regeln entspricht.