{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreigujpmjrzmr2wdwihgtvefyzytxr5k5ks333ukniqe3auxrp27ir4",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mlqz73eb3qv2"
  },
  "path": "/t/knownnat-indexed-vectors/14099#post_3",
  "publishedAt": "2026-05-13T17:24:30.000Z",
  "site": "https://discourse.haskell.org",
  "tags": [
    "@n"
  ],
  "textContent": "To get good performance you probably want to regularly cache the contents (and why use `Natural` instead of `Int`?):\n\n\n    {- cabal:\n    build-depends: base, primitive\n    default-language: GHC2021\n    -}\n\n    {-# LANGUAGE BlockArguments #-}\n    {-# LANGUAGE LambdaCase #-}\n    {-# LANGUAGE TypeAbstractions #-}\n    module T where\n\n    import Data.Primitive.Array\n    import Data.Proxy\n    import GHC.TypeLits\n\n    newtype V n x = V {unV :: Int -> x} deriving (Functor)\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\nBut why not just use arrays at that point?",
  "title": "KnownNat-indexed vectors"
}