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

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 wrote:

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