究竟是什么样的“*”在Haskell中？ [英] What exactly is the kind "*" in Haskell?

问题描述

在Haskell中，（值级）表达式被分类为类型，可以用 :: 来表示： 3 :: Int ，Hello:: String ，（+ 1）:: Num a = > a - >一个。类似地，类型被分类为 。在GHCi中，您可以使用命令：kind 或：k 来检查类型表达式的类型：

 > ：k Int 
 Int :: * 
> ：k也许
也许:: *  - > * 
> ：k要么
要么:: *  - > *  - > * 
> ：k Num 
 Num :: *  - >约束
> ：k Monad 
 Monad ::（*  - > *） - >约束
  

* 是具体类型或数值或运行时间值的一种。例如，请参阅了解你A哈斯克尔。那是多么真实？我们有一些 问题 关于类型的说明，但是如果有一个标准的和精确的 * 。

* 是什么意思？它与其他更复杂的类型有什么关系？

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

解决方案

首先， * 不是通配符！它也通常发音为星级。

出血边缘音符：截至2015年2月一个简化GHC子系统（7.12或更高版本）的建议。该页面包含关于GHC 7.8 / 7.10故事的良好讨论。展望未来，GHC可以通过 * :: * 降低类型和种类之间的差异。请参阅 Weirich，Hsu和Eisenberg，显式类平等系统FC标准：对表达式的描述。

Haskell 98报告在此上下文中定义 * a>：
$ b

符号 * 表示所有无类型构造函数的类型。

在这种情况下，空意味着构造函数不带任何参数。 是二进制的;它可以应用于两个参数：或者b 。 也许是一元的;它可以应用于一个参数：也许一个。 Int 是空的;它可以应用于 no 参数。

这个定义本身有点不完整。包含完全应用的一元，二元等类型构造函数的表达式也具有类型 * ，例如， 可能是Int :: * 。

GHC：包含值的东西吗？

如果我们讨论GHC文档，可以更接近可以包含运行时值的定义。 GHC评论页面种类指出< * '是盒装值的类型，比如 Int 和 Maybe Float 有种 * 。 GHC版本用户指南另一方面，7.4.1 指出 * 是提升类型的种类。 （当该部分修改为
PolyKinds 时，该段落未被​​保留。）

装箱值和提升类型有点不同。根据 GHC评论页面TypeType，

如果某个类型的表示不是指针，则该类型将被解除装箱。 Unboxed类型也是unlifted。

如果一个类型的底部是一个元素，则类型会被解除。闭包始终具有提升类型：即，Core中的任何允许绑定标识符必须具有提升类型。在操作上，抬起的物体是可以输入的物体。

所以 ByteArray＃ ，内存原始块的类型是 boxed ，因为它被表示为一个指针，但是 unlifted 因为bottom不是一个元素。

 > undefined :: ByteArray＃
错误：匹配类型时的种类不兼容：
 a0 :: * 
 ByteArray＃::＃
  

因此，旧的用户指南定义比GHC评论更准确： * 是 类型。（相反，＃是 unlifted 类型的类型。）注意如果类型 * 总是被取消，对于任何类型 t： ：* 你可以使用 undefined :: t 或其他一些机制来创建一个值。因此，即使是逻辑无人居住的类型，如 Void 也可以有一个值，即bottom。

所以看起来，如果 undefined 是您对运行时值的概念，那么 * 表示可以包含运行时值的类型。 （这不是一个完全疯狂的想法，我不认为。）

GHC扩展？

有几个扩展让这个系统有点活跃。其中一些是世俗的：> KindSignatures 可让我们编写类注释，就像类型注释一样。

ConstraintKinds 增加了类型约束，这大致是<$的左边的类型c $ c> => 。

DataKinds * 和＃，就像我们可以用 data ， newtype 和类型。





DataKinds 每个 data 声明（可能适用的条款和条件）会生成促销类声明。所以

  data Bool = True |假
  

