Haskell 中通过整数参数化类型

发布于 2024-12-02 07:41:50 字数 579 浏览 4 评论 0原文

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

我试图用元组参数化我的树，但它似乎没有去任何地方（而且这似乎不太可能被推动，特别是因为三元组或任何更大的东西似乎都不是函子（并且我不知道有什么方法可以说，例如 HomogeneousTuple 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 -> * -> *

有谁知道这些效果是否有效？是可行还是合理

？ -约瑟夫

原文

I am trying to make some Haskell types which are parametrized not by types but by elements of a type, specifically, integers. For instance, a (linear-algebra) vector in R^2 and a vector in R^3 are different typed objects. Specifically, I am writing a K-D tree in Haskell and I want to parametrize my data-structure by a positive integer so a 3-D tree and 4-D tree have different type.

I've tried to parametrize my tree by tuples, but it didn't seem to be going anywhere (and it seems somewhat unlikely this can be pushed through, especially since it doesn't seem that triples or anything bigger are even functors (and I don't know any way to say like, instance HomogeneousTuple a => Functor a). I want to do something like this:

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

that would be nice, or something like this would be equally good

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

Does anybody know if either of these effects are workable or reasonable?

Thanks
-Joseph

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

栀子花开つ 2024-12-09 07:41:50

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

There's a GHC extension being worked on called TypeNats, which would be exactly what you want. However the milestone for that is currently set to be 7.4.1 according to the ticket, so that'll be a bit of a wait still.

Until that extension is available, the only thing you can do is encode the dimension using types. For example something along these lines might work:

{-# 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)

The downside of an approach like this is of course that you have to write something like KDTree (Succ (Succ (Succ Zero))) Foo instead of KDTree 3 Foo.

回复收藏 0 原文

蓬勃野心 2024-12-09 07:41:50

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

类型级数字包

使用自然数类型级别编码的内容（示例）

不幸的是，这样的事情：

data KDTree Int a = ...

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

sepp2k's answer shows the basic approach to doing this. In fact, a lot of the work has already been done.

Type-level number packages

Stuff using type-level encodings of natural numbers (examples)

Unfortunately something like this:

data KDTree Int a = ...

isn't really possible. The final type (constructed by KDTree) depends on the value of the Int, which requires a feature called dependent types. Languages like Agda and Epigram support this, but not Haskell.

回复收藏 0 原文

~没有更多了~