代码之家  ›  专栏  ›  技术社区  ›  snak

一个善良的签名

  •  1
  • snak  · 技术社区  · 4 年前

    在里面 singletons-2.6 , Sigma 定义为

    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 ,但会发生什么呢?我有一种感觉,我错过了一些非常基本的东西。

    我试图找到任何描述这一点的文件,但我没有运气。

    0 回复  |  直到 4 年前
        1
  •  0
  •   snak    3 年前

    现在,我从你那里得到了一些想法 dependent haskell 在GHC维基上。

    我们现在可以将一种类型传递给类型构造函数,就像我们可以将一种类型传递给数据构造函数一样(我们仍然需要传递一个单例,而不是类型本身)。

    在这份声明中 Sigma ,

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

    s 在里面 s :: Type 是一种变量 Type 当您使用 西格玛 .以同样的签名,

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

    forall s 方法 s 是一种看得见的东西。这意味着当你说它是可见的时,你需要显式地传递它。你可以把它读作 西格玛 类型构造函数是否采用 s 还有一种 s ~> Type ,并返回一种 类型 .

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

    更新(2021/9/30) :

    这被称为可视依赖量化。你可以在网站上找到一个很好的解释 Visible dependent quantification in Haskell .

    推荐文章