如何定义具有显式种类量化的数据类型？

Question

当我定义

data Foo a = Foo [a]

那么类型就是那种

Foo :: * -> *

.

启用PolyKinds和

RankNTypes

我想用更通用的签名明确量化它

Foo :: forall k . k -> k

.

但是我的尝试都没有奏效：

--    Malformed head of type or class declaration: (Foo :: forall k.
--                                                         k -> k) a
32 | data (Foo :: forall k . k -> k) a = Foo [a]

-- error: parse error on input ‘::’
32 | data Foo a = Foo [a] :: forall k . k -> k

-- error:
--     Multiple declarations of ‘Foo’

data Foo :: forall k . k -> k
data Foo a = Foo [a]

Answer 1

您可以使用独立的签名：

type Foo :: forall k. k -> k
data Foo a = Foo [a]

但是请注意，种类

forall k. k -> k

对

Foo

无效，因为

Foo a

作为数据类型，必须有种类

Type

，而且

[]

的种类是

Type -> Type

。所以亲切的签名

Foo :: Type -> Type

是被逼的

编译没有错误的例子是：

type Foo :: forall k. k -> Type
data Foo a = Foo