Czy typy uniwersalne są podtypem, czy specjalnym przypadkiem typów egzystencjalnych?

Chciałbym wiedzieć, czy uniwersalnie skwantyfikowany typ : jest podtypem lub przypadkiem szczególnym skwantyfikowanego egzystencjalnie wpisz z tym samym podpisem: $T_a$

T_{a} = \forall X : {a \in X, f : X \to {T, F}}

$T_a = \forall X: \left\{ a\in X,f:X→\{T, F\} \right\}$

T_{e}

$T_e$

T_{e} = \exists X : {a \in X, f : X \to {T, F}}

$T_e = \exists X: \left\{ a\in X,f:X→\{T, F\} \right\}$

Powiedziałbym „tak”: Jeśli coś jest prawdą „dla wszystkich X” ( ), to musi być również prawdziwe „dla niektórych X” ( ). Oznacza to, że instrukcja z „ ” jest po prostu bardziej ograniczoną wersją tej samej instrukcji z „ ”: $\forall X$ $\exists X$ $\forall$ $\exists$

\forall X, P (X) \overset{?}{⟹} \exists X, P (X) .

$∀X, P(X) \overset?\implies ∃X, P(X).$

Czy gdzieś się mylę?

Tło: Dlaczego o to pytam?

Studiuję typy egzystencjalne, aby zrozumieć, dlaczego i jak „typy abstrakcyjne [dane] mają typ egzystencjalny” . Nie mogę dobrze zrozumieć tej koncepcji na podstawie samej teorii; Potrzebuję też konkretnych przykładów.

Niestety trudno znaleźć dobre przykłady kodu, ponieważ większość języków programowania ma ograniczoną obsługę typów egzystencjalnych. (Na przykład symbole wieloznaczne Haskellaforall lub Javy? .) Z drugiej strony typy uniwersalne są obsługiwane przez wiele najnowszych języków za pomocą „ogólnych”.

Co gorsza, generyczne wydają się łatwo mieszać z typami egzystencjalnymi , co jeszcze bardziej utrudnia odróżnienie typów egzystencjalnych od uniwersalnych. Jestem ciekawy, dlaczego takie pomieszanie występuje tak łatwo. Odpowiedź na to pytanie może to wyjaśnić: jeśli typy uniwersalne są rzeczywiście tylko szczególnym przypadkiem typów egzystencjalnych, nic dziwnego, że typy ogólne, np. Java List<T>, mogą być interpretowane w obie strony.

logic type-theory typing

— Raphael
źródło

Jaka jest nawet różnica między uniwersalnym a egzystencjalnym?

Z matematycznego punktu widzenia masz rację: jeśli forall x. P(x)tak exists x. P(x). Czy systemy typów uwzględniają to przy sprawdzaniu typów ... Nie mam pojęcia. +1 za interesujące pytanie.

@deinan: Jeśli P (x) nie ma żadnego x , to na pewno ∀xP (x) nie ma. Prawdopodobnie miałeś na myśli to, że gdy nie ma x , to znaczy ∀x∈XP (x) nie oznacza ∃x∈XP (x), jeśli X = ∅ .

... I zauważ, że jeśli zostaną przepisane bez ustawionej notacji, będą wyglądać inaczej: ∀xx∈X⇒P (x) vs. ∃xx∈X & P (x) i że ∃xx∈X⇒P (x) zostanie spełniony trywialnie żadnymi x nie z X .

Fajne pytanie. W Haskell z pewnością prawdą jest, że wartość typu (forall b. Show b => b) może zostać przekazana do funkcji, która przyjmuje (forall b. B), ale nie odwrotnie, co oznacza, że można oczekiwać podstawienia związek podtytułu. Ale oczywiście, kiedy mówisz o typach, powinieneś wspomnieć o systemie typów, na który patrzysz, szczególnie jeśli masz na myśli algebrę formalną dla swojej semantyki ...

