Geek Answers Handbook

Parameterization of types by integers in Haskell

I am trying to create some Haskell types that are parameterized not by types, but by type elements, in particular integers. For example, a vector (linear algebra) in R ^ 2 and a vector in R ^ 3 are different typed objects. In particular, I write a KD tree in Haskell, and I want to parameterize my data structure with a positive integer, so the three-dimensional tree and 4-D tree are of a different type.

I tried to parameterize my tree by tuples, but it seems that it will not go anywhere (and it seems that this is unlikely, it can be skipped, especially since it does not seem that triples or anything more functors (and I don’t know, how to say an instance of HomogeneousTuple a => Functor a). I want to do something like this:

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

which would be good, or something like that would be equally good

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

Does anyone know if any of these effects are workable or reasonable?

Thanks joseph

+7
source share
2 answers

There works a GHC extension called TypeNats , which would be exactly what you want. However, this milestone for this is currently set to 7.4.1 according to the ticket , so this will wait a bit.

Until this extension is available, the only thing you can do is encode the dimension using types. For example, something like 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 ab = -- ... dimension :: forall a b. MyTypeNat a => KDTree ab -> Integer dimension = toInteger (undefined :: a)

The disadvantage of this approach is, of course, that you should write something like KDTree (Succ (Succ (Succ Zero))) Foo instead of KDTree 3 Foo .

+5
source
Answer to

sepp2k shows a basic approach to this. In fact, most of the work has already been completed.

Type Type Number Packages

Material using encodings at the natural level (examples)

Unfortunately, something like this:

 data KDTree Int a = ...

really impossible. The final type (built by KDTree ) depends on the value of Int, which requires a function called dependent types. Languages ​​like Agda and Epigram support this, but not Haskell.

+3
source

More articles:


All Articles