DasHaskell Wiki erklärt gut, wie man existenzielle Typen benutzt, aber ich kann die Theorie dahinter nicht recht verstehen.

Betrachten Sie dieses Beispiel eines existenziellen Typs:

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

um einen Typwrapper für Dinge zu definieren, die wir in einen umwandeln könnenString. Das Wiki erwähnt das, was wirJa wirklich definieren wollen, ist ein Typ wie

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

d.h. ein wahrer "existentieller" Typ - lose denke ich, dass dies den Datenkonstruktor sagtS nimmt jeden Typ an, für den aShow Beispielexistiert und umhüllt es ". In der Tat könnten Sie wahrscheinlich eine GADT wie folgt schreiben:

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

Ich habe nicht versucht, das zu kompilieren, aber es scheint, als ob es funktionieren sollte. Für mich entspricht die GADT offensichtlich dem Code (2), den wir schreiben möchten.

Mir ist jedoch völlig unklar, warum (1) gleichbedeutend mit (2) ist. Warum dreht das Verschieben des Datenkonstruktors nach außen dasforall In einexists?

Das nächste, was mir einfällt, sindDe Morgans Gesetze in der Logik, wo das Vertauschen der Reihenfolge einer Negation und eines Quantifizierers existenzielle Quantifizierer in universelle Quantifizierer verwandelt und umgekehrt:

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

Aber Datenkonstruktoren scheinen ein ganz anderes Biest zu sein als der Negationsoperator.

Welche Theorie steckt hinter der Fähigkeit, existenzielle Typen mit zu definieren?forall anstelle des Nichtexistentenexists?