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.
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
