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

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

您可以使用 standalone kind signature :

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