什么是'[]和':在Haskell中？

Question

我在一些地方看过这个'[]和':语法,最着名的是在HList或HVect等异构列表包中.

例如,异构向量HVect定义为

data HVect (ts :: [*]) where
    HNil :: HVect '[]
    (:&:) :: !t -> !(HVect ts) -> HVect (t ': ts)

在GHCi中,通过扩展TemplateHaskell或者DataKinds,我得到了这个

> :t '[]
'[] :: template-haskell-2.13.0.0:Language.Haskell.TH.Syntax.Name
> :t '(:)
'(:) :: template-haskell-2.13.0.0:Language.Haskell.TH.Syntax.Name

我的印象是这与依赖类型和种类等有关,而不是模板haskell.

搜索引擎,以及hoogle和hayoo用'[]或者':相当糟糕地处理查询,因此问题是:这些'[]和':事物的名称是什么？非常欢迎指向文档或教程的指针.

Answer 1

DataKinds 允许在类型级别使用术语级构造函数.

后

data T = A | B | C

一个人可以编写索引值的类型 T

data U (t :: T) = ...
foo :: U A -> U B -> ...

但在这里,A并且B被用作类型,而不是价值.因此,他们必须使用引用"提升":

data U (t :: T) = ...
foo :: U 'A -> U 'B -> ...

熟悉的列表语法也是如此.'[]是一个空列表,在类型级别提升.与类型级别提升的列表'[a,b,c]相同a ': b ': c ': '[].

type           :: kind
'[]            :: [k]   -- polykinded! works for any kind k
'[ 'A, 'B, 'C] :: [T]   -- mind the spaces, we do not want the char '['
'A ': '[]      :: [T]
'[ Int, Bool ] :: [*]   -- a list of types
'[ Int ]       :: [*]   -- a list of types with only one element
[Int]          :: *     -- a type "list of Int"

请注意最后两种情况,其中引用消除了语法歧义.