種類列表究竟如何工作？

Question

最近我一直在閱讀vinyl，它使用奇怪的「種類列表」有點類型。閱讀種類和乙烯基一點後，我已經得到了一定程度上的其中一個直觀的瞭解，我已經能夠破解起來這

{-# LANGUAGE DataKinds, 
      TypeOperators, 
      FlexibleInstances, 
      FlexibleContexts, 
      KindSignatures, 
      GADTs #-} 
module Main where 

-- from the data kinds page, with HCons replaced with :+: 
data HList :: [*] -> * where 
    HNil :: HList '[] 
    (:+:) :: a -> HList t -> HList (a ': t) 

infixr 8 :+: 


instance Show (HList '[]) where 
    show _ = "[]" 
instance (Show a, Show (HList t)) => Show (HList (a ': t)) where 
    show (x :+: xs) = show x ++ " : " ++ show xs 

class ISum a where 
    isum :: Integral t => a -> t 

instance ISum (HList '[]) where 
    isum _ = 0 


instance (Integral a, ISum (HList t)) => ISum (HList (a ': t)) where 
    isum (x :+: xs) = fromIntegral x + isum xs 

-- explicit type signatures just to check if I got them right 
alist :: HList '[Integer] 
alist = (3::Integer) :+: HNil 

blist :: HList '[Integer,Int] 
blist = (3::Integer) :+: (3::Int) :+: HNil 

main :: IO() 
main = do 
    print alist 
    print (isum alist :: Int) 
    print blist 
    print (isum blist :: Integer) 

:i HList產生

data HList $a where 
    HNil :: HList ('[] *) 
    (:+:) :: a -> (HList t) -> HList ((':) * a t) 
    -- Defined at /tmp/test.hs:10:6 
instance Show (HList ('[] *)) -- Defined at /tmp/test.hs:17:10 
instance (Show a, Show (HList t)) => Show (HList ((':) * a t)) 
    -- Defined at /tmp/test.hs:19:10 
instance ISum (HList ('[] *)) -- Defined at /tmp/test.hs:25:10 
instance (Integral a, ISum (HList t)) => ISum (HList ((':) * a t)) 
    -- Defined at /tmp/test.hs:29:10 
*Main> :i HList 
data HList $a where 
    HNil :: HList ('[] *) 
    (:+:) :: a -> (HList t) -> HList ((':) * a t) 
    -- Defined at /tmp/test.hs:10:6 
instance Show (HList ('[] *)) -- Defined at /tmp/test.hs:17:10 
instance (Show a, Show (HList t)) => Show (HList ((':) * a t)) 
    -- Defined at /tmp/test.hs:19:10 
instance ISum (HList ('[] *)) -- Defined at /tmp/test.hs:25:10 
instance (Integral a, ISum (HList t)) => ISum (HList ((':) * a t)) 
    -- Defined at /tmp/test.hs:29:10 

從中我收集'[]的糖爲'[] *和x ': y爲(':) * x y。那是什麼*在那裏做？它是那種列表元素？此外，無論如何，這個名單到底是什麼？它是否構建在語言中？

Answer 1

那*是......不幸的。這是GHC用於多色化數據類型的漂亮打印機的結果。它會導致語法上無效的事情，但確實傳遞了一些有用的信息。

當GHC漂亮地打印具有多態類型的類型時，它在類型構造函數之後打印每個多態類型變量的類型。爲了。所以，如果你有一個像聲明：

data Foo (x :: k) y (z :: k2) = Foo y 

GHC會漂亮地打印的Foo類型（數據構造）爲y -> Foo k k1 x y z。如果你有一些使用該牽制的那種類型變量有點像之一..

foo :: a -> Int -> Foo a Int 5 -- Data Kind promoted Nat 

類型的foo "hello" 0將被打印成Foo * Nat String Int 5。是的，這太可怕了。但是如果你知道發生了什麼，至少你可以閱讀它。

'[]東西是DataKinds擴展的一部分。它允許將類型提升爲種類，並且該類型的構造函數變爲類型構造函數。這些升級類型沒有有效值，甚至不是undefined，因爲它們的類型與*不兼容，這是所有可以與它們一起使用值的類型。所以他們只能出現在沒有這種價值類型的地方。欲瞭解更多信息，請參閱http://www.haskell.org/ghc/docs/7.4.1/html/users_guide/kind-polymorphism-and-promotion.html

編輯：

您的評論引發了一些關於點的方式ghci的作品。

-- foo.hs 
{-# LANGUAGE DataKinds, PolyKinds #-} 

data Foo (x :: k) y (z :: k1) = Foo y 

當加載在ghci中一個文件，它不激活交互在文件中使用的擴展。

GHCi, version 7.6.3: http://www.haskell.org/ghc/ :? for help 
Loading package ghc-prim ... linking ... done. 
Loading package integer-gmp ... linking ... done. 
Loading package base ... linking ... done. 
Prelude> :l foo 
[1 of 1] Compiling Main    (foo.hs, interpreted) 
Ok, modules loaded: Main. 
*Main> :t Foo 
Foo :: y -> Foo * * x y z 
*Main> :set -XPolyKinds 
*Main> :t Foo 
Foo :: y -> Foo k k1 x y z 

所以，是的。必須在ghci中啓用PolyKinds擴展名，因爲它缺省爲類型中的多態類型。我試着在文件中定義我的foo函數，但它確實使這個版本的ghc崩潰。哎呦。我認爲現在已經解決了，但我想檢查ghc trac會很好。無論如何，我可以交互地定義它，它工作正常。

*Main> :set -XDataKinds 
*Main> let foo :: a -> Int -> Foo a Int 5 ; foo = undefined 
*Main> :t foo "hello" 0 
foo "hello" 0 :: Foo * GHC.TypeLits.Nat [Char] Int 5 
*Main> :m + GHC.TypeLits 
*Main GHC.TypeLits> :t foo "hello" 0 
foo "hello" 0 :: Foo * Nat [Char] Int 5 

好了，好了，我忘了把它顯示Nat不合格需要進口。而且由於我只是在演示打印，所以我並不關心實現，所以undefined已經足夠好了。

但是一切確實工作我怎麼說，我保證。我只是略去了一些關於需要什麼擴展的細節，特別是PolyKinds和DataKinds。我認爲，既然你在代碼中使用這些代碼，你就會明白它們。以下是關於PolyKinds擴展的文檔：http://www.haskell.org/ghc/docs/7.6.3/html/users_guide/kind-polymorphism.html

Answer 2

這是由於某些關於打印的不幸實現。種類可以被認爲是'種類的類型'。請注意以下幾點：

>:t [] 
[] :: [a] 
>:k '[] 
'[] :: [*] 

就像[a]手段 「爲各類一，[a]」，[*]手段 「爲所有種*，[*]」。然而，你可以用類型做的推理量要比類型小得多。例如，a -> a表示兩個a s都是相同的類型，但是* -> *表示兩個*都可以是任何類型（可以認爲* -> *是類型a -> b「提升」到種類級別）。但是沒有辦法將類型a -> a提升到種類水平。這意味着[a]和[*]不是很相似。 [*]更接近[forall a . a]。更簡潔但更不準確的是，你可以說沒有辦法區分'多態'種類，因爲沒有'種類變量'之類的東西。 （邊注：​​使文件所稱的「多態種」的東西，但它仍然不會給你真正的多態性）

所以，當你寫HList :: [*] -> *（這實際上意味着HList (k :: [*]) :: *）要表示的那種第一類型參數應該是[*]，和「價值」這類型的一種[*]可以是'[]，* ': '[]，* ': * ': '[]等

現在的問題。當打印類型受限的東西時，如第一個類型參數HNil，它將嘗試包含所有類型的信息。無論出於何種原因，而不是寫

HNil :: HList ('[] :: '[*]) 
^ data  ^type ^kind 

這實際上表明*指的是那種'[]，它打印在您親眼目睹了非常困惑格式的東西。有必要獲得這些信息，因爲列表中存儲的東西不一定是開放式的（這是*的名稱）。你可能有這樣的：

data Letter = A | B -- | C .. etc 
data LetterProxy p 

data HList (k :: [Letter]) where 
    HNil :: HList '[] 
    (:+:) :: LetterProxy (a :: Letter) -> HList t -> HList (a ': t) 

這是非常愚蠢的，但仍然有效！

我認爲這個錯誤是由於兩個原因造成的。首先，如果事情是按照我所述的格式打印的，則某些數據類型或類的:i的結果將非常長且非常難以理解。其次，種類是非常新的（僅在7.4之後？），所以沒有花費大量的時間來決定如何打印附帶的東西，因爲沒有人確定應該/將如何工作。