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

[Bas van Dijk]

On Fri, Aug 21, 2009 at 8:50 PM, Jason Dagit<dagit at codersbase.com> wrote:
>>>    toPeano :: Int -> (forall n. Nat n => n -> t) -> t
>
> This looks a bit more promising.  For those unfamiliar with this form,
> it is the logical "negation" of the previous type.  One description is
> here [1], where it is mentioned that the type of t cannot depend on n.
>  So you could not for example, return Vector a n or do, "toPeano 5
> id".
>
> I guess you end up writing your program inside out in a sense which is
> fine, but then how do you address the forgetfulness?  Everything has
> to be inside one scope where you never wrap things in an existential
> type?  Perhaps via the negated existential encoding your last version
> of toPeano?  I have a hard time wrapping my head around it at this
> point.

I got out of the scope using unsafeCoerce. I think its safe because I
know my levmarML function is correct. However I can't express that in
the type.

Bas