为什么 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。 The documentation on datatype promotion for GHC 7.10.3 列出了一个类型可能无法提升的各种原因（例如，如果它已经涉及提升的类型），但我不明白为什么他们会排除 Int。

(1) 为什么会出现这个错误？

作为奖励，

(2) 是否有合理的修复或替代方法？例如，搜索显示 Fixed-Length Vector Types in Haskell，但这似乎过于复杂。

Answer 1

Int 原则上是可以推广的，但是实施工作还没有（还？）完成。它们在术语级别实现为硬件字，原始操作实现为 C 或汇编例程；想要在类型级别（包括 "convert this compile-time constant to an 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 是幻像类型。

为什么 Int 不可提升？

Why is Int not promotable?

haskell

ghc