External Publication
Visit Post

KnownNat-indexed vectors

Haskell Community [Unofficial] May 13, 2026
Source

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

Loading comments...