Parameterizing types by integers in Haskell

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

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.

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

• natural-number and type-level-natural-number
• numtype
• type-level

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

• Vec
• Dimensional
• llvm
• ForSyDe

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.