8

我已经在几个地方看到过这个'[]和':语法，尤其是在HList或HVect等异构列表包中。

例如，异质向量HVect定义为

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

在 GHCi 中，带有扩展名TemplateHaskellor 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处理查询的方式'[]或':相当糟糕，因此问题是：这些'[]和':事物的名称是什么？指向文档或教程的指针将是最受欢迎的。

4

2 回答 2

9

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"

请注意最后两种情况，其中引号消除了语法的歧义。

于 2019-01-03T10:46:31.693 回答
1

这本书

桑迪·马奎尔 (Sandy Maguire)的类型思考( http://thinkingwithtypes.com )

一般来说，它可能是关于 Haskell 中类型级编程主题的一个很好的资源。“解除限制”一章处理DataKinds并提升了构造函数。

（免责声明：无从属关系。）

于 2019-01-04T06:45:20.480 回答