On Fri, Aug 21, 2009 at 4:41 AM, Bas van Dijk
My single question is: how can I convert a list to a Vector???
fromList :: [b] -> Vector b n fromList = ?
A simpler thing to help you see why this is such a problem is, the problem of how to get a type level natural from Int. data Z = Z newtype S n = S n toPeano :: Int -> n toPeano n = {- what goes here? -} Going the other way is not bad. I found this in an Oleg paper: npred :: S n -> n npred = undefined class Nat n where nat2num :: Num a => n -> a instance Nat Z where nat2num _ = 0 instance Nat n => Nat (S n) where nat2num n = 1 + (nat2num (npred n)) 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 If we had this, we could define the 'AnyVector' that Daniel Peebles suggested. With it, you can write: fromList' :: [b] -> AnyVector b fromList' [] = AnyVector Nil fromList' (b:bs) = case fromList' bs of AnyVector bs' -> AnyVector (b :*: bs') fromList :: (Nat size) => size -> [b] -> Vector b size fromList _ xs = case fromList' xs of -- can't use a where because of existential type AnyVector v -> unsafeCoerce v -- needed due to existential type, but safe-ish because of the type sig of fromList You would expose fromList to the real world (eg., export it from the module but hide fromList'). But, now how to bootstrap 'size'? Perhaps Oleg has a trick for writing the toPeano function I proposed above. With it, you could write a wrapper around fromList like this: fromList2 :: [b] -> Vector b size fromList2 xs = fromList (toPeano (length xs)) -- you may still need to wrap this in unsafeCoerce I found this in a paper about type families which would help in some cases: type family Add a b type instance Add Z a = a type instance Add (S a) b = S (Add a b) appendVec :: Vector a n -> Vector a m -> Vector a (Add n m) appendVec Nil y = y appendVec (x:*:xs) ys = x :*: (xs `appendVec` ys) For a brief second I thought it may be possible to define fromList in terms of appendVec. For example, you wrote a fold to and used appendVec you could append them all together. That quickly gets you back to the problem of "What peano number corresponds to the length of a given list?". I'd love to see what you figure out. Jason