Co to jest typ egzystencjalny?

Przeczytałem artykuł w Wikipedii Typy egzystencjalne . Dowiedziałem się, że nazywa się je typami egzystencjalnymi ze względu na operator egzystencjalny (∃). Nie jestem jednak pewien, jaki to ma sens. Jaka jest różnica pomiędzy

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

i

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

?

Kiedy ktoś definiuje typ uniwersalny ∀X, mówi: Możesz podłączyć dowolny typ, nie muszę nic wiedzieć o typie, aby wykonać swoją pracę, będę się do niego odnosił nieprzejrzysto jakoX .

Kiedy ktoś definiuje typ egzystencjalny ∃X, mówi: Użyję tutaj dowolnego typu; nie będziesz wiedział nic o typie, więc możesz nazywać go nieprzejrzystym językiemX .

Uniwersalne typy pozwalają pisać takie rzeczy jak:

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

copyFunkcja nie ma pojęcia, co Trzeczywiście będzie, ale to nie jest konieczne.

Typy egzystencjalne pozwolą Ci pisać takie rzeczy, jak:

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

Każda implementacja maszyny wirtualnej na liście może mieć inny typ kodu bajtowego. runAllCompilersFunkcja nie ma pojęcia, co rodzaj kodu bajtowego jest, ale to nie jest konieczne; wszystko, co robi, to przekazywanie kodu bajtowego z VirtualMachine.compiledo VirtualMachine.run.

Symbole wieloznaczne typu Java (np.:) List<?>To bardzo ograniczona forma typów egzystencjalnych.

Aktualizacja: zapomniałem wspomnieć, że możesz symulować typy egzystencjalne za pomocą typów uniwersalnych. Najpierw zawiń swój typ uniwersalny, aby ukryć parametr typu. Po drugie, odwrócenie kontroli (to skutecznie zamienia część „ty” i „ja” w powyższych definicjach, co jest podstawową różnicą między egzystencjalnymi i uniwersalnymi).

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

Teraz możemy mieć VMWrapperwłasne wywołanie, VMHandlerktóre ma uniwersalną handlefunkcję. Efekt netto jest taki sam, nasz kod musi być traktowany Bjako nieprzejrzysty.

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

Przykładowa implementacja maszyny wirtualnej:

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

Wartość typu egzystencjalnego, takiego jak, ∃x. F(x) jest parą zawierającą pewien typ x i wartość typu F(x). Natomiast wartość typu polimorficznego, takiego jak, ∀x. F(x)jest funkcją, która przyjmuje pewien typ xi wytwarza wartość typu F(x). W obu przypadkach typ zamyka się na jakimś konstruktorze typów F.

Zwróć uwagę, że ten widok łączy typy i wartości. Dowód egzystencjalny to jeden typ i jedna wartość. Dowód uniwersalny to cała rodzina wartości indeksowanych według typu (lub odwzorowanie typów na wartości).

Zatem różnica między dwoma określonymi typami jest następująca:

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

Oznacza to: Wartość typu Tzawiera wywołany typ X, wartość a:Xi funkcję f:X->int. Producent wartości typu Tmoże wybrać dowolny typ, Xa konsument nie może nic wiedzieć X. Tyle tylko, że istnieje jeden przykład o nazwie ai że tę wartość można zamienić na a int, podając ją f. Innymi słowy, wartość typu Twie, jak w intjakiś sposób utworzyć . Cóż, możemy wyeliminować typ pośredni Xi po prostu powiedzieć:

T = int

Ten, który jest określany ilościowo, jest trochę inny.

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

Oznacza to, że: Wartość typu Tmoże mieć dowolny typ Xi wygeneruje wartość a:Xi funkcję f:X->int bez względu na to, co nią Xjest . Innymi słowy: konsument wartości typu Tmoże wybrać dowolny typ X. A wytwórca wartości typu Tnie może w ogóle nic wiedzieć X, ale musi być w stanie wytworzyć wartość adla dowolnego wyboru Xi być w stanie przekształcić taką wartość w int.