Odpowiedzi:

$\forall x:T, P(x)$ $\exists x:T,P(x)$ $T$

$(\forall x:T, P(x)) ⇒ (\exists x:T, P(x))$ $T_a$ $T_e$

$T_a = ∀X.\{a: X, f: X\rightarrow\mathsf{bool}\}$ $A$ $A(M)$ $M:X$ $M_1$ $M_2$ $X$ $A(M_1)$ $A(M_2)$ $T_a$

$T_e = \exists X.\{a: X, f: X\rightarrow\mathsf{bool}\}$ $B$ $T_e$ $N: X$ $\pi_1(B) = N$ $\pi_2(B) = \{a:N, f:N\rightarrow\mathsf{bool}\}$ $N$

Nie daj się zwieść Haskellowi forall: pomimo nazwy jest to forma egzystencjalnego kwantyfikatora.

W tle zdecydowanie polecam Typy i Języki programowania (rozdziały 23 i 24 omawiają odpowiednio typy uniwersalne i typy egzystencjalne). Zapewni przydatne tło do zrozumienia artykułów badawczych.

— Gilles „SO- przestań być zły”
źródło

Jeden drobny i dość późny spór - Haskell foralljest rzeczywiście uniwersalnym kwantyfikatorem w oryginalnym kontekście ukrytej kwantyfikacji, którą wyraźnie określa, mianowicie oglądając typy polimorficzne „z zewnątrz” dla definicji najwyższego poziomu. W „wnętrzu” takiej definicji, manipulując argumentami, typy polimorficzne są faktycznie egzystencjalne; każda zmienna typu jest powiązana z jakimś typem, ale nie wiemy (i nie możemy), czym jest ten typ. Według mojej wiedzy żadna implementacja Haskell nie obsługuje prawdziwych (surowych, najwyższych poziomów) typów egzystencjalnych i nie jest dla mnie jasne, jaki cel by to w ogóle służyło.

— CA McCann

Typy egzystencjalne obsługiwane przez GHC to typy, które (bezpośrednio lub pośrednio) mają uniwersalne kwantyfikatory, które, patrząc z „zewnątrz”, występują w pozycji przeciwstawnej. Wykorzystuje to w przybliżeniu tę samą dualność, co logicznej negacji, więc aby mieć takie typy egzystencjalne na najwyższym poziomie, muszą one być podwójnie sprzeczne, używając kodowania podobnego do CPS (jest to równoważność, którą daje Uday Reddy). Należy zauważyć, że kwantyfikatory egzystencjalne w intuicyjnej formie powodują podobne niedogodności z podobnych powodów.

— CA McCann,

$\forall X.\, P(X)$ $\exists X.\, P(X)$

$\forall X.\, (X \times (X \to Bool))$ $X$ $\exists X.\, (X \times (X \to Bool))$

 f (p: \forall X. (X * (X -> Bool))) = PACK X = Bool WITH p[Bool]

Artykuł, który wspominasz o typach egzystencjalnych, jest nieco teoretyczny. Bardziej samouczkiem jest artykuł Cardelli i Wegnera: O zrozumieniu typów, abstrakcji danych i polimorfizmu . Najbardziej zaawansowane podręczniki na temat języków programowania również omawiają typy egzystencjalne. Dobrą książką do sprawdzenia byłyby Podstawy języków programowania Mitchella .

Masz rację, że większość języków programowania nie ma jawnie typów egzystencjalnych. Jednak wiele z nich ma abstrakcyjne typy (lub inne nazwy, takie jak „pakiety” lub „moduły”). Są więc w stanie wyrażać wartości typów egzystencjalnych, nawet jeśli nie traktują takich wartości jako byty pierwszej klasy.

$\exists X.\, P(X)$ $\forall Y.\, (\forall X.\, P(X) \rightarrow Y) \to Y$ $\forall$

— Uday Reddy
źródło