TheWiki Haskell robi dobrą robotę wyjaśniając, jak używać typów egzystencjalnych, ale nie do końca rozumiem teorię stojącą za nimi.

Rozważmy ten przykład typu egzystencjalnego:

data S = forall a. Show a => S a      -- (1)

zdefiniować opakowanie typu dla rzeczy, które możemy przekonwertować naString. Wiki wspomina, co mynaprawdę chcesz zdefiniować to rodzaj

data S = S (exists a. Show a => a)    -- (2)

tj. prawdziwy typ „egzystencjalny” - luźno myślę o tym jako o „konstruktorze danychS przyjmuje dowolny typ, dla któregoShow instancjaistnieje i zawija to. ”Prawdę mówiąc, możesz napisać GADT w następujący sposób:

data S where                          -- (3)
    S :: Show a => a -> S

Nie próbowałem tego kompilować, ale wygląda na to, że powinno działać. Dla mnie GADT jest oczywiście odpowiednikiem kodu (2), który chcielibyśmy napisać.

Jednak nie jest dla mnie oczywiste, dlaczego (1) jest równoważne (2). Dlaczego przeniesienie konstruktora danych na zewnątrz powoduje obrótforall wexists?

Najbliższą rzeczą, jaką mogę myśleć, sąPrawa De Morgana w logice, gdzie zamiana kolejności negacji i kwantyfikatora zamienia kwantyfikatory egzystencjalne w uniwersalne kwantyfikatory i odwrotnie:

¬(∀x. px) ⇔ ∃x. ¬(px)

ale konstruktorzy danych wydają się być zupełnie inną bestią niż operator negacji.

Jaka jest teoria, która kryje się za możliwością definiowania typów egzystencjalnychforall zamiast nieistniejącegoexists?