C'è un motivo per cui non è possibile popolare i tipi con DataKinds?

Question

Con DataKinds, una definizione come

data KFoo = TFoo 

introduce il tipo KFoo :: BOX e il tipo TFoo :: KFoo. Perché non posso poi passare a definire

data TFoo = CFoo 

tale che CFoo :: TFoo, TFoo :: KFoo, KFoo :: BOX?

Tutti i costruttori devono appartenere a un tipo che appartiene al tipo *? Se è così, perché?

Edit: Non ottengo un errore quando faccio questo, perché i costruttori e tipi condividono uno spazio dei nomi, ma GHC, autorizza i conflitti perché disambigua nomi come tipi normali, piuttosto che costruttori promossi. I documenti dicono di prefisso con un ' per fare riferimento al costruttore promosso. Quando cambio che seconda linea per

data 'TFoo = CFoo 

ottengo l'errore

valido capo del tipo o dichiarazione di classe: TFoo

Answer 1

fare tutti i costruttori hanno bisogno di appartenere a un tipo quello appartiene al tipo *?

Sì. Questo è esattamente ciò che significa *: è il tipo di (tipo sollevato/inscatolato, non sono mai sicuro di quella parte) Haskell. In realtà tutti gli altri tipi non sono in realtà tipi di tipi anche se condividono la sintassi type. Piuttosto * è il tipo a livello metatype per i tipi e tutti gli altri tipi sono tipi a livello metatype per cose che non sono tipi ma costruttori di tipi o qualcosa di completamente diverso.

(Anche in questo caso, c'è anche qualcosa su unboxed tipo genere;. Quelli sono certamente i tipi, ma credo che questo non è possibile per un costruttore data)

Answer 2

fare tutti i costruttori hanno bisogno di appartenere a un tipo che appartiene al genere *? Se è così, perché?

La ragione più importante per cui devono essere di tipo * (o #) è la separazione di fase impiegato da GHC: DataKinds get cancellati durante la compilazione. Siamo in grado di rappresentarli Runtime solo indirettamente, attraverso la definizione di Singleton GADT tipi di dati:

{-# LANGUAGE DataKinds #-} 

data Nat = Z | S Nat 

data SNat n where 
    SZ :: SNat Z 
    SS :: SNat n -> SNat (S n) 

Ma la DataKind indici stessi ancora non esistono runtime. I vari tipi offrono una semplice regola per la separazione di fase, che non sarebbe così semplice con i tipi dipendenti (anche se potrebbe potenzialmente semplificare notevolmente la programmazione a livello di caratteri).