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

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