Hi Iavor, Am 19.03.2014 22:27, schrieb Iavor Diatchki:
I see two separate issues that show in what you describe, so it might be useful to discuss them separately:
Thank you and Richard Eisenberg for the detailed explanations. For now, I have just fooled GHC by unsafeCoerceing dictionaries as suggested by Richard.
A general comment: the function `withVec` is fairly tricky because it introduces vectors whose length is not known statically. This tends to require much more advanced tools because one has to do real mathematical reasoning about abstract values. Of course, sometimes there is no way around this, but on occasion one can avoid it. For example, in the expression `withVec 1 [2,3,4]` we know exactly the length of the vectors involved, so there is no reason to resort to using fancy reasoning. The problem is that Haskell's list notation does not tell us the length of the list literal. One could imagine writing a little quasi-quoter that will allow us to write things like `[vec| 1, 2, 3, 4]`, which would generate the correctly sized vector. Then you can append and manipulate these as usual and GHC will be able to check the types because it only has to work with concrete numbers. This is not a great program verification technique, but it certainly beats having to do it manually :-)
For this problem I have a simple solution. I think that the infix list syntax is underrated. If you are used to write 1:2:3:4:[], then you have no problem writing: x = 1:.2:.3:.4:.End with data OneMore f a = a :. f a data End a = End Then x has type (OneMore (OneMore (OneMore (OneMore End))) a) and GHC can easily derive the static list length from it.