所有人的亲切签名

data Sigma (s :: Type) :: (s ~> Type) -> Type

GHC 8.8.4告诉我们它的种类是

> :k Sigma
Sigma :: forall s -> (s ~> *) -> *

这种forall这种签名是什么？

显然，它不同于

data Sigma :: forall s. Type -> (s ~> Type) -> Type

在这种情况下，当然是

Sigma :: * -> (s ~> *) -> *

而且，这似乎与

不同

data Sigma :: f s -> (s ~> *) -> *

在我看来，s中类型变量s :: Type的提升类型与s中类型变量(s ~> Type) -> Type统一，但是会发生什么吗？我觉得我缺少一些非常基本的东西。

我试图找到任何描述此事的文件，但我没有运气。

现在，我从GHC Wiki的dependent haskell中得到了一些想法。

我们现在可以将类型传递给类型构造函数，就像我们可以将类型传递给数据构造函数一样（尽管我们仍然需要传递单例而不是类型本身）。

在Sigma的声明中，

data Sigma (s :: Type) :: (s ~> Type) -> Type

s中的

s :: Type是Type种类的种类变量，当您使用Sigma时必须显式传递该种类。并以亲切的签名

Sigma :: forall s -> (s ~> *) -> *

forall s表示s是可见的种类。这意味着您需要在其可见时明确传递它。您可以将其读为Sigma是一个类型构造器，它接受类型s和类型s ~> Type，并返回类型Type。

您不能直接在GHC 8.8.4中编写此类型签名，但可以在GHC 8.10.1中使用StandaloneKindSignatures来编写。