种类清单究竟如何运作？

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 ': yfor for (':) * 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

是的.该PolyKinds扩展必须在ghci中启用它默认为多态种类型.我也尝试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