haskell - Haskell 中的 "*"到底是什么？

Question

在 Haskell 中，(值级)表达式分为类型，可以用 :: 表示。像这样:3 :: Int , "Hello" :: String , (+ 1) :: Num a => a -> a .类似地，类型被分类为种类。在 GHCi 中，您可以使用命令 :kind 检查类型表达式的种类。或 :k :

> :k Int
Int :: *
> :k Maybe
Maybe :: * -> *
> :k Either
Either :: * -> * -> *
> :k Num
Num :: * -> Constraint
> :k Monad
Monad :: (* -> *) -> Constraint

周围有一些定义 *是一种“具体类型”或“值”或“运行时值”。例如，参见 Learn You A Haskell .这有多真实？我们有 a few questions about kinds顺便解决了这个话题，但最好能对 * 有一个规范和准确的解释。 .
* 到底是什么意思？意思是？它与其他更复杂的类型有什么关系？

另外，请执行 DataKinds或 PolyKinds扩展改变答案？

Answer 1

首先，*不是通配符!它通常也发音为“明星”。
出血边缘注释:截至 2015 年 2 月 a proposal to simplify GHC's subkind system (in 7.12 or later) .该页面包含对 GHC 7.8/7.10 故事的精彩讨论。展望 future ，GHC 可能会放弃类型和种类之间的区别，* :: * .见 Weirich, Hsu, and Eisenberg, System FC with Explicit Kind Equality .
标准:类型表达式的描述。
Haskell 98 报告 defines * in this context as :

The symbol * represents the kind of all nullary type constructors.

在这种情况下，“nullary”只是意味着构造函数不带参数。 Either是二进制的；它可以应用于两个参数: Either a b . Maybe是一元的；它可以应用于一个参数: Maybe a . Int是无效的；它可以应用于无参数。
这个定义本身有点不完整。包含完全应用的一元、二元等类型构造函数的表达式也有种类 * ，例如 Maybe Int :: * .
在 GHC 中:包含值的东西？
如果我们浏览 GHC 文档，我们会得到更接近“可以包含运行时值”定义的东西。 GHC Commentary page "Kinds"声明“' * '是一种装箱值。像 Int 和 Maybe Float 这样的东西有 * 。” GHC user's guide for version 7.4.1 ，另一方面，表示 *是那种“举起的类型”。 (当该部分被修改时，该段落没有保留 PolyKinds .)
装箱值和提升类型有点不同。根据 GHC Commentary page "TypeType" ,

A type is unboxed iff its representation is other than a pointer. Unboxed types are also unlifted.

A type is lifted iff it has bottom as an element. Closures always have lifted types: i.e. any let-bound identifier in Core must have a lifted type. Operationally, a lifted object is one that can be entered. Only lifted types may be unified with a type variable.

所以 ByteArray# ，原始内存块的类型，因为它被表示为指针而被装箱，但因为底部不是元素而未被提升。

> undefined :: ByteArray#
Error: Kind incompatibility when matching types:
   a0 :: *
   ByteArray# :: #

因此，旧的用户指南定义似乎比 GHC 评论更准确: *是那种提升的类型。 (相反， # 是未提升的类型。)
请注意，如果种类 *总是被提升，对于任何类型 t :: *你可以用 undefined :: t 构造一个“值”或其他一些创建底部的机制。因此，即使是“逻辑上无人居住”的类型，如 Void可以有一个值，即底部。
所以看起来，是的， *表示可以包含运行时值的类型，如果 undefined是您对运行时值(value)的看法。 (这不是一个完全疯狂的想法，我不认为。)
GHC 扩展？
有几个扩展使善良系统活跃了一点。其中一些是平凡的: KindSignatures让我们编写类型注释，如类型注释。 ConstraintKinds加样 Constraint ，大致就是 => 左侧的那种. DataKinds让我们介绍 *以外的新品种和 # ，就像我们可以用 data 引入新类型一样, newtype , 和 type .
与 DataKinds每 data声明(可能适用条款和条件)生成提升的种类声明。所以

 data Bool = True | False

介绍了常用的值构造函数和类型名称；此外，它还产生了一种新类型， Bool , 和两种类型: True :: Bool和 False :: Bool . PolyKinds引入种类变量。这只是一种说“对于任何类型 k”的方式，就像我们在类型级别说“对于任何类型 t”一样。至于我们的 friend *以及它是否仍然意味着“具有值的类型”，我想你可以说一个类型 t :: k在哪里 k是一种可以包含值的变量，如果 k ~ *或 k ~ # .