{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreieum7g7y264cpak7k25c2n42iqxggmc2cewdioiplckzjsvp54eai",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mlr7vxwdk6e2"
  },
  "path": "/t/knownnat-indexed-vectors/14099#post_11",
  "publishedAt": "2026-05-13T19:39:45.000Z",
  "site": "https://discourse.haskell.org",
  "tags": [
    "@n"
  ],
  "textContent": "jaror:\n\n>\n>     cache :: KnownNat n => V n x -> V n x\n>     cache @n (V f) =\n>       let\n>         n = fromIntegral (natVal (Proxy @n)) :: Int\n>         arr = createArray n undefined $ \\m -> do\n>           let go i\n>                 | i < n = writeArray m i (f i) *> go (i + 1)\n>                 | otherwise = pure ()\n>           go 0\n>       in V (indexArray arr)\n>\n\n`Data.Array` is lazy, so you can just write the memoized version directly:\n\n\n    cache :: KnownNat n => V n x -> V n x\n    cache @n (V f) =\n      let\n        n = fromIntegral (natVal (Proxy @n)) :: Int\n        arr = array (0,n-1) [ (i, f i) | i <- [0..n-1] ]\n      in V (arr !)\n",
  "title": "KnownNat-indexed vectors"
}