[Haskell-cafe] Implementing fixed-sized vectors (using datatype algebra?)

[Alfonso Acosta]

Hi,

The EDSL implementation (system design) I'm working on would really
benefit from an implementation of fixed-sized vectors.

I thought this would be a generally desired ADT but it turned out I
wasn't able to find an implementation.

I was thinking about  using  datatype algebra plus GADTs to implement
a type-level parameter indicating the size of the vector.

I'm a total noob with regard to GADTs and type-level algebra trickery.
So my questions are:

1) Do you think it is feasible? Can you think about a better approach?

2) An implementation of type-level Naturals would really help. What
has already been done?


Thanks in advance,

Fons