[Haskell-cafe] How to convert a list to a vector encoding its length in its type?

[Ryan Ingram]

On Mon, Aug 24, 2009 at 4:24 PM, Bas van Dijk<v.dijk.bas at gmail.com> wrote:
> Thanks very much! I'm beginning to understand the code.
>
> The only thing I don't understand is why you need [witnessNat]
>
>> toList = ... induction (witnessNat :: n) ...
>> fromList = ... induction (witnessNat :: n) ...
>
> However the following also works:
>
>> toList = ... induction (undefined :: n) ...
>> fromList = ... induction (undefined :: n) ...

Yes, that's true.  But because we have lazy evaluation, witnessNat
never gets evaluated, so it doesn't matter :)

And I prefer to keep the (undefined/error) calls, along with
recursion, in my code to a minimum, since both of those can lead to
_|_ and runtime errors.  So, by keeping the calls to "undefined" and
the use of recursion limited to "induction" and "witnessNat", I create
a very small 'trusted core' of code that has to be checked carefully
for errors.  Other code that uses these functions are entirely safe as
long as we keep those functions total and avoid explicit recursion.

This is why I called out "fromJust" in my example; it's the one use of
non-totality outside of the kernel.

> Although it looks like that a case analysis on 'n' is made at run-time in:
>
>> instance Nat n => Nat (S n) where
>>   caseNat (S n) _ s = s n
>
> But I guess that is desugared away because 'S' is implemented as a newtype:
>
>> newtype S n = S n

Yes, in my original post[1] I comment about this nicety; if I used
"data" instead of "newtype" I would have implemented it as
]  instance Nat Z where caseNat ~Z z _ = z
]  instance Nat n => Nat (S n) where caseNat ~(S n) _ s = s n

> Again, thanks very much for this!
>
> Do you mind if I use this code in the levmar package (soon to be
> released on hackage)?

No problem.  I hereby release this code under the WTFPL[2], version 2
with the "no warranty" clause.

  -- ryan

[1] Lightweight type-level dependent programming in Haskell.
http://www.haskell.org/pipermail/haskell-cafe/2009-June/062690.html
[2] http://sam.zoy.org/wtfpl/