positive type-level naturals

[Henning Thielemann]

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.