Just to expand on David's higher-order function for the original Vector type, we can do:
data AnyVec a where AnyVec :: Vec a n -> AnyVec a listToVec :: [a] -> AnyVec a listToVec = worker AnyVec worker :: (forall n. Nat n => Vec a n -> t) -> [a] -> t worker f [] = f Nil worker f (x:xs) = worker (f . (Cons x)) xs and have it behave as you'd expect. Note that in a sense this is "forgetful" of the original length of the list. Dan On Fri, Aug 21, 2009 at 2:03 PM, David Menendez<d...@zednenem.com> wrote: > On Fri, Aug 21, 2009 at 1:03 PM, Jason Dagit<da...@codersbase.com> wrote: >> >> Even with a type class for our type level numbers I'm at a loss. I >> just don't understand how to convert an arbitrary int into an >> arbitrary but fixed type. Perhaps someone else on the list knows. I >> would like to know, if it's possible, how to do it. >> >> toPeano :: Nat n => Int -> n > > The problem is that the parameter, n, is part of the input to toPeano, > but you need it to be part of the output. To rephrase slightly, you > have > > toPeano :: forall n. (Nat n) => Int -> n > > but you need, > > toPeano :: Int -> exists n. (Nat n) => n > > which states that toPeano determines the type of its return value. In > Haskell, you can encode this with an existential data type, > > data SomeNat where SomeNat :: (Nat n) => n -> SomeNat > toPeano :: Int -> SomeNat > > or, equivalently, by using a higher-order function. > > toPeano :: Int -> (forall n. Nat n => n -> t) -> t > > -- > Dave Menendez <d...@zednenem.com> > <http://www.eyrie.org/~zednenem/> > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe