如何通过显式类型量化来定义数据类型？

Question

当我定义

\n

data Foo a = Foo [a]\n

\n

那么类型就是种类Foo :: * -> *。

\n

启用PolyKinds后，RankNTypes我想使用更通用的种类签名来明确量化它 Foo :: forall k . k -> k。

\n

然而我的尝试都没有成功：

\n

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

\n

-- error: parse error on input \xe2\x80\x98::\xe2\x80\x99\n32 | data Foo a = Foo [a] :: forall k . k -> k\n

\n

-- error:\n--     Multiple declarations of \xe2\x80\x98Foo\xe2\x80\x99\n\ndata Foo :: forall k . k -> k\ndata Foo a = Foo [a]\n

\n

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