{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreifvrd2oqtndcb35q6uwgfvtbqlznldco6ncxrsoaek2ppotfqsj5a",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mltqpatfkbv2"
  },
  "path": "/t/knownnat-indexed-vectors/14099?page=2#post_26",
  "publishedAt": "2026-05-14T20:14:21.000Z",
  "site": "https://discourse.haskell.org",
  "textContent": "Thankfully we don’t need `Finite` if you’re indexing known-at-compile-time values:\n\n\n    {- cabal:\n    build-depends: base, primitive\n    default-language: GHC2021\n    -}\n\n    {-# LANGUAGE BlockArguments #-}\n    {-# LANGUAGE LambdaCase #-}\n    {-# LANGUAGE DataKinds #-}\n    {-# LANGUAGE TypeAbstractions #-}\n    {-# LANGUAGE ScopedTypeVariables #-}\n    {-# LANGUAGE RequiredTypeArguments #-}\n    module Main where\n\n    import Data.Primitive.Array\n    import Data.Proxy\n    import GHC.TypeLits\n    import Data.Type.Ord\n\n    newtype V n x = V {unV :: Array x} deriving (Functor)\n\n    indexV :: KnownNat n => V n x -> forall i -> (KnownNat i, i < n) => x\n    indexV (V unV) i' = indexArray unV (fromInteger (natVal (Proxy :: Proxy i')))\n\n    main = do\n      let v :: V 5 Int\n          v = V $ createArray 5 0 $ \\a -> do\n            writeArray a 1 3\n            writeArray a 2 7\n            writeArray a 3 10\n            writeArray a 4 1000\n      print $ v `indexV` 0 -- 0\n      print $ v `indexV` 3 -- 10\n      -- print $ v `indexV` 5 -- does not compile!\n\n\nBuilding off of jaror’s example, you can use required type arguments to index into `V` and know that you can never get an out of bounds access.\n\nI use Array for convenience but this’d work for any internal V representation.",
  "title": "KnownNat-indexed vectors"
}