为什么在GHCI中:k [False]会导致错误？

Question

我对下面会话结束时收到的错误感到困惑：

$ ghci
GHCi, version 7.10.2: http://www.haskell.org/ghc/  :? for help
Ok, modules loaded: Main.
*Main> :set -XDataKinds

*Main> :t [False, True]
[False, True] :: [Bool]

*Main> :t [False]
[False] :: [Bool]

*Main> :k [False, True]
[False, True] :: [Bool]

*Main> :k [False]

<interactive>:1:2:
    Expected kind ‘*’, but ‘False’ has kind ‘Bool’
    In a type in a GHCi command: [False]

为什么会出现错误？

---

进一步的实验表明：

*Main> :k [Int]
[Int] :: *

*Main> :k [Int, Int]
[Int, Int] :: [*]

[Int] 可以有实际值，因此其类型为 *，但也可以看作是 [*] 类型。

---

更多数据点：

*Main> :k []
[] :: * -> *

*Main> :k [Bool]
[Bool] :: *

- user1002430

---

我刚开始学习这个，所以我对我的答案没有信心，但是使用-XDataKinds，类型[False, True]不会是种类为[Bool]吗？ - user1002430

Answer 1

如果您有仅包含单个元素的类型级列表，GHC会认为这不是提升的列表，而是应用于某种*类型的常规列表类型构造函数。

您应该在列表前面加上一个撇号，以明确选择提升的列表：

> :k '[False]
'[False] :: [Bool]

同样适用于空列表：

> :k '[]
'[] :: [k]

- András Kovács

---

具体来说，[False] 被解析为 [] :: * -> * 应用于 False :: Bool 的类型，这里存在一种不匹配的情况 - [] 期望一个 *，这导致了观察到的 "kind error"。 - user2407038

Answer 2

正如您所指出的：

[Int] 可以具有实际值，因此其种类为 *，但它也有意义是种类为 [*]

您发现的是，在某些类型表达式中，如果您允许将值表达式提升到类型级别，那么 DataKinds 中存在歧义。这往往在列表中经常出现，因为方括号用于列表字面量和列表类型，但它并不完全特定于列表。

基本上，源代码文本 [False] 可能指代 三个 不同的事情：

1. 值级别列表的列表字面量语法，包含一个元素，该元素是值 False
2. 应用于 类型 False 的列表类型构造函数
3. 类型级别列表的列表字面量语法，包含一个元素，该元素是 类型 False

没有 DataKinds，第三个含义就不存在了，因此编译器始终可以使用其上下文知识，以确定源代码文本 [False] 是否出现在类型表达式或值表达式中。但是，情况 2 和 3 都出现在类型表达式中，因此这并没有帮助。

在这种情况下，我们可以看到 [False] 作为类型 "类型为 False 的事物的列表" 没有任何意义，因为 [] 类型构造函数只能应用于种类为 * 的事物。但是编译器必须知道您要表达什么，然后才能对其进行类型/种类检查以查看是否一致；我们真的不希望它尝试几种可能的解释并对它们全部进行类型/种类检查，如果其中一种起作用，则默默接受。而且无论如何，通过一些努力（沿着定义适当的类型名称和/或使用 PolyKinds 来使类型构造函数接受多种种类的事物的线路），您可以想出一种情况，在该情况下，源文本具有我上面概述的所有 3 种含义，所有这 3 种都可以编译而不出错。

因此，为了消除歧义（而不破坏现有语法，例如用于 "类型为 Int 的事物的列表" 的 [Int]），GHC采用普通的非提升类型构造函数具有优先权的规则。因此，[False] 实际上并不意味着类型级别的单例列表；它只意味着（无意义的）"类型为 False 的事物的列表" 类型，这会导致您看到的种类错误。

但是 DataKinds 还引入了语法，以明确请求其他含义；如果在任何类型构造函数之前加上撇号，则 GHC 知道您正在引用值构造函数的提升版本，而不是同名的任何非提升类型构造函数。例如：

Prelude> :k 'False
'False :: Bool

类似地，对于列表字面量语法，在开头添加一个撇号明确表示您正在编写类型级别的列表字面量，即使列表只有一个项目，也不是编写列表类型。 所以：

Prelude> :k '[False]
'[False] :: [Bool]

Prelude> :k '[Int]
'[Int] :: [*]

你可以同样使用它来区分类型构造器 kind 为 * -> * 的列表类型和空的类型级别列表：

Prelude> :k []
[] :: * -> *
Prelude> :k '[]
'[] :: [k]

- Ben