在 Haskell 中通过整数参数化类型

Question

我正在尝试创建一些 Haskell 类型，这些类型不是按类型而是按类型的元素（特别是整数）参数化的。例如，R^2 中的（线性代数）向量和 R^3 中的向量是不同类型的对象。具体来说，我正在用 Haskell 编写一个 K-D 树，我想用一个正整数参数化我的数据结构，因此 3-D 树和 4-D 树具有不同的类型。

我尝试通过元组对我的树进行参数化，但它似乎并没有去任何地方（而且这似乎不太可能被推动，特别是因为它似乎没有三元组或任何更大的东西函子（我不知道如何说，例如 HomogeneousTuple a => Functor a）。我想做这样的事情：

data (TupleOfDoubles a) => KDTree a b = ... ---so in a 3DTree a is (Double,Double,Double)

那会很好，或者类似的东西也一样好

data KDTree Int a = ... -- The Int is k, so KDTree has kind Int -> * -> *

有人知道这些效果是否可行或合理吗？

谢谢 -约瑟夫

Answer 1

正在开发一个名为 TypeNats 的 GHC 扩展，这正是您想要的。然而，根据the ticket，目前的里程碑设置为 7.4.1，所以还是有点等待。

在该扩展可用之前，您唯一能做的就是使用类型对维度进行编码。例如，沿着这些思路可能会起作用：

{-# LANGUAGE ScopedTypeVariables #-}
class MyTypeNat a where
    toInteger :: a -> Integer

data Zero
data Succ a

instance MyTypeNat Zero where
    toInteger _ = 0

instance MyTypeNat a => MyTypeNat (Succ a) where
    toInteger _ = toInteger (undefined :: a) + 1

data KDTree a b = -- ...

dimension :: forall a b. MyTypeNat a => KDTree a b -> Integer
dimension = toInteger (undefined :: a)

这样的方法的缺点当然是你必须写KDTree (Succ (Succ (Succ Zero))) Foo而不是KDTree 3 Foo。

Answer 2

sepp2k 的回答显示了执行此操作的基本方法。事实上，很多工作已经完成。

类型级号码包

• natural-number 和 type-level-natural-number
• numtype
• type-level

使用自然数类型级编码的东西（示例）

• Vec
• Dimensional
• llvm
• ForSyDe

不幸的是这样的：

data KDTree Int a = ...

真的不可能。最终类型（由KDTree 构造）取决于 Int 的值，这需要一个称为依赖类型的特性。 Agda 和 Epigram 等语言支持这一点，但 Haskell 不支持。