介绍了常用的值构造函数和类型名称;此外，它会生成一个新的类， Bool 和两个类型： True :: Bool 和 False :: Bool 。

PolyKinds 介绍类型变量。这只是对任何类型 k 的说法，就像我们所说的任何类型 t 类型级别。至于我们的朋友 * 以及它是否仍然意味着带值的类型，我想你可以说类型 t :: k 其中 k 是一种变量可以包含值，如果 k〜* 或 k〜＃。

In Haskell, (value-level) expressions are classified into types, which can be notated with :: like so: 3 :: Int, "Hello" :: String, (+ 1) :: Num a => a -> a. Similarly, types are classified into kinds. In GHCi, you can inspect the kind of a type expression using the command :kind or :k:

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

There are definitions floating around that * is the kind of "concrete types" or "values" or "runtime values." See, for example, Learn You A Haskell. How true is that? We've had a few questions about kinds that address the topic in passing, but it'd be nice to have a canonical and precise explanation of *.

What exactly does * mean? And how does it relate to other more complex kinds?

Also, do the DataKinds or PolyKinds extensions change the answer?

解决方案

First off, * is not a wildcard! It's also typically pronounced "star."

Bleeding edge note: There is as of Feb. 2015 a proposal to simplify GHC's subkind system (in 7.12 or later). That page contains a good discussion of the GHC 7.8/7.10 story. Looking forward, GHC may drop the distinction between types and kinds, with * :: *. See Weirich, Hsu, and Eisenberg, System FC with Explicit Kind Equality.

The Standard: A description of type expressions.

The Haskell 98 report defines * in this context as:

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

In this context, "nullary" simply means that the constructor takes no parameters. Either is binary; it can be applied to two parameters: Either a b. Maybe is unary; it can be applied to one parameter: Maybe a. Int is nullary; it can be applied to no parameters.

This definition is a little bit incomplete on its own. An expression containing a fully-applied unary, binary, etc. type constructor also has kind *, e.g. Maybe Int :: *.

In GHC: Something that contains values?

If we poke around the GHC documentation, we get something closer to the "can contain a runtime value" definition. The GHC Commentary page "Kinds" states that "'*' is the kind of boxed values. Things like Int and Maybe Float have kind *." The GHC user's guide for version 7.4.1, on the other hand, stated that * is the kind of "lifted types". (That passage wasn't retained when the section was revised for PolyKinds.)

Boxed values and lifted types are a bit different. According to the 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.

So ByteArray#, the type of raw blocks of memory, is boxed because it is represented as a pointer, but unlifted because bottom is not an element.

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

Therefore it appears that the old User's Guide definition is more accurate than the GHC Commentary one: * is the kind of lifted types. (And, conversely, # is the kind of unlifted types.)

Note that if types of kind * are always lifted, for any type t :: * you can construct a "value" of sorts with undefined :: t or some other mechanism to create bottom. Therefore even "logically uninhabited" types like Void can have a value, i.e. bottom.

So it seems that, yes, * represents the kind of types that can contain runtime values, if undefined is your idea of a runtime value. (Which isn't a totally crazy idea, I don't think.)

GHC Extensions?

There are several extensions which liven up the kind system a bit. Some of these are mundane: KindSignatures lets us write kind annotations, like type annotations.

ConstraintKinds adds the kind Constraint, which is, roughly, the kind of the left-hand side of =>.

DataKinds lets us introduce new kinds besides * and #, just as we can introduce new types with data, newtype, and type.

With DataKinds every data declaration (terms and conditions may apply) generates a promoted kind declaration. So

 data Bool = True | False

introduces the usual value constructor and type name; additionally, it produces a new kind, Bool, and two types: True :: Bool and False :: Bool.

PolyKinds introduces kind variables. This just a way to say "for any kind k" just like we say "for any type t" at the type level. As regards our friend * and whether it still means "types with values", I suppose you could say a type t :: k where k is a kind variable could contain values, if k ~ * or k ~ #.

这篇关于究竟是什么样的“*”在Haskell中？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！