12

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

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

2 回答 2

11

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

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

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

与空列表类似：

> :k '[]
'[] :: [k]
于 2015-11-05T21:32:14.583 回答
3

如您所述：

[Int]可以有可居住的价值观，所以它是善良的*，但它是善良的也是有道理的[*]

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

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

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

如果没有 DataKinds，则不存在第三种含义，因此编译器始终可以使用其上下文知识来判断源代码文本[False]是出现在类型表达式还是值表达式中。但是 case 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]
于 2015-11-06T00:07:38.877 回答