Czym różnią się typy egzystencjalne od interfejsów?

Biorąc pod uwagę typ egzystencjalny

T = ∃X.{op₁:X, op₂:X→boolean}

i ten ogólny interfejs Java:

interface T<X> {
    X op₁();
    boolean op₂(X something);
}

Jakie są podstawowe różnice między typem egzystencjalnym a interfejsem Java?

Oczywiście istnieją różnice składniowe i orientacja obiektowa Javy (która obejmuje również szczegóły, takie jak ukryte thisparametry itp.). Nie interesuję się nimi tak bardzo, jak różnicami koncepcyjnymi i semantycznymi - chociaż jeśli ktoś chciałby rzucić światło na pewne drobniejsze punkty (takie jak różnica notacyjna między Tvs. T<X>), to też byłoby to docenione.

Hmm ... Ta definicja wygląda bardzo podobnie do próbki Haskell, którą widziałem dawno temu.

{-# LANGUAGE ExistentialQuantification #-}
data X = forall a . X { value :: a, viewValue :: a -> String }
instance Show X where show (X { value = x, viewValue = f}) = f x
sample :: [X]
sample = [X 3 show, X "abc" show, X 3.14 show]

Po Xzastosowaniu konstruktora ∀ faktycznie staje się ∃. Zauważ, że kiedy wyjmujesz, valuenie znasz typu i masz nad nim pusty zestaw operacji. Ale ponieważ viewValuejest to w pewnym sensie spójne value, można do niego zastosować.

Myślę, że główną różnicą w Javie, interfacektórą zaproponowałeś, jest fakt, że musisz znać typ pośredni, aby przekazać wynik op₁do op₂. Tj. Odpowiedni system dla typu egzystencjalnego powinien wybrać odpowiedni typ, który jest gwarantowany przez warunek. Czyli powinien być w stanie napisać funkcję z rodzaju: ∀X. X→(X→boolean)→T. W poprzednim przykładzie taka funkcja jest Xkonstruktorem używanym w X 3 show( showjest funkcją, która pobiera argument dowolnego typu, który implementuje Showi zwraca String)

Zaktualizowano: Właśnie przeczytałem twoje pytanie i myślę, że mam odpowiednią konstrukcję dla Java:

interface T {
    boolean op₂();
}
...
T x = new T() {
    private final int op₁ = ...;
    public boolean op₂() { return ((op₁ % 2) == 0); }
};
T y = new T() {
    private final char op₁ = ...;
    public boolean op₂() { return ('0' <= op₁ && op₁ <= '9'); }
};
if (x.op₂() && y.op₂()) ...

Masz rację, wspominając this- to właściwie twój op₁.

Wydaje mi się, że rozumiem teraz, że klasyczne języki OOP (Java, C #, C ++ itp.) Zawsze implementują typ egzystencjalny z pojedynczą wartością thisi nad nim funkcje zwane „metodami”, które domyślnie wywoływane są z tą wartością :)

PS Niestety, nie znam się zbytnio na Javie, ale mam nadzieję, że masz pomysł.

Jedyną różnicą jest to, że interfejs Java w rzeczywistości coś znaczy dla kompilatora Java.

Typ egzystencjalny jest formalną definicją typu, niespecyficzną dla żadnego języka. Informatycy używają tego rodzaju definicji, aby udowodnić pewne rzeczy na temat typu i języków, które go implementują. Interfejs Java jest jedną z implementacji języka Java formalnie zdefiniowanego typu.

2 przedstawione typy są bardzo różne. Definicja interfejsu, którą napisałeś, jest uniwersalnym typem (ogólnie rzecz biorąc Java należy do tej kategorii).

Typ egzystencjalny ukrywa typ w ramach swojej implementacji przed konsumentem. Intuicyjnie, aby X był egzystencjalny w T, tożsamości X nie można poznać od żadnego konsumenta; wszystko, co powinno być znane, to zestaw operacji podanych w definicji. Istnieje jeden typ T dla niektórych typów X.

Natomiast typ uniwersalny definiuje operacje mające zastosowanie do wszystkich typów, z których konsument ma swobodę wyboru. Typ interfejsu T jest dokładnie taki. X jest tworzony przez konsumenta, który dokładnie wie, jaki jest typ X. Istnieje typ T dla każdego typu X we wszechświecie.

Egzystencje nie są w rzeczywistości obecne w Javie jako konstrukcja języka, z wyjątkiem ograniczonego przypadku symboli wieloznacznych ( List<?>). Ale tak, można je emulować za pomocą interfejsów. Problem staje się wtedy bardziej projektowy.

Jak już wskazano, w obiektowym ustawieniu egzystencjalne stają się trudne do wdrożenia, ponieważ sposób, w jaki zwykle kodujesz informacje o typie X (co możesz z tym zrobić), to mieć funkcje składowe w typie interfejsu, który implementuje X. Krótko mówiąc, interfejsy mogą kupić pewne funkcje abstrakcji typu, ale w pewnym stopniu wymagają eliminacji egzystencjalnej.