haskell - 关于基类中类型级别 bool 值的混淆

Question

Base 包含许多用于类型级别 bool 运算的类型系列，如下所示:

https://hackage.haskell.org/package/base-4.8.2.0/docs/Data-Type-Bool.html

但是，指向 True 和 False 的链接仅引用 Bool 的数据构造函数，而不是类型本身，因此推测它们不能用于类型级别操作，因为它们是值，而不是类型。

有人可以解释一下这里发生了什么以及我在哪里可以找到类型级别定义吗？

Answer 1

the links to True and False just refer to data constructors of Bool, not types themselves

没错。事实上它们不是类型(例如True有什么值^*)？它们本身仍然只是 Bool 类型的值。 。只是，整个类型已通过 -XDataKinds extension“提升”了一级。 ，所以Bool现在也是一个类型级别的类型:又名种类。

传统上，在 Haskell 中，我们主要使用该死的单一类型:* ，普通类型的那种^†。该类包含Bool和String和IO ()和(Int -> Double) -> Char ...实际上具有值(value)的一切^‡。加上构造函数类型，它们都是某种形式的 * -> *并包含类似 Maybe 的内容或[] (当未应用于包含类型参数时)。

与 DataKinds现在，我们已经添加了一整套类型:您可以在运行时使用的任何类型^§ - Haskell 代码现在也可以在编译时用作类型!所有这些类型都包含它们在运行时级别上也具有的值。但那些类型级别的值，例如 False和True您问的问题实际上不是类型，它们只是存在于类型级别中。但您可以构建实际的*他们的类型，例如类似的东西

data CanContain :: Bool -> * -> * where
  Interesting :: a -> CanContain True a
  Boring :: CanContain False a

然后是一个类型为 X -> CanContain True Y 的函数实际上必须生成 Y值，而是类型为 X -> CanContain False Y 的函数不需要。

<小时/>

^*_{不，答案不是 True 。不过，我们可以实现 type Bool = Either False True ，这有点道理。}

^†_{可以说，对于解析*的语言来说，这不是一个很好的名字。作为中缀符号。将来实际上会改变。}

^‡_{事情没那么简单:也有未装箱的类型，但这些都是技术细节。}

^§_{正如 dfeuer 所说，现在并非所有类型都可以被提升 (GHC-7.10)，但简单的类型如 Bool当然可以。}