种类列表究竟如何工作？

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之后？），所以没有花费大量的时间来决定如何打印附带的东西，因为没有人确定应该/将如何工作。