Czy istnieje powód, dla którego nie możemy zapełnić typów danymi w DataKinds?

Question

Z DataKinds definicję jak

data KFoo = TFoo 

wprowadza rodzaj KFoo :: BOX i rodzaj TFoo :: KFoo. Dlaczego nie mogę następnie przejść do definiowania

data TFoo = CFoo 

takie, że CFoo :: TFoo, TFoo :: KFoo, KFoo :: BOX?

Czy wszyscy konstruktorzy muszą należeć do typu należącego do rodzaju *? Jeśli tak, dlaczego?

Edit: Nie pojawia się błąd, kiedy to zrobić, ponieważ konstruktorzy i rodzaje dzielić przestrzeń nazw, ale GHC pozwala konfliktów, ponieważ disambiguates nazwiska jak zwykłych typów, zamiast promowanych konstruktorów. Dokumenty mówią, aby poprzedzać prefiksem ', aby odnosić się do promowanego konstruktora. Kiedy zmieni drugiej linii do

data 'TFoo = CFoo 

pojawia się błąd

malformed głowy typu lub deklaracji klasy: Tfoo

Answer 1

Czy wszyscy konstruktorzy muszą należeć do typu który należy do rodzaju *?

Tak. Dokładnie to oznacza *: jest to rodzaj (podniesiony/zapakowany, nigdy nie jestem pewien co do tej części) typów Haskella. Rzeczywiście, wszystkie inne rodzaje nie są tak naprawdę rodzajami, chociaż mają one składnię type. Raczej * jest typem poziomu metypoziomu dla typów, a wszystkie pozostałe są typami na poziomie metatype dla rzeczy, które nie są typami, ale konstruktorami typu lub czymś zupełnie innym.

(Ponownie, istnieje również coś takiego rodzaju unboxed typu;. Te z pewnością są typy, ale myślę, że nie jest to możliwe dla data konstruktora)

Answer 2

Czy wszyscy konstruktorzy muszą należeć do typu, który należy do rodzaju *? Jeśli tak, dlaczego?

Najważniejszym powodem, dlaczego muszą być typu * (lub #) jest rozdzielenie faz zatrudniony przez GHC: DataKinds dostać usunięte podczas kompilacji. Możemy reprezentować ich środowiska wykonawczego jedynie pośrednio, poprzez zdefiniowanie singleton GADT typy danych:

{-# LANGUAGE DataKinds #-} 

data Nat = Z | S Nat 

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

Ale DataKind indeksów sami jeszcze nie istnieją środowiska wykonawczego. Różne rodzaje oferują prostą regułę separacji faz, która nie byłaby tak prosta w przypadku typów zależnych (nawet gdyby to znacznie uprościło programowanie na poziomie typu).