Oczywiście implementacja tego typu jest niemożliwa, ponieważ nie ma programu, który mógłby wygenerować wartość każdego możliwego do wyobrażenia typu. Chyba że pozwolisz na absurdy takie jak nulllub dno.

Ponieważ egzystencjalny jest parą, egzystencjalny argument można przekształcić w uniwersalny za pomocą curry .

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

jest taki sam jak:

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

Ten pierwszy jest egzystencjalny na drugim miejscu . Prowadzi to do następującej użytecznej właściwości:

Każdy egzystencjalnie skwantyfikowany typ rangi n+1jest ogólnie skwantyfikowany typ rangi n.

Istnieje standardowy algorytm przekształcania egzystencji w uniwersalia, zwany skolemizacją .

Myślę, że sensowne jest wyjaśnianie typów egzystencjalnych razem z typami uniwersalnymi, ponieważ te dwa pojęcia są komplementarne, tj. Jedno jest „przeciwieństwem” drugiego.

Nie mogę odpowiedzieć na wszystkie szczegóły dotyczące typów egzystencjalnych (takich jak podanie dokładnej definicji, lista wszystkich możliwych zastosowań, ich związek z abstrakcyjnymi typami danych itp.), Ponieważ po prostu nie mam do tego wystarczającej wiedzy. Pokażę tylko (używając Java), co ten artykuł HaskellWiki określa jako główny efekt typów egzystencjalnych:

Typy egzystencjalne mogą być używane do kilku różnych celów. Ale to, co robią, to „ukrywanie” zmiennej typu po prawej stronie. Zwykle każda zmienna typu pojawiająca się po prawej stronie musi również pojawić się po lewej stronie […]

Przykładowa konfiguracja:

Poniższy pseudo-kod nie jest całkiem poprawnym kodem Java, chociaż byłoby to łatwe do naprawienia. Właściwie to właśnie zamierzam zrobić w tej odpowiedzi!

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

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

Pozwól, że ci to krótko przeliteruję. Definiujemy…

• typ rekurencyjny, Tree<α>który reprezentuje węzeł w drzewie binarnym. Każdy węzeł przechowuje valuejakiś typ α i ma odniesienia do opcjonalnych lefti rightpoddrzew tego samego typu.

• funkcja, heightktóra zwraca najdalszą odległość od dowolnego węzła liścia do węzła głównego t.

Teraz zamieńmy powyższy pseudokod heightna właściwą składnię Java! (Ze względu na zwięzłość będę nadal pomijał pewne schematy, takie jak orientacja obiektowa i modyfikatory dostępności). Pokażę dwa możliwe rozwiązania.

1. Rozwiązanie uniwersalne:

Najbardziej oczywistą poprawką jest po prostu utworzenie heightgenerycznego poprzez wprowadzenie parametru typu α do jego podpisu:

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

Umożliwiłoby to deklarowanie zmiennych i tworzenie wyrażeń typu α wewnątrz tej funkcji, gdybyś chciał. Ale...

2. Rozwiązanie typu egzystencjalnego:

Jeśli spojrzysz na treść naszej metody, zauważysz, że tak naprawdę nie mamy dostępu do niczego typu α ani nie pracujemy z nim ! Nie ma wyrażeń posiadających ten typ, ani żadnych zmiennych zadeklarowanych z tym typem ... więc dlaczego w ogóle musimy tworzyć heightrodzajowe? Dlaczego nie możemy po prostu zapomnieć o α ? Jak się okazuje, możemy:

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

Jak napisałem na samym początku tej odpowiedzi, typy egzystencjalne i uniwersalne mają charakter komplementarny / dualny. Tak więc, gdyby uniwersalne rozwiązanie typu miało uczynić height bardziej rodzajowym, to należałoby się spodziewać, że typy egzystencjalne mają odwrotny skutek: uczynienie go mniej rodzajowym, a mianowicie poprzez ukrycie / usunięcie parametru typu α .

