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

问题描述

当我尝试使用 Haskell 类型并尝试获得 -> 类型时，结果出现了:

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?

推荐答案

这些是 Haskell 类系统的 GHC 特定扩展.Haskell 98 报告仅指定一个简单的种类系统:

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:

符号*代表的种类所有空类型构造函数.如果 k1和 k2 是种类，那么 k1->k2 是kind of types 采取一种类型的类型k1 并返回 k2 类型.

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 扩展这个系统种类子类型，允许未装箱的类型，并允许函数构造器在种类上是多态的.GHC支持的类格为:

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

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

特别是:

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

在最后一个示例中的位置 t :: ??(即不是未装箱的元组).所以，引用 GHC 的话，在种类层面上有一些子类型".

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".

对于感兴趣的灵魂，GHC 还支持强制类型和种类(作为类型相等性证据的类型级术语"，根据 System Fc) 用于 GADT、新类型和类型系列.

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 奇怪的种类:种类 (->) 是 ??->?->*的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！