Haskell奇怪的种类：（ - >）的种类是？ - > ？ - > * [英] Haskell Weird Kinds: Kind of (->) is ?? -> ? -> *

问题描述

当我尝试使用Haskell类型时，试图获得 - > 类型，并且这个结果显示出来了：

  $ ghci 
 ... 
前奏> ：k（ - >）
（ - >）:: ?? - > ？ - > * 
前奏> 
  

而不是预期的 * - > * - > * 。
什么是 ?? 和？东西？它们是指具体类型还是类变量？还是其他的东西？

解决方案

这些是Haskell类系统的GHC特定扩展。 Haskell 98报告仅指定一个简单类型的系统：

...类型表达式被分类为不同的
类型，其中
有两种可能的形式：

符号*表示
所有空类型构造函数的类型。如果k1
和k2是种类，那么k1-> k2是
类型的类型，它们采用类型
k1并返回一种类型k2。

GHC 用这种类型的子类型来扩展这个系统，以允许 unboxed types ，并允许函数构造器在多种类型上是多态的。 GHC支持的类格是：

 ？ 
 / \ 
 / \ 
 ?? （＃）
 / \ 
 *＃
 
其中：* [LiftedTypeKind]表示盒装类型
＃[UnliftedTypeKind]表示取消装箱类型
（＃ ）[UbxTupleKind]表示取消装箱的元组
？ [ArgTypeKind]是{*，＃} 
的润色吗？ [OpenTypeKind]意味着任何类型的所有
  

定义于 ghc / compiler / types / Type.lhs

：

 >错误:: forall a：？。字符串 - > a 
> （ - >）:: ?? - > ？ - > * 
> （\\（x :: t） - > ...）
  

最后一个例子 t :: ?? （即不是未装箱的元组）。所以，引用GHC的话来说，在类别层面上有一些子类型。

对于感兴趣的灵魂，GHC也支持强制类型和种类（类型级别的术语作为类型平等的证据，正如 System Fc < a>）用于GADT，newtypes和类型系列。

When I was experimenting with Haskell kinds, and trying to get the kind of ->, and this showed up:

$ ghci
...
Prelude> :k (->)
(->) :: ?? -> ? -> *
Prelude> 

Instead of the expected * -> * -> *. What are the ?? and ? things? Do they mean concrete types or "kind variables"? Or something else?

解决方案

These are GHC-specific extensions of the Haskell kind system. The Haskell 98 report specifies only a simple kind system:

... type expressions are classified into different kinds, which take one of two possible forms:

The symbol * represents the kind of all nullary type constructors. If k1 and k2 are kinds, then k1->k2 is the kind of types that take a type of kind k1 and return a type of kind k2.

GHC extends this system with a form of kind subtyping, to allow unboxed types, and to allow the function construtor to be polymorphic over kinds. The kind lattice GHC supports is:

             ?
             /\
            /  \
          ??   (#)
          / \     
         *   #     

Where:       *   [LiftedTypeKind]   means boxed type
             #   [UnliftedTypeKind] means unboxed type
            (#)  [UbxTupleKind]     means unboxed tuple
            ??   [ArgTypeKind]      is the lub of {*, #}
            ?    [OpenTypeKind]     means any type at all

Defined in ghc/compiler/types/Type.lhs

In particular:

> error :: forall a:?. String -> a
> (->)  :: ?? -> ? -> *
> (\\(x::t) -> ...)

Where in the last example t :: ?? (i.e. is not an unboxed tuple). So, to quote GHC, "there is a little subtyping at the kind level".

For interested souls, GHC also supports coercion types and kinds ("type-level terms which act as evidence for type equalities", as needed by System Fc) used in GADTs, newtypes and type families.

这篇关于Haskell奇怪的种类：（ - &gt;）的种类是？ - &GT; ？ - &GT; *的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！