W konsekwencji nie można już odwoływać się do typu t.valuew tej metodzie ani manipulować jakimikolwiek wyrażeniami tego typu, ponieważ żaden identyfikator nie został z nim powiązany. (Symbol ?wieloznaczny jest specjalnym tokenem, a nie identyfikatorem, który „przechwytuje” typ.) W t.valuerzeczywistości stał się nieprzejrzysty; być może jedyne, co nadal możesz z nim zrobić, to przerzucić go na typ Object.

Podsumowanie:

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

To są dobre przykłady, ale wolę odpowiedzieć na to trochę inaczej. Przypomnijmy sobie z matematyki, że ∀x. P (x) oznacza „dla wszystkich x mogę udowodnić, że P (x)”. Innymi słowy, jest to rodzaj funkcji, dajesz mi x i mam metodę, aby to udowodnić.

W teorii typów nie mówimy o dowodach, ale o typach. Więc w tym miejscu mamy na myśli „dla każdego typu X, który mi podasz, podam ci konkretny typ P”. Ponieważ nie podajemy P zbyt wielu informacji na temat X poza faktem, że jest to typ, P nie może z nim wiele zrobić, ale jest kilka przykładów. P może tworzyć rodzaj „wszystkich par tego samego typu”: P<X> = Pair<X, X> = (X, X). Lub możemy utworzyć typ opcji P<X> = Option<X> = X | Nil:, gdzie Nil jest typem wskaźników zerowych. Możemy zrobić listę z niego: List<X> = (X, List<X>) | Nil. Zwróć uwagę, że ostatni jest rekurencyjny, wartościami List<X>są albo pary, gdzie pierwszy element to X, a drugi element to a, List<X>albo jest to wskaźnik zerowy.

Teraz w matematyce ∃x. P (x) oznacza „Mogę udowodnić, że istnieje taki konkretny x, że P (x) jest prawdziwy”. Takich x może być wiele, ale aby to udowodnić, wystarczy jeden. Inaczej można o tym myśleć, że musi istnieć niepusty zestaw par dowód-dowód {(x, P (x))}.

Przetłumaczone na teorię typów: typ w rodzinie ∃X.P<X>to typ X i odpowiadający mu typ P<X>. Zauważ, że chociaż wcześniej daliśmy X do P (tak, że wiedzieliśmy wszystko o X, ale o P bardzo mało), teraz jest odwrotnie. P<X>nie obiecuje podać żadnych informacji o X, tylko, że istnieje i że rzeczywiście jest typem.

Jak to jest przydatne? Cóż, P może być typem, który ma sposób na ujawnienie swojego wewnętrznego typu X. Przykładem może być obiekt, który ukrywa wewnętrzną reprezentację swojego stanu X. Chociaż nie mamy możliwości bezpośredniego manipulowania nim, możemy zaobserwować jego efekt poprzez szturchanie w P. Może być wiele implementacji tego typu, ale można użyć wszystkich tych typów, niezależnie od tego, który z nich został wybrany.

Aby bezpośrednio odpowiedzieć na Twoje pytanie:

W przypadku typu uniwersalnego użycie Tmusi zawierać parametr type X. Na przykład T<String>lub T<Integer>. W przypadku typów egzystencjalnych użycie Tnie obejmuje tego parametru, ponieważ jest on nieznany lub nieistotny - po prostu użyj T(lub w Javie T<?>).

Dalsza informacja:

Typy uniwersalne / abstrakcyjne i typy egzystencjalne to dwoistość perspektywy między konsumentem / klientem obiektu / funkcji a jej producentem / wdrożeniem. Kiedy jedna strona widzi typ uniwersalny, druga widzi typ egzystencjalny.

W Javie możesz zdefiniować klasę ogólną:

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

• Z punktu widzenia klienta o MyClass, Tjest uniwersalny, ponieważ można zastąpić dowolny typ dla Tpodczas korzystania z tej klasy, a trzeba wiedzieć, rzeczywisty typ T każdym użyciu instancjęMyClass
• Z punktu widzenia MyClasssamych metod instancji Tjest egzystencjalny, ponieważ nie zna prawdziwego typuT
• W Javie ?reprezentuje typ egzystencjalny - tak więc, gdy jesteś wewnątrz klasy, w Tzasadzie jest ?. Jeśli chcesz obsłużyć wystąpienie MyClassz Tegzystencjalnym, możesz zadeklarować MyClass<?>jak w secretMessage()powyższym przykładzie.

