1
\$\begingroup\$

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?

\$\endgroup\$

1 Answer 1

1
\$\begingroup\$

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
\$\endgroup\$
1
  • \$\begingroup\$ 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. \$\endgroup\$ Commented Jul 21, 2021 at 0:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.