Spine-lazy vector functions

[gergoerdi]

Functions that construct vectors with a known length should be able to produce the spine fully lazily. For example, I don't think there's a good reason why map (const 0) (undefined :: Vec 5 ()) should bottom out.

So I propose rewriting the vector functions a la the following examples:

map :: forall n a b. (KnownNat n) => (a -> b) -> Vec n a -> Vec n b
map f = go (toUNat SNat)
  where
    go :: forall n. UNat n -> Vec n a -> Vec n b
    go UZero     ~Nil       = Nil
    go (USucc n) ~(x :> xs) = f x :> go n xs

zipWith :: forall n a b c. (KnownNat n) => (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith f = go (toUNat SNat)
  where
    go :: forall n. UNat n -> Vec n a -> Vec n b -> Vec n c
    go UZero     ~Nil       ~Nil       = Nil
    go (USucc n) ~(x :> xs) ~(y :> ys) = f x y :> go n xs ys

(I'm including zipWith here to demonstrate how nicely unbiased it becomes with this technique).

[gergoerdi]

As @kleinreact can attest to, I have real-life code where, due to zipWith being unnecessarily strict in its first argument's spine, f <$> x <*> y loops, whereas pure f <*> x <*> y works, which can be hella confusing unless one is aware of zipWith's details.

[gergoerdi]

Related: If KnownNat n, then Vec n can be made a distributive functor, which is basically the generalization of the observation that we can go from Maybe (Vec n a) to Vec n (Maybe a) in the same build-the-spine-from-the-type way.

[gergoerdi]

Hmm, I wanted to start working on this but very quickly realized that map has no KnownNat n constraint, and neither does the Functor (Vec n) instance, so this would actually be quite a big & nasty API change. Sigh.

[DigitalBrains1]

Oh no, that really is too bad. If spine-lazy vector functions are a thing that can work (I really can't gauge its effect on Clash the compiler, which is why I kept quiet in this issue), we should think about whether it's actually worth it to add a KnownNat constraint to map and Functor. In practice, functions you write quite quickly gain a KnownNat constraint, so if we require one for some extra functions, the fallout might be limited. I think you can always add a KnownNat constraint, although it might blow up a bit once you add KnownNat to expressions... then again that particular example type checks fine with just KnownNat d, so it might not be a good example.

(And sometimes you're saved because you have an actual SNat term with which to introduce the constraint)

Anyway, you should probably always use ensureSpine (errorX "[...]") unless you know there is no spine or what you're trying to do has no NFDataX instance. But I understand the desire to not need that here.