Warum gibt es kein "Exist" -Schlüsselwort in Haskell für existenzielle Quantifizierung?

Question

Nach der GHC Dokumentation, da die folgende Erklärung ab:

data Foo = forall a. MkFoo a (a -> Bool) 
      | Nil 

dann

MkFoo :: forall a. a -> (a -> Bool) -> Foo 

ist (fast) isomorph auf die folgende pseudo-Haskell Erklärung

MkFoo :: (exists a . (a, a -> Bool)) -> Foo 

, Deshalb gibt ist nicht für ein getrenntes "Exist" Schlüsselwort erforderlich. Denn:

Haskell Programmierer können sicher an die üblichen universellen quantifizierten Typ wie oben angegeben denken.

Aber ich bin mir nicht sicher, was das bedeutet. Kann mir bitte jemand erklären, warum wir den universellen Quantifizierer verwenden können, um die existentielle Quantifizierung auszudrücken?

Answer 1

In der Logik (klassische oder intuitionistic), die Formeln

(exists x. p x) -> q 
forall x. (p x -> q) 

gleichwertig sind (beachten Sie, dass q nicht auf x oben abhängt). Dies kann verwendet werden, um die existenzielle Quantifizierung in Form einer universellen Quantifizierung auszudrücken, vorausgesetzt, das Existenzielle liegt auf der linken Seite implizit. (Hier ist eine klassische proof.)

In der funktionalen Programmierung können Sie das gleiche erreichen. Statt

-- Pseudo-Haskell follows 
f :: (exists a. (a, a->Int)) -> Int 
f (x,h) = h x 

schreiben, können wir

-- Actual Haskell 
f :: forall a. (a, a->Int) -> Int 
f (x,h) = h x 

verwenden, so können wir ohne existenzielle Quantifizierung tun, zumindest in Fällen wie dem oben.

Existenzielle Quantifizierung wird immer noch benötigt, wenn sie nicht auf der linken Seite eines Pfeils auftritt. Zum Beispiel

g :: exists a. (a, a->Int) 
g = (2 :: Int, \x -> x+3) 

Leider hat sich Haskell entschieden, diese Typen nicht einzuschließen. Wahrscheinlich wurde diese Entscheidung getroffen, um zu verhindern, dass das bereits hoch entwickelte System zu komplex wird.

Dennoch hat Haskell existenzielle Datentypen, die nur einen Konstruktor um das Existentialumwickeln müssen. Zum Beispiel GADT Syntax verwenden, können wir schreiben:

data Ex where 
    E :: forall a. (a, a->Int) -> Ex 
g :: Ex 
g = E (2 :: Int, \x -> x+3) 

Abschließend möchte ich hinzufügen, dass Existenziale kann auch durch Rang-2-Typen und Fortgang simuliert werden:

g :: forall r. (forall a. (a, a->Int) -> r) -> r 
g k = k (2 :: Int, \x -> x+3) 

Answer 2

Wenn Sie sich die Art von Datenkonstruktoren ansehen, werden Sie feststellen, dass wir -> ähnlich verwenden, um irgendwie Produkt zu meinen. Z.B.

(:) :: a -> [a] -> [a] 

wirklich bedeutet, dass wir (:) verwenden eine azusammen [a] mit eine Liste von Typ [a] und liefern eine Liste der Art zu packen.

In Ihrem Beispiel bedeutet die Verwendung von forall einfach, dass MkFoo als Konstruktor bereit ist, einen beliebigen Typ a zu packen. Wenn Sie (exists a . (a, a -> Bool)) -> Foo in der GHC-Dokumentation lesen, sollten Sie es als eine unverletzte Version des ursprünglichen Typs MkFoo betrachten. Die entsprechende unverdünnte Version von (:) wäre (a, [a]) -> [a].

Answer 3

Das erste, was zu bemerken ist, dass die forall quantifier auf der rechten Seite des Gleichheitszeichens angezeigt wird, so wird es mit einem Daten Konstruktors zugeordnet (nicht Art): MkFoo. So sagt der Typ Foo nichts über a.

Wir stoßen wieder auf a, wenn wir versuchen, Muster auf Werte vom Typ Foo zu pattern. An diesem Punkt werden Sie so gut wie nichts über die Komponenten von MkFoo wissen, außer dass sie existieren (dort muss ein Typ zum Aufruf MkFoo existieren) und dass die erste Komponente als ein Argument für die zweite Komponente verwendet werden kann, die eine Funktion ist:

f :: Foo -> Bool 
f (MkFoo val fn) = fn val