为什么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可能很难推断出类型,因为din Point d是幻像类型.