KnownNat-indexed vectors
Haskell Community [Unofficial]
May 13, 2026
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 !)
Discussion in the ATmosphere