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

Question

给定一个像

这样的 ADT

data K = A | B Bool

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

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

有没有办法将构造函数添加到 K 提升到类型构造函数

'C :: * -> K

?

Answer 1

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

This ticket 记录了声明数据类型的前景，天生的类型，而不是强加于它们的数据类型。此类事物的构造函数按照您的建议打包类型是完全合理的。我们还没有到那一步，但看起来问题不大。

我的目光投向了更大的奖赏。我希望 * 成为完全合理的运行时值类型，以便您想要的类型可以像我们今天拥有的那样通过提升而存在。将其与提出的 pi-type 概念（对类型和值有效共享的语言部分的非参数抽象）相结合，我们可能会得到比我们拥有的更直接的方法来进行临时类型抽象Data.Typeable。通常的 forall 将保持参数化。

Answer 2

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

data K a = ... | C a

那么这个提升为

C :: a -> K a

如果你再使用K *，你就可以达到你想要的效果。

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

Constructor that lifts (via DataKinds) to * -> A

haskell

data-kinds