Cosa fa la parola chiave "forall" in Haskell/GHC?

https://stackoverflow.com/questions/3071136

28-09-2019
|

Domanda

Sto cominciando a capire come funziona il forall La parola chiave viene utilizzata nei cosiddetti "tipi esistenziali" come questi:

data ShowBox = forall s. Show s => SB s

Questo è solo un sottoinsieme, tuttavia, di come forall è usato e semplicemente non riesco a capire il suo utilizzo in cose come queste:

runST :: forall a. (forall s. ST s a) -> a

Oppure spiegare perché sono diversi:

foo :: (forall a. a -> a) -> (Char, Bool)
bar :: forall a. ((a -> a) -> (Char, Bool))

O il tutto RankNTypes cose...

Tendo a preferire un inglese chiaro e privo di termini tecnici piuttosto che i tipi di linguaggio normali negli ambienti accademici.La maggior parte delle spiegazioni che cerco di leggere al riguardo (quelle che posso trovare tramite i motori di ricerca) presentano questi problemi:

Sono incompleti.Spiegano una parte dell'uso di questa parola chiave (come "tipi esistenziali") che mi fa sentire felice finché non leggo il codice che la usa in un modo completamente diverso (come runST, foo E bar Sopra).
Sono densamente pieni di ipotesi che ho letto le ultime novità in qualunque ramo della matematica discreta, della teoria delle categorie o dell'algebra astratta sia popolare questa settimana.(Se non leggo mai la parola "consulta il giornale Qualunque cosa per i dettagli dell'implementazione" ancora una volta, sarà troppo presto.)
Sono scritti in modi che spesso trasformano anche concetti semplici in una grammatica e una semantica tortuosamente contorte e fratturate.

COSÌ...

Passiamo alla domanda vera e propria.Qualcuno può spiegare completamente il forall parola chiave in un inglese chiaro e semplice (o, se esiste da qualche parte, indica una spiegazione così chiara che mi sono persa) che non presuppone che io sia un matematico esperto di gergo?

Modificato per aggiungere:

Ci sono state due risposte eccezionali tra quelle di qualità superiore di seguito, ma sfortunatamente posso sceglierne solo una come migliore. La risposta di Norman era dettagliato e utile, spiegando le cose in un modo che mostrava alcune delle basi teoriche di forall e allo stesso tempo mostrandomi alcune delle sue implicazioni pratiche. la risposta di yairchu ha coperto un'area che nessun altro ha menzionato (variabili di tipo con ambito) e ha illustrato tutti i concetti con codice e una sessione GHCi.Se fosse possibile selezionarli entrambi come migliori, lo farei.Sfortunatamente non posso e, dopo aver esaminato attentamente entrambe le risposte, ho deciso che yairchu è leggermente in contrasto con quello di Norman a causa del codice illustrativo e della spiegazione allegata.Questo è un po' ingiusto, però, perché in realtà avevo bisogno di entrambe le risposte per capirlo fino in fondo forall non mi lascia con un vago senso di terrore quando lo vedo in una firma di tipo.

Soluzione

La partenza di Let con un esempio di codice:

foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b
foob postProcess onNothin onJust mval =
    postProcess val
    where
        val :: b
        val = maybe onNothin onJust mval

Questo codice non compila (errore di sintassi) in pianura Haskell 98. Si richiede una proroga per sostenere la parola chiave forall.

Esistono fondamentalmente 3 differenti utilizzi comuni per la parola forall (o almeno così sembra ), e ciascuno ha una propria estensione Haskell: ScopedTypeVariables, RankNTypes / Rank2Types, ExistentialQuantification.

Il codice di cui sopra non ottiene un errore di sintassi con uno di quelli abilitati, ma solo di tipo controlli con ScopedTypeVariables abilitato.

con mirino variabili di tipo:

variabili di tipo con ambito aiuta a specificare i tipi di clausole where codice all'interno. Rende il b nel val :: b lo stesso come il b in foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b.

