positive type-level naturals
Henning Thielemann
lemming at henning-thielemann.de
Wed Mar 19 22:40:53 UTC 2014
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.
More information about the Glasgow-haskell-users
mailing list