haskell - 为什么存在量化和数据类型不能一起工作？

Question

{-# LANGUAGE DataKinds, ExistentialQuantification, KindSignatures #-}
import Data.Proxy

data Type t= forall (a :: t). Type (Proxy a)

给出错误

Type variable ‘t’ used in a kind
In the kind ‘t’
In the definition of data constructor ‘Type’
In the data declaration for ‘Type’

Butt是 Kind 变量，而不是类型变量。这是怎么回事？

score 9 · Accepted Answer

在 GHC 8 之前，任何地方都不允许使用种类绑定。在这里，我们必须使用善良的代理。在这种情况下，我们可以这样做：

import Data.Proxy

data Type (kp :: KProxy k) = forall (a :: k). Type (Proxy a)

使用 GHC 8，您确实可以编写原始版本：

{-# language TypeInType #-}

data Type t = forall (a :: t). Type (Proxy a)

score 2 · Accepted Answer

类型构造函数的参数是类型，而不是种类。所以data Type t = ...手段t是一个类型变量。

在 GHC 8.0 中，TypeInType 扩展消除了类型和种类之间的区别，如果您启用它，则允许您的程序被接受（如果您不启用，GHC 会建议启用该扩展）。

2 回答 2