Build a fixed-length vector from a recursive factory function

Question

I need a function of type forall (n :: Nat). RandomGen q => q -> Vec n q. Obviously this is possible to do (correctly, don't just repeat) using split.

(Documentation links: Nat, RandomGen, Vec, repeat, split, induction1.)

I generalized this to not specifically be about RNGs by taking the splitting/unfolding function as an argument. I'm not wedded to this decision; I don't think it makes much difference.

import Data.Type.Nat (SNatI, induction1)
import Data.Vec.Lazy (Vec(VNil, (:::)))
import qualified Data.Vec.Lazy as Vec

unfold :: SNatI n =>
          (a -> (a, a)) ->
          a ->
          Vec n a
unfold uf value = induction1 VNil (\vs -> let v ::: vs' = vs `Vec.snoc` value
                                              (v', v'') = uf v
                                          in Vec.init $ v' ::: v'' ::: vs')

It works, but it's pretty clunky looking. Also, consider an example like

> import Data.Nat (Nat(Z, S))
> unfold (\n -> (n * 2, n*2)) 1 :: Vec (S(S(S(S(S Z))))) Int
↪ 32 ::: 32 ::: 16 ::: 8 ::: 4 ::: VNil

That's not wrong, but I think it would be just as correct (and less weird looking) if it came out to
32 ::: 16 ::: 8 ::: 4 ::: 2 ::: VNil.

Anyone know what options I'm overlooking?

Answer 1

I am not an expert at type level programming, but from my experience with folds I know that you can add an extra parameter to the result type to implement foldl in terms of foldr. Here is what that would look like in this case:

newtype VecBuilder s m a = VecBuilder { buildVec :: s -> Vec m a }

unfold' :: forall n a. SNatI n =>
          (a -> (a, a)) ->
          a ->
          Vec n a
unfold' uf = buildVec (induction1 (VecBuilder base) (VecBuilder . step))
  where
    base _ = VNil
    step :: forall m. VecBuilder a m a -> a -> Vec (S m) a
    step vs x = let (v', x') = uf x in v' ::: buildVec vs x'

That will produce a nice output:

2 ::: 4 ::: 8 ::: 16 ::: 32 ::: VNil