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
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?