Haskell Weird Kinds: Kind of (->) is ?? ->？ -> *

Question

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

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

而不是预期的* -> * -> *。 ?? 和 ? 是什么？它们是指具体类型还是“种类变量”？还是别的什么？

Answer 1

这些是 Haskell 类系统的特定于 GHC 的扩展。 Haskell 98 报告specifies only a simple kind system：

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

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

GHC extends this system 带有一种类型的子类型，允许unboxed types，并允许函数构造器在类型上是多态的。格GHC支持的种类有：

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

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 的话，“在种类层面有一点子类型化”。

对于感兴趣的灵魂，GHC 还支持在 GADT、新类型和类型族中使用的强制类型和种类（“作为类型相等性证据的类型级术语”，System Fc 需要）。