Typy egzystencjalne są czasami używane do ukrywania szczegółów implementacji czegoś, co omówiono w innym miejscu. Wersja Java może wyglądać następująco:

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

Trochę trudno jest to poprawnie uchwycić, ponieważ udaję, że jestem w jakimś funkcjonalnym języku programowania, którym nie jest Java. Ale chodzi o to, że przechwytujesz jakiś stan oraz listę funkcji, które działają na tym stanie i nie znasz rzeczywistego typu części stanu, ale funkcje tak, ponieważ zostały już dopasowane do tego typu .

Teraz w Javie wszystkie nieokończone typy niebędące prymitywami są częściowo egzystencjalne. Może to zabrzmieć dziwnie, ale ponieważ zmienna zadeklarowana jako Objectmoże potencjalnie być podklasą Objectzamiast tego, nie można zadeklarować określonego typu, a jedynie „ten typ lub podklasę”. I tak, obiekty są reprezentowane jako bit stanu oraz lista funkcji, które działają na tym stanie - dokładnie, która funkcja do wywołania jest określana w czasie wykonywania przez wyszukiwanie. Jest to bardzo podobne do użycia typów egzystencjalnych powyżej, w których mamy część stanu egzystencjalnego i funkcję, która działa na tym stanie.

W językach programowania z typami statycznymi bez podtypów i rzutowań typy egzystencjalne pozwalają na zarządzanie listami obiektów o różnym typie. Lista T<Int>nie może zawierać T<Long>. Jednak lista T<?>może zawierać dowolną odmianę T, co pozwala na umieszczenie wielu różnych typów danych na liście i przekonwertowanie ich wszystkich na int (lub wykonanie jakichkolwiek operacji w strukturze danych) na żądanie.

Prawie zawsze można przekonwertować rekord typu egzystencjalnego na rekord bez użycia domknięć. Zamknięcie jest również wpisane egzystencjalnie, ponieważ wolne zmienne, nad którymi jest zamykane, są ukryte przed wywołującym. Tak więc język, który obsługuje domknięcia, ale nie typy egzystencjalne, może pozwolić ci na tworzenie domknięć, które mają ten sam stan ukryty, który umieściłbyś w egzystencjalnej części obiektu.

Typ egzystencjalny to typ nieprzejrzysty.

Pomyśl o uchwycie pliku w systemie Unix. Wiesz, że jest to typ int, więc możesz go łatwo podrobić. Możesz na przykład spróbować czytać z uchwytu 43. Jeśli tak się stanie, że program ma otwarty plik z tym konkretnym uchwytem, ​​będziesz czytać z niego. Twój kod nie musi być złośliwy, po prostu niechlujny (np. Uchwyt może być niezainicjowaną zmienną).

Typ egzystencjalny jest ukryty przed twoim programem. Jeśli fopenzwracany jest typ egzystencjalny, wszystko, co możesz z nim zrobić, to użyć go z niektórymi funkcjami bibliotecznymi, które akceptują ten typ egzystencjalny. Na przykład skompilowałby się następujący pseudokod:

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

Interfejs „do odczytu” jest deklarowany jako:

Istnieje typ T taki, że:

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

Zmienna exfile nie jest int, nie jest char*ani strukturą File - nic, co można wyrazić w systemie typów. Nie możesz zadeklarować zmiennej, której typ jest nieznany i nie możesz rzutować, powiedzmy, wskaźnika na ten nieznany typ. Język ci na to nie pozwala.

Wygląda na to, że spóźniam się trochę, ale w każdym razie ten dokument dodaje inny pogląd na to, jakie typy egzystencjalne są, chociaż nie jest to specyficznie niezależne od języka, powinno być wtedy znacznie łatwiejsze do zrozumienia typów egzystencjalnych: http: //www.cs.uu .nl / groups / ST / Projects / ehc / ehc-book.pdf (rozdział 8)

