How do I lazily transform a list into this type?

Question

Consider this Vect type:

{-# LANGUAGE GADTs, DataKinds, KindSignatures, RankNTypes #-}

import Data.Kind (Type)

data Nat = Zero | Succ Nat

data Vect :: Nat -> Type -> Type where
  Nil :: Vect 'Zero a
  Cons :: a -> Vect n a -> Vect ('Succ n) a

I'd like to write a function that takes a list and lazily transforms it to this type. Since the length obviously isn't known, we need to use an existential. My first attempt at this used CPS and a rank-2 type to emulate one:

listToVect1 :: [a] -> (forall n. Vect n a -> b) -> b
listToVect1 [] f = f Nil
listToVect1 (x:xs) f = listToVect1 xs (f . Cons x)

However, this isn't lazy. This is just a foldl (though written as explicit recursion because actually using foldl would require impredicativity), so f won't start running until it's gone all the way to the end of the list.

I can't think of a way to do CPS in a right-associative manner, so I tried again, this time with a wrapper type instead:

data ArbitraryVect a = forall n. ArbitraryVect (Vect n a)

nil :: ArbitraryVect a
nil = ArbitraryVect Nil

cons :: a -> ArbitraryVect a -> ArbitraryVect a
cons x (ArbitraryVect xs) = ArbitraryVect (Cons x xs)

listToVect2 :: [a] -> ArbitraryVect a
listToVect2 = foldr cons nil

The problem with this attempt is that I have to use data rather than newtype (or I get A newtype constructor cannot have existential type variables), and I need to pattern-match strictly in cons (or I get An existential or GADT data constructor cannot be used inside a lazy (~) pattern), so it doesn't return anything until it's through the entire list.

I don't have any other ideas for how to do this. Is this even possible? If so, how? If not, why not?

Answer 1

This is going to be an unsatisfying answer, but I'm going to post it anyway.

---

I don't think this is technically possible, because the head of the result should contain the type n, and types cannot be lazily constructed. They're sort of "ephemeral", don't really exist at runtime as such, but logically they have to be fully known.

(I am not 100% sure the above is correct though)

---

However, if you really need to do this, you can cheat. Observe that the polymorphic continuation doesn't actually know anything about n. The only thing it can possibly find out about n is whether it's a Zero or Succ, but even that is not actually encoded at runtime in any way. Instead, it gets inferred from whichever constructor of Vect matches during pattern match. This means that, at runtime, we don't actually have to pass in the correct type for n. Sure, the compiler will get anxious during compilation if it can't prove the type is right, but we can convince it to shut up with unsafeCoerce:

listToVect1 :: [a] -> (forall n. Vect n a -> b) -> b
listToVect1 xs f = f $ go xs
  where
    go :: [a] -> Vect Zero a
    go [] = Nil
    go (x:xs) = unsafeCoerce $ Cons x (go xs)

Here, the second line of go constructs a Vect (Succ Zero) a, but then erases its n component to Zero. This happens at every step, so the ultimate result is always Vect Zero a. This result is then passed to the continuation, which is none the wiser, because it doesn't care.

When the continuation later tries to match on Vect's constructors, it works fine, because the constructors have been instantiated correctly in the right order, reflecting the correct shape of the vector, and by extension, the correct shape of n.

This works, try it:

vectLen :: Vect n a -> Int
vectLen Nil = 0
vectLen (Cons _ xs) = 1 + vectLen xs

toList :: Vect n a -> [a]
toList Nil = []
toList (Cons a xs) = a : toList xs

main :: IO ()
main = do
  print $ listToVect1 [1,2,3] vectLen        -- prints 3
  print $ listToVect1 [] vectLen             -- prints 0
  print $ listToVect1 [1,2,3,4,5] vectLen    -- prints 5

  print $ listToVect1 [1,2,3] toList         -- prints [1,2,3]
  print $ listToVect1 ([] :: [Int]) toList   -- prints []
  print $ listToVect1 [1,2,3,4,5] toList     -- prints [1,2,3,5]

---

Of course, the above is fragile. It relies (to an extent) on some lower-level knowledge. If this is not just a curiosity exercise, I would rather go back and rethink the original problem that lead you to this.

But for what it's worth, this technique of "hiding ugliness by hand-waving" is in a relatively common use in lower-level libraries.