Un punto di confusione : si può sentire che quando si omette l'forall da un tipo in realtà è ancora implicitamente lì. ( dalla risposta di Norman: "normalmente nelle lingue omettono il forall da tipi polimorfi "). Questa affermazione è corretta, ma si riferisce agli altri usi di forall, e non all'uso ScopedTypeVariables.

Classifica-N-Tipi:

La partenza di Let con quella mayb :: b -> (a -> b) -> Maybe a -> b è equivalente a mayb :: forall a b. b -> (a -> b) -> Maybe a -> b, eccezione per quando ScopedTypeVariables è attivato.

Questo significa che funziona per ogni a e b.

diciamo Let si vuole fare qualcosa di simile.

ghci> let putInList x = [x]
ghci> liftTup putInList (5, "Blah")
([5], ["Blah"])

Che cosa deve essere il tipo di questo liftTup? E 'liftTup :: (forall x. x -> f x) -> (a, b) -> (f a, f b). Per capire perché, cerchiamo di codice è:

ghci> let liftTup liftFunc (a, b) = (liftFunc a, liftFunc b)
ghci> liftTup (\x -> [x]) (5, "Hello")
    No instance for (Num [Char])
    ...
ghci> -- huh?
ghci> :t liftTup
liftTup :: (t -> t1) -> (t, t) -> (t1, t1)

"Hmm .. perché non GHC dedurre che la tupla deve contenere due dello stesso tipo? Diciamo che non devono essere"

-- test.hs
liftTup :: (x -> f x) -> (a, b) -> (f a, f b)
liftTup liftFunc (t, v) = (liftFunc t, liftFunc v)

ghci> :l test.hs
    Couldnt match expected type 'x' against inferred type 'b'
    ...

Hmm. ecco GHC non ci permette di applicare liftFunc su v perché v :: b e liftFunc vuole una x. Vogliamo davvero la nostra funzione per ottenere una funzione che accetta ogni possibile x!

