6

我最近一直在阅读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

我从中收集到'[]的是糖 for'[] *和x ': yfor (':) * x y。那个*在那里做什么？它是列表元素的那种吗？另外，这样的列表到底是什么？它是语言内置的吗？

4

2 回答 2

7

那*是……不幸。这是 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

于 2013-11-26T22:08:49.847 回答
0

这是由于一些关于打印的不幸实现。种类可以被认为是“类型的类型”。请注意以下事项：

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

就像[a]意思是“对于所有类型 a, [a]”，[*]意思是“对于所有种类 *，[*]”。然而，你可以用种类做的推理量比用类型要少得多。例如，a -> a表示两个as 是相同的类型，但* -> *表示两者都*可以是任何类型（可以认为* -> *是将类型a -> b“提升”到 kind 级别）。但是没有办法将类型提升a -> a到善良的水平。这意味着[a]和[*]并不十分相似。[*]更接近于[forall a . a]. 更简洁但不太准确，您可以说没有办法区分“多态”种类，因为没有“种类变量”之类的东西。（边注：-XPolyKinds启用文档所谓的“多态类型”，但它仍然没有给你真正的多态性）

因此，当您编写时HList :: [*] -> *（这实际上意味着HList (k :: [*]) :: *），您表明第一个类型参数的种类应该是[*]，种类类型[*]可以采用的“值”是'[]、、、* ': '[]等* ': * ': '[]。

现在的问题。当打印种类受到约束的东西时，比如 的第一个类型参数HNil，它会尝试包含所有种类信息。无论出于何种原因，而不是写作

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

这实际上表明 the*指的是那种'[]，它以您目睹的非常混乱的格式打印事物。有这个信息是必要的，因为列表中“存储”的东西不一定是开放式的（这是 的名称*）。你可以有类似的东西：

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 之后才出现？）所以没有花费太多时间来决定如何打印种类的东西，因为还没有人确定种类应该/将如何工作。

于 2013-11-27T00:26:12.437 回答