为什么 :k [False] 会导致 GHCI 出错？

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] :: *

Answer 1

如果您的类型级别列表只有一个元素，GHC 认为它不是提升列表，而是应用于某种类型的常规列表类型构造函数 *。

对于提升列表，您应该在列表前加上撇号以显式 select：

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

与空列表类似：

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

Answer 2

如您所见：

[Int] can have inhabited values so it is of kind *, but it also makes sense that it is of kind [*]

您发现的是，如果您只是允许将值表达式提升到类型级别，则 DataKinds 在某些类型表达式中存在歧义。由于对列表文字和列表类型都使用了方括号，因此它经常出现列表，但它并不完全特定于列表。

基本上，源代码文本 [False] 可以引用三个不同的东西：

值级别列表的列表文字语法，包含一个值为 False
列表类型构造函数应用于类型 False
类型级别列表的列表文字语法，包含一个元素，即 type False

没有 DataKinds，第三个含义不存在，因此编译器始终可以使用其上下文知识来判断源代码文本 [False] 是出现在类型表达式还是值表达式中。但是情况 2 和 3 都出现在类型表达式中，所以这无济于事。

在这种情况下我们可以看到 [False] 作为类型 "list of things of type False" 没有任何意义，因为 [] 类型构造函数只能应用于种类 *。但是编译器必须先知道你想说什么，然后才能type/kind检查内容是否一致；我们真的不希望它尝试几种可能的解释并 type/kind 检查所有解释，如果其中一个有效则默默接受。无论如何，只要付出一点努力（按照使用 PolyKinds 定义合适的类型名称 and/or 来制作接受多种事物的类型构造函数的思路），您可以想出这样一种情况，即一段源文本具有所有 3 个我上面概述的各种含义，所有 3 个都可以无错误地编译。

因此，为了解决歧义（不破坏现有语法，如 [Int] for "list of things of type Int"）GHC 采用普通非提升类型构造函数优先的规则。所以 [False] 实际上并不表示类型级别的单例列表；它仅表示（废话）"list of things of type False" 类型，这会导致您看到的那种错误。

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

Prelude> :k 'False
'False :: Bool

并且类似地，在列表文字语法的前面添加一个撇号明确表示您正在编写类型级别的列表文字，而不是编写列表类型，即使列表只有一项。所以：

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

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

您可以类似地使用它来区分类型 * -> * 的列表类型构造函数和空类型级列表：

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

为什么 :k [False] 会导致 GHCI 出错？

Why does :k [False] result in an error in GHCI?

haskell

data-kinds