在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 -> * -> *

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

谢谢 - Joseph

- Joseph Victor

---

你可能会对一些关于依赖类型的文献感兴趣，它是一种更一般的从值到类型的函数类型：我喜欢 http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf 。 - Amos Robinson

谢谢Amos，那看起来是我可以使用的东西。 - Joseph Victor

Answer 1

目前有一个名为TypeNats的GHC扩展正在开发中，它正是您想要的。然而，根据该票证，该里程碑目前设定为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。

- sepp2k

---

当然，但是一个类型为Three = Succ (Succ (Succ Zero))的变量会有所帮助。 - Ingo

如果你只需要使用小数字，那么直接对它们进行编码会更容易阅读：数据一/数据二/数据三/数据四。 - firefrorefiddle

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不支持。

- John L

---

谢谢。对我来说，Vec似乎是最简单的例子，让我学会如何做到这一点。 - Joseph Victor

是的，Vec可能是最简单的，然后是Dimensional。LLVM和ForSyDe更加复杂，尽管我认为它们基本上只是实现与Vec相同的东西。 - John L