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