Создайте вектор фиксированной длины из рекурсивной фабричной функции

Мне нужна функция типа forall (n :: Nat). RandomGen q => q -> Vec n q. Очевидно, это возможно (правильно, не просто repeat) с использованием split.

(Ссылки на документацию: Nat, RandomGen, Vec, repeat, split, induction1.)

Я обобщил это на нет в частности, о ГСЧ, принимая в качестве аргумента функцию разделения / разворачивания. Я не привязан к этому решению; Я не думаю, что это имеет большое значение.

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')

Это работает, но выглядит довольно неуклюже. Также рассмотрим такой пример, как

> 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

Это не неправильный, но я думаю, что это было бы так же правильно (и выглядело бы менее странно), если бы
32 ::: 16 ::: 8 ::: 4 ::: 2 ::: VNil.

Кто-нибудь знает, какие варианты я упускаю?

Я не являюсь экспертом в программировании на уровне типов, но по своему опыту работы со складками я знаю, что вы можете добавить дополнительный параметр к типу результата, чтобы реализовать foldl в терминах foldr. Вот как это будет выглядеть в этом случае:

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'

Это даст хороший результат:

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