haskell - 将（通过 DataKinds）提升到 * -> A 的构造函数

Question

给定一个 ADT

data K = A | B Bool

该DataKinds扩展允许我们将其提升为种类和类型/类型构造函数

K :: BOX
'A :: K
'B :: 'Bool -> K

有没有办法向K类型构造函数添加一个构造函数

'C :: * -> K

?

Answer 1

正如康纳所说，这不是直接可能的。但是，您可以定义

data K a = ... | C a

然后这促进

C :: a -> K a

如果你然后使用K *，你可以实现你想要的。

Answer 2

目前，恐怕没有。我也没有发现明显的解决方法。

这张票记录了声明数据类型的前景，天生的类型，而不是带有善意的数据类型。对于此类事物的构造函数来说，按照您的建议打包类型是完全合理的。我们还没有到那里，但它看起来并不那么成问题。

我的眼睛盯着更大的奖品。我希望 * 是完全合理的运行时值类型，以便您想要的那种类型可以通过提升存在，就像我们今天拥有的那样。pi将其与-type的讨论概念（对由类型和值有效共享的语言部分的非参数抽象）结合起来，我们可能会获得一种比使用Data.Typeable. 通常forall将保持参数化。