On Fri, Aug 21, 2009 at 8:50 PM, Jason Dagit<da...@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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
