
31 Jan
2008
31 Jan
'08
6:02 a.m.
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