Haskell 奇怪的种类 : Kind of (->) is ? ？ ->？ -> *

Question

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

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

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

Answer 1

这些是 Haskell 类系统的 GHC 特定扩展。 Haskell 98 报告 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使用某种形式的子类型，允许 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 所需要)。