KnownNat-indexed vectors

[oisdk]

@jaror

cache :: KnownNat n => V n x -> V n x
cache @n (V f) = 
  let 
    n = fromIntegral (natVal (Proxy @n)) :: Int
    arr = createArray n undefined $ \m -> do
      let go i
            | i < n = writeArray m i (f i) *> go (i + 1)
            | otherwise = pure ()
      go 0
  in V (indexArray arr)

Data.Array is lazy, so you can just write the memoized version directly:

cache :: KnownNat n => V n x -> V n x
cache @n (V f) = 
  let 
    n = fromIntegral (natVal (Proxy @n)) :: Int
    arr = array (0,n-1) [ (i, f i) | i <- [0..n-1] ]
  in V (arr !)