为什么 Int 不可推广

Question

我希望在二维或三维空间中具有点，以便二维点和三维点可以共享代码，但编译器可以区分它们。 这是第一次尝试。

{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}
data Dimension = D2 | D3
data Point :: Dimension -> * where
  Point :: Dimension -> [Int] -> Point d
origin = Point D2 [0, 0]

到目前为止，这工作正常。 这是一个简化版本：

data Point' :: Int -> * where
  Point' :: Int -> [Int] -> Point' d
origin' = Point' 2 [0, 0]

这不会编译：‘Int’ of kind ‘*’ is not promotable 。 GHC 7.10.3 的数据类型升级文档列出了类型可能无法升级的各种原因（例如，如果它已经涉及升级的类型），但我不明白为什么他们会排除 Int。

（1）为什么会给出这个错误？

作为奖励，

（2）是否有合理的解决方法或替代方法？ 例如，搜索显示 Haskell 中的固定长度向量类型，但这似乎过于复杂。

Answer 1

Int原则上是可推广的，但实现工作尚未完成（尚未？它们在术语级别作为硬件字实现，基元操作实现为 C 或汇编例程;每个这样的操作都希望在类型级别使用（包括"将此编译时常量转换为Int"！需要手工推广，据我所知，这还没有完成。

使用数字的标准代数定义 - 例如Peano nats或位列表 - 相反，因为代数类型可以通过现有实现来提升。虽然我还没有做足够的工作来推荐一个特定的，但在 Hackage 的某个地方应该有几个这些实现。

Answer 2

虽然我不能说为什么Int不可推广，但我可以建议使用类似的可推广类型GHC.TypeLits.Nat。您的第二个示例逐字处理此Point'定义

import GHC.TypeLits
data Point' :: Nat -> * where
    Point' :: Int -> [Int] -> Point' d

我还建议明确键入origin否则 GHC 可能很难推断出类型，因为 Point d 中的d是幻像类型。