# Build a fixed-length vector from a recursive factory function

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?

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

• This does what I want! The s parameter to VecBuilder turns out to be unnecessary. The newtype seems to be necessary, which is frustrating. It looks like clutter, both in the top-level namespace and also for reading/writing the function. But GHC won't understand how to use induction1 on a -> Vec n a without it. Commented Jul 21, 2021 at 0:33