On Fri, Aug 21, 2009 at 8:50 PM, Jason Dagit
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