Perché: k [False] genera un errore in GHCI?

Question

Sono confuso circa l'errore che ho ricevuto al termine della sessione di seguito:

$ ghci 
GHCi, version 7.10.2: http://www.haskell.org/ghc/ :? for help 
Ok, modules loaded: Main. 
*Main> :set -XDataKinds 

*Main> :t [False, True] 
[False, True] :: [Bool] 

*Main> :t [False] 
[False] :: [Bool] 

*Main> :k [False, True] 
[False, True] :: [Bool] 

*Main> :k [False] 

<interactive>:1:2: 
    Expected kind ‘*’, but ‘False’ has kind ‘Bool’ 
    In a type in a GHCi command: [False] 

Perché l'errore?

---

sperimentazione Future rivela:

*Main> :k [Int] 
[Int] :: * 

*Main> :k [Int, Int] 
[Int, Int] :: [*] 

[Int] può aver abitato valori quindi è di tipo *, ma rende anche senso che è di tipo [*].

punti dati

---

un po 'più:

*Main> :k [] 
[] :: * -> * 

*Main> :k [Bool] 
[Bool] :: * 

Answer 1

Se si dispone di elenchi di livello tipo con un solo elemento, GHC pensa che non è un elenco sollevato, ma un normale tipo di elenco costruttore applicata a un certo tipo di tipo *.

Si dovrebbe anteporre la lista con un apostrofo per selezionare in modo esplicito per gli elenchi sollevato:

> :k '[False] 
'[False] :: [Bool] 

Allo stesso modo con le liste vuote:

> :k '[] 
'[] :: [k] 

Answer 2

Come si nota:

[Int] può avere valori abitati quindi è di tipo *, ma ha anche senso che è di tipo [*]

Cosa avete scoperto è che DataKinds c'è ambiguità in alcune espressioni del tipo se si consente semplicemente di valore espressioni per essere sollevati al livello tipo. Molto spesso viene fornito questo elenco a causa dell'uso di parentesi quadre per entrambi i letterali di elenco e i tipi di elenco, ma non è interamente specifico per le liste.

Fondamentalmente, il codice sorgente testo [False] potrebbe fare riferimento tre cose diverse:

1. Elenco sintassi letterale per una lista livello valore, contenente un unico elemento che è il valore False
2. Il tipo elenco costruttore applicato al tipoFalse
3. Sintassi letterale di lista per un elenco di livello di tipo, contenente un singolo elemento che è il tipoFalse

Senza DataKinds terzo significato non esiste, per cui il compilatore potrebbe sempre usare la sua conoscenza contestuale se il codice sorgente testo [False] si verificava in un'espressione tipo o un'espressione di valore. Ma entrambi i casi 2 e 3 si verificano nelle espressioni di tipo, quindi questo non aiuta.

In questo caso possiamo vedere che [False] come tipo "elenco delle cose di tipo False" non ha alcun senso, perché il costruttore [] tipo può essere applicato solo a cose del genere *. Ma il compilatore deve sapere cosa sei cercando di dire prima che possa digitare/tipo controllare le cose per vedere se è coerente; non vogliamo davvero che provi diverse possibili interpretazioni e tipo/tipo controllandoli tutti, accettando in silenzio se uno di loro funziona. E comunque con un piccolo sforzo (sulla falsariga di definire nomi di tipi adatti e/o usare PolyKinds per costruire costruttori di tipi che accettano cose di più tipi) si può arrivare a una situazione in cui un pezzo di testo sorgente ha tutti e 3 i tipi di significato che ho delineato sopra, e tutti e 3 potrebbero essere compilati senza errori.

Così, per risolvere l'ambiguità (senza interrompere la sintassi esistente come [Int] per "elenco delle cose di tipo Int") GHC adotta la regola che le ordinarie costruttori di tipo non alzate la precedenza. Quindi [False] in realtà non corrisponde a significa un elenco di singleton di livello tipo; indica solo il tipo di "elenco di cose di tipo False" (senza senso), che genera l'errore di tipo che vedi.

Ma DataKinds introduce anche la sintassi per richiedere esplicitamente l'altro significato; se si precede qualsiasi costruttore di tipi con un apostrofo, GHC sa che si sta riferendo alla versione revocata del costruttore di valori, non a un costruttore di tipo non revocato con lo stesso nome. Per esempio:

Prelude> :k 'False 
'False :: Bool 

E allo stesso modo, virare un apostrofo sulla parte anteriore della lista la sintassi letterale dice esplicitamente che si sta scrivendo un elenco di tipo a livello letterale, non scrivere un tipo di elenco, anche se la lista ha un solo articolo. Quindi:

Prelude> :k '[False] 
'[False] :: [Bool] 

Prelude> :k '[Int] 
'[Int] :: [*] 

È simile può utilizzare per distinguere tra il tipo di elenco costruttore di tipo * -> * e l'elenco tipo di livello vuota:

Prelude> :k [] 
[] :: * -> * 
Prelude> :k '[] 
'[] :: [k]