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

Question

给定ADT之类的

data K = A | B Bool

该DataKinds扩展可以让我们把它提升到种类和类型/类型构造

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

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

'C :: * -> K

？

Answer 1

正如Conor所说,这不是直接可能的.但是,您可以定义

data K a = ... | C a

然后这促进了

C :: a -> K a

如果您随后使用K *,您可以实现您想要的.

Answer 2

目前,我不敢.我也没有发现明显的解决方法.

这张票证明了数据类型声明的前景,天生的种类,而非数据类型,以及对它们的善意.对于这类事物的构造者来说,按照你的建议打包类型是完全合理的.我们还没有,但看起来并不是那么有问题.

我的眼睛获得了更大的奖励.我希望*是完全合理的运行时值类型,因此您希望的类型可以通过促销存在,就像我们今天所拥有的那样.将它与pi-type的概念结合起来(对于由类型和值有效共享的语言部分进行非参数抽象),我们可能会得到一种比我们更直接的方式来制作临时类型抽象Data.Typeable.通常forall会保持参数化.