7

我正在尝试制作一些 Haskell 类型，这些类型不是按类型而是按类型的元素（特别是整数）进行参数化。例如，R^2 中的（线性代数）向量和 R^3 中的向量是不同类型的对象。具体来说，我正在用 Haskell 编写一个 KD 树，我想用一个正整数参数化我的数据结构，因此 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 -> * -> *

有人知道这些效果中的任何一个是否可行或合理吗？

谢谢-约瑟夫

4

2 回答 2

5

有一个名为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.

于 2011-09-01T07:38:17.790 回答
3

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

类型级号码包

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

不幸的是这样的：

data KDTree Int a = ...

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

于 2011-09-01T09:21:59.297 回答