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

[Jason Dagit]

On Fri, Aug 21, 2009 at 4:41 AM, Bas van Dijk<v.dijk.bas at gmail.com> wrote:

> 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