Perché non esiste una parola chiave "esistente" in Haskell per la quantificazione esistenziale?

Question

Secondo la documentazione GHC, data la seguente dichiarazione:

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

poi

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

Is (quasi) isomorfa alla seguente dichiarazione pseudo-Haskell

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

Pertanto, non vi non è necessario per una parola chiave "esistente" separata. Perché:

I programmatori Haskell possono tranquillamente pensare al tipo ordinario universalmente quantificato sopra indicato.

Ma non sono sicuro di cosa significhi. Qualcuno può spiegarmi perché possiamo usare il quantificatore universale per esprimere quantificazione esistenziale?

Answer 1

Nella logica (classico o intuizionistici), le formule

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

sono equivalenti (si noti che q non dipende x sopra). Questo può essere usato per esprimere la quantificazione esistenziale in termini di quantificazione universale, a patto che le menzogne ​​esistenziali a sinistra siano implicite. (Ecco un classico proof.)

Nella programmazione funzionale, è possibile ottenere lo stesso risultato. Invece di scrivere

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

possiamo usare

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

in modo che possiamo fare a meno di quantificazione esistenziale, almeno in casi come quello di cui sopra.

La quantificazione esistenziale è ancora necessaria quando si verifica non a sinistra di una freccia. Ad esempio,

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

Ahimè, Haskell ha scelto di non includere questi tipi. Probabilmente, questa scelta è stata fatta per mantenere il sistema di tipo già sofisticato dal diventare troppo complesso.

Ancora, Haskell ha tipi di dati esistenziali, che richiedono solo di avvolgere/scartare un costruttore attorno all'esistente. Ad esempio, utilizzando la sintassi GADT, possiamo scrivere:

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

Infine, permettetemi di aggiungere che esistenziali possono essere simulate da rango-2 tipi e continuazione-passing:

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

Answer 2

Se si osserva il tipo di costruttori di dati, si noterà che analogamente si utilizza -> per un prodotto in qualche modo significativo. Per esempio.

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

significa davvero che stiamo utilizzando (:) mettere in valigia un ainsieme con un elenco di tipo [a] e fornire un elenco di tipo [a].

Nel tuo esempio, l'uso di forall significa semplicemente che MkFoo, come costruttore, è disposto a confezionare qualsiasi tipo a. Quando leggi (exists a . (a, a -> Bool)) -> Foo nella documentazione di GHC, dovresti pensare a una versione non corta del tipo originale di MkFoo. La corrispondente versione non corazzata di (:) sarebbe (a, [a]) -> [a].

Answer 3

La prima cosa da notare è che il quantificatore forall appare sul lato destro del segno di uguale, quindi è associato con un costruttore di dati (non digitare): MkFoo. Pertanto, il tipo Foo non dice nulla su a.

Incontriamo di nuovo a quando cerchiamo di eseguire lo schema di corrispondenza sui valori di tipo Foo. A quel punto non conoscerai praticamente nulla dei componenti di MkFoo, tranne che sono esistenti (deve esistere un tipo utilizzato per chiamare MkFoo) e che il primo componente può essere utilizzato come argomento per il secondo componente, che è una funzione:

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