Różnicę między typem kwantyfikowanym uniwersalnie a egzystencjalnie można scharakteryzować za pomocą następującej obserwacji:

• Użycie wartości z typem ilościowym ∀ określa typ, który należy wybrać do tworzenia wystąpienia zmiennej typu określonego ilościowo. Na przykład, obiekt wywołujący funkcję tożsamości „id :: ∀aa → a” ​​określa typ do wyboru dla zmiennej typu a dla tego konkretnego zastosowania id. Dla aplikacji funkcji „id 3” ten typ jest równy Int.

• Utworzenie wartości o typie ilościowym ∃ określa i ukrywa typ zmiennej typu ilościowego. Na przykład twórca „∃a. (A, a → Int)” mógł skonstruować wartość tego typu z „(3, λx → x)”; inny twórca skonstruował wartość tego samego typu z „('x', λx → ord x)”. Z punktu widzenia użytkownika obie wartości są tego samego typu i dlatego można je stosować zamiennie. Wartość ma określony typ wybrany dla zmiennej typu a, ale nie wiemy, jakiego typu, więc informacji tej nie można już wykorzystać. Ta informacja o typie wartości została „zapomniana”; wiemy tylko, że istnieje.

Typ uniwersalny istnieje dla wszystkich wartości parametrów typu. Typ egzystencjalny istnieje tylko dla wartości parametrów typu, które spełniają ograniczenia typu egzystencjalnego.

Na przykład w Scali jednym ze sposobów wyrażenia typu egzystencjalnego jest typ abstrakcyjny, który jest ograniczony do jakichś górnych lub dolnych granic.

trait Existential {
  type Parameter <: Interface
}

Równoważnie ograniczony typ uniwersalny jest typem egzystencjalnym, jak w poniższym przykładzie.

trait Existential[Parameter <: Interface]

Każda witryna użytkowania może stosować, Interfaceponieważ wszystkie instancyjne podtypy Existentialmuszą definiować, type Parameterktóre muszą implementować Interface.

Zdegenerowany przypadek od typu egzystencjalnego w Scala jest abstrakcyjny typ, który nigdy nie jest dalej, a zatem nie musi być określone przez każdego podtypu. To faktycznie ma skróconą notację List[_] w Scali i List<?>Javie.

Moja odpowiedź została zainspirowana propozycją Martina Odersky'ego, aby ujednolicić typy abstrakcyjne i egzystencjalne. Slajdów towarzyszący wspomaga zrozumienie.

Badania nad abstrakcyjnymi typami danych i ukrywaniem informacji wprowadziły typy egzystencjalne do języków programowania. Tworzenie abstraktu typu danych ukrywa informacje o tym typie, więc klient tego typu nie może ich nadużywać. Powiedzmy, że masz odniesienie do obiektu ... niektóre języki umożliwiają rzutowanie tego odniesienia na odniesienie do bajtów i robienie wszystkiego, co chcesz, z tym fragmentem pamięci. W celu zagwarantowania zachowania programu przydatne jest, aby język wymusił, że działasz tylko na odwołaniu do obiektu za pośrednictwem metod dostarczonych przez projektanta obiektu. Wiesz, że ten typ istnieje, ale nic więcej.

Widzieć:

Typy abstrakcyjne mają typ egzystencjalny, MITCHEL i PLOTKIN

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

Stworzyłem ten diagram. Nie wiem, czy to jest rygorystyczne. Ale jeśli to pomoże, cieszę się.

Jak rozumiem, jest to matematyczny sposób opisania interfejsów / klasy abstrakcyjnej.

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

W przypadku C # będzie to przekładać się na ogólny typ abstrakcyjny:

abstract class MyType<T>{
    private T a;

    public abstract int f(T x);
}

„Egzystencjalny” oznacza po prostu, że istnieje pewien typ, który jest zgodny z określonymi tutaj regułami.