{-# LANGUAGE RankNTypes #-}
liftTup :: (forall x. x -> f x) -> (a, b) -> (f a, f b)
liftTup liftFunc (t, v) = (liftFunc t, liftFunc v)

Quindi non è liftTup che funziona per tutti x, è la funzione che si ottiene che fa.

Esistenziale Quantificazione:

l'uso di Let un esempio:

-- test.hs
{-# LANGUAGE ExistentialQuantification #-}
data EQList = forall a. EQList [a]
eqListLen :: EQList -> Int
eqListLen (EQList x) = length x

ghci> :l test.hs
ghci> eqListLen $ EQList ["Hello", "World"]
2

Come è molto diverso da Rank-N-Tipi?

ghci> :set -XRankNTypes
ghci> length (["Hello", "World"] :: forall a. [a])
    Couldnt match expected type 'a' against inferred type '[Char]'
    ...

Con Rank-N-Tipi, forall a ha fatto sì che la vostra espressione deve soddisfare tutte le possibili as. Ad esempio:

ghci> length ([] :: forall a. [a])
0

Un elenco vuoto funziona come un elenco di qualsiasi tipo.

Quindi, con Esistenziale-Quantificazione, foralls nelle definizioni data significano che, il valore contenuto possono essere di qualsiasi tipo adatto, non che deve essere di tutti tipi adatti.

Altri suggerimenti

Può chiunque completamente spiegare la parola chiave forall in un inglese chiaro e semplice?

NO. (Beh, forse Don Stewart può farlo.)

Ecco gli ostacoli a una spiegazione semplice e chiara o forall:

È un quantificatore.È necessario avere almeno un po' di logica (calcolo dei predicati) per aver visto un quantificatore universale o esistenziale.Se non hai mai visto il calcolo dei predicati o non ti senti a tuo agio con i quantificatori (e ho visto studenti durante gli esami di abilitazione al dottorato che non si sentono a proprio agio), allora per te non c'è una spiegazione semplice di forall.
È un tipo quantificatore.Se non hai visto Sistema F e hai fatto un po' di pratica nello scrivere tipi polimorfici, scoprirai forall confuso.L'esperienza con Haskell o ML non è sufficiente, perché normalmente questi linguaggi omettono il file forall da tipi polimorfici.(A mio avviso, questo è un errore di progettazione del linguaggio.)
In Haskell in particolare, forall è usato in modi che trovo confusi.(Non sono un teorico dei tipi, ma il mio lavoro mi porta in contatto con a quantità della teoria dei tipi, e mi trovo abbastanza a mio agio.) Per me, la principale fonte di confusione è questa forall è usato per codificare un tipo con cui io stesso preferirei scrivere exists.È giustificato da un complicato isomorfismo di tipo che coinvolge quantificatori e frecce, e ogni volta che voglio capirlo, devo cercare le cose e elaborare io stesso l'isomorfismo.

Se non ti senti a tuo agio con l'idea di isomorfismo di tipo, o se non hai alcuna pratica nel pensare agli isomorfismi di tipo, questo uso di forall ti ostacolerà.
Mentre il concetto generale di forall è sempre lo stesso (è obbligatorio introdurre una variabile di tipo), i dettagli dei diversi usi possono variare in modo significativo.L’inglese informale non è uno strumento molto valido per spiegare le variazioni.Per capire veramente cosa sta succedendo, hai bisogno di un po’ di matematica.In questo caso la matematica rilevante si trova nel testo introduttivo di Benjamin Pierce Tipi e linguaggi di programmazione, che è un ottimo libro.

Per quanto riguarda i tuoi esempi particolari,

runST Dovrebbe farti male alla testa.I tipi di rango più alto (per tutti a sinistra di una freccia) si trovano raramente in natura.Vi incoraggio a leggere il documento che ha introdotto runST: "Thread di stato funzionale pigro".Questo è davvero un ottimo articolo e ti darà un'intuizione molto migliore per il tipo di runST in particolare e per i tipi di rango superiore in generale.La spiegazione occupa diverse pagine, è molto ben fatta e non cercherò di condensarla qui.
Prendere in considerazione
```
foo :: (forall a. a -> a) -> (Char,Bool)
bar :: forall a. ((a -> a) -> (Char, Bool))
```
Se chiamo bar, posso semplicemente scegliere qualsiasi tipo a che mi piace e posso passargli una funzione da type a digitare a.Ad esempio, posso passare la funzione (+1) o la funzione reverse.Puoi pensare a forall come dicendo "Ora posso scegliere il tipo".(La parola tecnica per scegliere il tipo è istanziando.)

Le restrizioni alle chiamate foo sono molto più stringenti:l'argomento a foo dovere essere una funzione polimorfica.Con quel tipo, le uniche funzioni a cui posso passare foo Sono id o una funzione che diverge sempre o presenta errori, come undefined.Il motivo è che con foo, IL forall è a sinistra della freccia, così come il chiamante di foo Non posso scegliere cosa a è—anzi è il implementazione Di foo quello deve scegliere cosa a È.Perché forall è a sinistra della freccia, anziché sopra la freccia come in bar, l'istanziazione avviene nel corpo della funzione anziché nel sito di chiamata.

Riepilogo: UN completare spiegazione del forall La parola chiave richiede la matematica e può essere compresa solo da qualcuno che ha studiato la matematica.Anche le spiegazioni parziali sono difficili da comprendere senza la matematica.Ma forse le mie spiegazioni parziali e non matematiche aiutano un po’.Vai a leggere Launchbury e Peyton Jones runST!

Addendum: Gergo "sopra", "sotto", "a sinistra di".Questi non hanno nulla a che fare con il testuale i modi in cui vengono scritti i tipi e tutto ciò che ha a che fare con gli alberi di sintassi astratta.Nella sintassi astratta, a forall prende il nome di una variabile di tipo e quindi c'è un tipo completo "sotto" il forall.Una freccia assume due tipi (tipo di argomento e tipo di risultato) e forma un nuovo tipo (il tipo di funzione).Il tipo di argomento è "a sinistra" della freccia;è il figlio sinistro della freccia nell'albero della sintassi astratta.

Esempi:

In forall a . [a] -> [a], il forall è sopra la freccia;ciò che è a sinistra della freccia è [a].
In
```
forall n f e x . (forall e x . n e x -> f -> Fact x f) 
              -> Block n e x -> f -> Fact x f
```
il tipo tra parentesi sarebbe chiamato "un forall a sinistra di una freccia".(Sto utilizzando tipi come questo in un ottimizzatore su cui sto lavorando.)

La mia risposta originale:

Qualcuno può spiegare completamente la parola chiave forall in modo chiaro, semplice English

Come Norman indica, è molto difficile dare una chiara, semplice spiegazione inglese di un termine tecnico da teoria dei tipi. Stiamo tutti cercando però.

C'è veramente solo una cosa da ricordare di 'forall': si lega a tipi certo margine . Una volta capito questo, tutto è abbastanza facile. È il equivalente di 'lambda' (o una forma di 'lasciare') a livello tipo - Norman Ramsey utilizza il concetto di "sinistra" / "al di sopra" per trasmettere questo stesso concetto di portata in la sua risposta eccellente .

La maggior parte dei usi di 'forall' sono molto semplici, e si possono trovare li introdotti nel il GHC Manuale d'uso, S7.8 ., In particolare l'eccellente S7.8.5 su nidificato forme di 'forall'.

In Haskell, di solito togliere l'legante per i tipi, quando il tipo è universalmente quanitified, in questo modo:

length :: forall a. [a] -> Int

è equivalente a:

length :: [a] -> Int

Questo è tutto.

Dal momento che è possibile associare le variabili di tipo ora in una certa portata, si può avere scopi altri al livello superiore ( " universalmente quantificata "), come il vostro primo esempio, dove la variabile tipo è visibile solo all'interno della struttura dati. Questo permette per i tipi di nascosto ( " tipi esistenziali "). Oppure possiamo avere arbitraria nidificazione di attacchi ( "rango tipi N").

Per comprendere a fondo i sistemi di tipo, è necessario imparare un po 'il gergo. Quello è la natura della scienza informatica. Tuttavia, usi semplici, come sopra, dovrebbero essere in grado di essere colto in modo intuitivo, attraverso l'analogia con 'lasciare' a livello di valore. UN grande introduzione è Launchbury e Peyton Jones .

Si stanno densamente ricco di assunzioni che ho letto l'ultimo di qualunque ramo della matematica discreta, teoria delle categorie o algebra astratta è popolare questa settimana. (Se non ho mai letto le parole "consultare la carta qualunque per i dettagli di implementazione" ancora una volta, sarà troppo presto.)

Er, e che dire di semplice logica del primo ordine? forall è abbastanza chiaramente in riferimento a universale quantificazione , e in questo contesto il termine esistenziale ha più senso e, anche se sarebbe meno imbarazzante se ci fosse una parola chiave exists. Sia che la quantificazione è effettivamente universale o esistenziale dipende dal posizionamento del quantificatore rispetto al punto in cui le variabili sono utilizzati su quale lato di una freccia funzione ed è tutto un po 'di confusione.

Quindi, se questo non risolve il problema, o se semplicemente non ti piace la logica simbolica, da una prospettiva di programmazione-ish più funzionale si può pensare di variabili di tipo come solo essere (implicito) tipo parametri alla funzione. Funzioni che assumono parametri di tipo in questo senso sono tradizionalmente scritti usando un lambda capitale per qualsiasi motivo, che scriverò qui come /\.

Quindi, si consideri la funzione id:

id :: forall a. a -> a
id x = x

possiamo riscrivere come lambda, spostando il "parametro di tipo" fuori della firma tipo e l'aggiunta di tipo inline annotazioni:

id = /\a -> (\x -> x) :: a -> a

Ecco la stessa cosa fatta a const:

const = /\a b -> (\x y -> x) :: a -> b -> a

Quindi, la vostra funzione bar potrebbe essere qualcosa di simile:

bar = /\a -> (\f -> ('t', True)) :: (a -> a) -> (Char, Bool)

Si noti che il tipo di funzione data a bar come argomento dipende dal parametro tipo di bar. Prendere in considerazione se si ha qualcosa di simile a questo, invece:

bar2 = /\a -> (\f -> (f 't', True)) :: (a -> a) -> (Char, Bool)

Qui bar2 sta applicando la funzione di qualcosa di tipo Char, in modo da dare bar2 qualsiasi tipo di parametro diverso Char causerà un errore di tipo.

D'altra parte, ecco cosa foo potrebbe essere simile:

foo = (\f -> (f Char 't', f Bool True))

A differenza bar, foo realtà non accetta parametri di tipo a tutti! Ci vuole una funzione che si un parametro di tipo, quindi applica tale funzione a due diverso tipi.

Quindi, quando si vede un forall in una firma di tipo, basta pensare a come un espressione lambda per tipo firme . Proprio come lambda regolari, l'ambito di forall si estende fino alla destra possibile, fino a parentesi che racchiude, e proprio come le variabili legate in un lambda regolare, le variabili di tipo legati da un forall sono solo in ambito entro l'espressione quantificata.

Post scriptum : Forse si potrebbe chiedere - ora che stiamo pensando di funzioni che assumono parametri di tipo, perché non possiamo fare qualcosa di più interessante con quei parametri di metterli in una firma di tipo ? La risposta è che possiamo!

Una funzione che mette tipo variabili insieme con un'etichetta e ritorna un nuovo tipo è un tipo costruttore , che si potrebbe scrivere qualcosa di simile:

Either = /\a b -> ...

Ma avremmo bisogno completamente nuova notazione, perché il modo in cui un tale tipo è scritto, come Either a b, è già suggestiva di "applicare la funzione Either a questi parametri".

D'altra parte, una funzione che sorta di "abbinamento modello" a suoi parametri di tipo corrispondente valori diversi per i diversi tipi, è un metodo di una classe tipo . Una leggera espansione per la mia sintassi /\ suggerisce sopra qualcosa di simile a questo:

fmap = /\ f a b -> case f of
    Maybe -> (\g x -> case x of
        Just y -> Just b g y
        Nothing -> Nothing b) :: (a -> b) -> Maybe a -> Maybe b
    [] -> (\g x -> case x of
        (y:ys) -> g y : fmap [] a b g ys 
        []     -> [] b) :: (a -> b) -> [a] -> [b]

Personalmente, credo di preferire syn effettiva di Haskellfiscale ...

Una funzione che "le partite del modello" i suoi parametri di tipo e restituisce un arbitrarie, tipo esistente è un di tipo familiare o dipendenza funzionale - nel primo caso, ancora già sembra un grande affare come una definizione di funzione.

Ecco una spiegazione rapida e sporca in termini semplici che probabilmente conoscerai già.

IL forall la parola chiave è in realtà utilizzata solo in un modo in Haskell.Significa sempre la stessa cosa quando lo vedi.

Quantificazione universale

UN tipo universalmente quantificato è un tipo del modulo forall a. f a.Un valore di quel tipo può essere pensato come una funzione ci vuole un tipo a come argomento e restituisce a valore di tipo f a.Tranne che in Haskell questi argomenti di tipo vengono passati implicitamente dal sistema di tipo.Questa "funzione" deve darti lo stesso valore indipendentemente dal tipo che riceve, quindi il valore lo è polimorfico.

Consideriamo ad esempio il tipo forall a. [a].Un valore di quel tipo assume un altro tipo a e ti restituisce un elenco di elementi dello stesso tipo a.Naturalmente esiste una sola implementazione possibile.Dovrebbe darti la lista vuota perché a potrebbe essere assolutamente di qualsiasi tipo.La lista vuota è l'unico valore della lista che è polimorfico nel suo tipo di elemento (poiché non ha elementi).

O il tipo forall a. a -> a.Il chiamante di tale funzione fornisce sia un tipo a e un valore di tipo a.L'implementazione deve quindi restituire un valore dello stesso tipo a.C'è ancora una sola possibile implementazione.Dovrebbe restituire lo stesso valore che gli è stato assegnato.

Quantificazione esistenziale

UN tipo esistenzialmente quantificato avrebbe la forma exists a. f a, se Haskell supportasse quella notazione.Un valore di quel tipo può essere pensato come un paio (o un "prodotto") costituito da un tipo a e un valore di tipo f a.

Ad esempio, se hai un valore di tipo exists a. [a], hai un elenco di elementi di qualche tipo.Potrebbe essere di qualsiasi tipo, ma anche se non sai di cosa si tratta c'è molto che potresti fare per un elenco del genere.Potresti invertirlo, oppure potresti contare il numero di elementi o eseguire qualsiasi altra operazione sull'elenco che non dipenda dal tipo di elementi.

Ok, aspetta un attimo.Perché Haskell usa forall per denotare un tipo "esistenziale" come il seguente?

data ShowBox = forall s. Show s => SB s

Può creare confusione, ma in realtà descrive il tipo del costruttore di dati SB:

SB :: forall s. Show s => s -> ShowBox

Una volta costruito, puoi pensare a un valore di tipo ShowBox come composto da due cose.È un tipo s insieme a un valore di tipo s.In altre parole, è un valore di tipo esistenzialmente quantificato. ShowBox potrebbe davvero essere scritto come exists s. Show s => s, se Haskell supportasse quella notazione.

runST e amici

Detto questo, in cosa differiscono?

foo :: (forall a. a -> a) -> (Char,Bool)
bar :: forall a. ((a -> a) -> (Char, Bool))

Prendiamo prima bar.Ci vuole un tipo a e una funzione di tipo a -> a, e produce un valore di tipo (Char, Bool).Potremmo scegliere Int come il a e assegnargli una funzione di tipo Int -> Int Per esempio.Ma foo è diverso.Si richiede che l'attuazione di foo essere in grado di passare qualsiasi tipo desideri alla funzione che gli diamo.Quindi l'unica funzione che potremmo ragionevolmente dargli è id.

Ora dovremmo essere in grado di affrontare il significato del tipo di runST:

runST :: forall a. (forall s. ST s a) -> a

COSÌ runST deve essere in grado di produrre un valore di tipo a, non importa quale tipo diamo come a.Per fare ciò, è necessario un argomento di tipo forall s. ST s a che sotto il cofano è solo una funzione di tipo forall s. s -> (a, s).Tale funzione deve quindi essere in grado di produrre un valore di tipo (a, s) non importa quale sia il tipo di implementazione runST decide di dare come s.

Ok, e allora?Il vantaggio è che questo pone un vincolo al chiamante runST in questo il tipo a non può coinvolgere il tipo s affatto.Non puoi passargli un valore di tipo ST s [s], Per esempio.Ciò che ciò significa in pratica è che l'implementazione di runST è libero di eseguire mutazioni con il valore di type s.Il sistema di tipi garantisce che questa mutazione sia locale all'implementazione di runST.

Il tipo di runST è un esempio di a tipo polimorfico di rango 2 perché il tipo del suo argomento contiene a forall quantificatore.Il tipo di foo sopra è anch'esso di rango 2.Un tipo polimorfico ordinario, come quello di bar, è di rango 1, ma diventa di rango 2 se i tipi di argomenti devono essere polimorfici, con i propri forall quantificatore.E se una funzione accetta argomenti di rango 2, il suo tipo sarà di rango 3 e così via.In generale, un tipo che accetta argomenti polimorfici di rango n ha rango n + 1.

Il motivo per cui ci sono diversi usi di questa parola chiave è che è effettivamente utilizzato in almeno due diverse estensioni di sistema Tipo:. Tipi più alto rango, e esistenziali

E 'probabilmente meglio solo per leggere e capire queste due cose separatamente, piuttosto che cercare di ottenere una spiegazione del motivo per cui 'forall' è un bit appropriato della sintassi in entrambi allo stesso tempo.

Qualcuno può spiegare completamente la parola chiave forall in modo chiaro, semplice inglese (o, se esiste qualche parte, scegliere una spiegazione così chiara che ho perso) che non assumo io sono un matematico immerso nel gergo?

Ho intenzione di cercare di spiegare solo il significato e forse l'applicazione della forall nel contesto dei suoi sistemi di tipo Haskell e.

Ma prima di capire che vorrei di indirizzarvi verso un discorso molto accessibile e piacevole da Runar Bjarnason dal titolo " Vincoli Liberate, le libertà Constrain ". Il discorso è pieno di esempi di casi d'uso reali così come esempi in Scala a sostegno di questa affermazione, anche se non menziona forall. Cercherò di spiegare il punto di vista forall di seguito.

                CONSTRAINTS LIBERATE, LIBERTIES CONSTRAIN

E 'molto importante per digerire e credere questa dichiarazione per procedere con la seguente spiegazione, quindi vi esorto a guardare il discorso (almeno una parte di esso).

Ora un esempio molto comune, che mostra l'espressività del sistema di tipo Haskell è questo tipo di firma:

foo :: a -> a

Si dice che in questo tipo di firma, c'è solo una funzione in grado di soddisfare questo tipo e che è la funzione identity o ciò che è più comunemente conosciuta id.

Nelle fasi iniziali di apprendimento me Haskell, mi sono sempre chiesto il seguito funzioni:

foo 5 = 6

foo True = False

entrambi soddisfano la firma tipo sopra, allora perché la gente Haskell sostengono che è solo id che soddisfa il tipo di firma?

Questo è perché c'è un forall implicita nascosto nella firma tipo. Il tipo effettivo è:

id :: forall a. a -> a

Così, ora torniamo alla dichiarazione: Vincoli liberano, libertà vincolo

Traducendo che al tipo di sistema, questa affermazione diventa:

Un vincolo a livello di tipo, diventa una libertà a livello termine

Una libertà a livello di tipo, diventa un vincolo a livello termine

Cerchiamo di dimostrare la prima dichiarazione:

Un vincolo a livello di tipo ..

Quindi, mettere un vincolo sulla nostra firma di tipo

foo :: (Num a) => a -> a

diventa una libertà a livello termine ci dà la libertà o la flessibilità di scrivere tutte queste

foo 5 = 6
foo 4 = 2
foo 7 = 9
...

Lo stesso può essere osservato vincolando a con qualsiasi altro typeclass etc

Quindi, ora ciò che questo tipo di firma: foo :: (Num a) => a -> a traduce è:

∃a , st a -> a, ∀a ∈ Num

Questo è noto come la quantificazione esistenziale, che si traduce in esiste alcuni casi di a per cui una funzione quando alimentato qualcosa di tipo a rendimenti qualcosa dello stesso tipo, e quei casi appartengono tutti alla serie di numeri.

Quindi possiamo vedere l'aggiunta di un vincolo (che a dovrebbe appartenere alla serie di numeri), libera il termine livello di avere più possibili implementazioni.

Ora venendo alla seconda affermazione e quella che porta in realtà la spiegazione di forall:

una libertà a livello di tipo, diventa un vincolo a livello termine

Quindi, ora cerchiamo di liberare la funzione a livello di tipo:

foo :: forall a. a -> a

Ora, questo si traduce in:

∀a , a -> a

che significa che l'attuazione di questo tipo firma dovrebbe essere tale che sia a -> a per tutte le circostanze.

Così ora questo comincia noi vincolante a livello termine. Non possiamo più scrivere

foo 5 = 7

perché questa implementazione non soddisferebbe se mettiamo a come Bool. a può essere un Char o un [Char]o un tipo di dati personalizzato. In tutte le circostanze deve restituire qualcosa del tipo simile. Questa libertà a livello di tipo è il cosiddetto universale Quantificazione e l'unica funzione che può soddisfare questo è

foo a = a

che è comunemente noto come funzione identity

Quindi forall è un liberty a livello di tipo, il cui scopo è quello di effettiva constrain il termine livello di una particolare implementazione.

Come è esistenziale esistenziale?

Con esistenziale-Quantificazione, foralls nelle definizioni data significano che, il valore contenuto possono essere qualsiasi tipo adatto, non che deve essere di tutti tipi adatti. - risposta di Yachiru

Una spiegazione del perché forall nelle definizioni data sono isomorfi a (exists a. a) (pseudo-Haskell) può essere trovato in di Wikibooks "Haskell / tipi quantificate esistenzialmente" .

Di seguito una breve sintesi testualmente:

data T = forall a. MkT a -- an existential datatype
MkT :: forall a. a -> T -- the type of the existential constructor

Quando pattern-matching / decostruzione MkT x, qual è il tipo di x?

foo (MkT x) = ... -- -- what is the type of x?

x può essere di qualsiasi tipo (come indicato nella forall), e così il suo tipo è:

x :: exists a. a -- (pseudo-Haskell)

Pertanto, i seguenti sono isomorfi:

data T = forall a. MkT a -- an existential datatype
data T = MkT (exists a. a) -- (pseudo-Haskell)

forall significa forall

Il mio semplice interpretazione di tutto questo, è che "forall veramente significa 'per tutti'". Una distinzione importante da fare è l'impatto del forall sulla definizione contro la funzione applicazione .

A forall intende il definizione del valore o funzione deve essere polimorfico.

Se cosa che viene definita una polimorfico valore , significa che il valore deve essere valido per tutti a adatto, che è abbastanza restrittivo.

Se cosa che viene definita una polimorfico funzione , allora significa che la funzione deve essere valida per tutti a adatto, che non è quello restrittivo perché, proprio perché la funzione è polimorfica no significa che il parametro di essere applicare deve essere polimorfico. Cioè, se la funzione è valida per tutti a, quindi inversamente qualsiasi a adatta può essere applicare alla funzione. Tuttavia, il tipo di parametro può essere scelto soltanto una volta nella definizione della funzione.

Se un forall è dentro il tipo di parametro funzionale (cioè, un Rank2Type) allora significa il applicare parametro deve essere veramente polimorfica, per coerenza con l'idea di mezzi forall definizione è polimorfico. In questo caso, il tipo di parametro può essere scelto più di una volta nella definizione della funzione ( "ed è scelto dal implementazione della funzione ", come fuori punte da Norman )

Quindi, il motivo per cui le definizioni esistenziale data permette qualsiasi a è perché il costruttore dei dati è un polimorfico Funzione :

MkT :: forall a. a -> T

tipo di MKT :: a -> *

Il che significa che qualsiasi a può essere applicato alla funzione. Al contrario di, diciamo, un polimorfico Valore :

valueT :: forall a. [a]

tipo di Valuet :: a

Il che significa che la definizione di Valuet deve essere polimorfico. In questo caso, valueT può essere definita come elenco [] vuota di tutti i tipi.

[] :: [t]

Differenze

Anche se il significato per forall è coerente in ExistentialQuantification e RankNType, esistenziali ha una differenza in quanto il costruttore data può essere utilizzato in pattern matching. Come documentato nel GHC guida :

Quando pattern matching, ogni pattern match introduce un nuovo, distinto, tipo per ciascuna variabile di tipo esistenziale. Questi tipi non possono essere unificati con qualsiasi altro tipo, né possono fuoriuscire dall'ambito della partita modello.

Autorizzato sotto: CC-BY-SA insieme a attribuzione

Non affiliato a StackOverflow