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 this
parametry 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 T
vs. T<X>
), to też byłoby to docenione.
java
interfaces
type-systems
stakx
źródło
źródło
Odpowiedzi:
Hmm ... Ta definicja wygląda bardzo podobnie do próbki Haskell, którą widziałem dawno temu.
Po
X
zastosowaniu konstruktora ∀ faktycznie staje się ∃. Zauważ, że kiedy wyjmujesz,value
nie znasz typu i masz nad nim pusty zestaw operacji. Ale ponieważviewValue
jest to w pewnym sensie spójnevalue
, można do niego zastosować.Myślę, że główną różnicą w Javie,
interface
którą zaproponowałeś, jest fakt, że musisz znać typ pośredni, aby przekazać wynikop₁
doop₂
. 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 jestX
konstruktorem używanym wX 3 show
(show
jest funkcją, która pobiera argument dowolnego typu, który implementujeShow
i zwracaString
)Zaktualizowano: Właśnie przeczytałem twoje pytanie i myślę, że mam odpowiednią konstrukcję dla Java:
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ą
this
i 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ł.
źródło
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.
źródło
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.
źródło