KnownNat-indexed vectors

Thankfully we don’t need Finite if you’re indexing known-at-compile-time values:

{- cabal:
build-depends: base, primitive
default-language: GHC2021
-}

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RequiredTypeArguments #-}
module Main where

import Data.Primitive.Array
import Data.Proxy
import GHC.TypeLits
import Data.Type.Ord

newtype V n x = V {unV :: Array x} deriving (Functor)

indexV :: KnownNat n => V n x -> forall i -> (KnownNat i, i < n) => x
indexV (V unV) i' = indexArray unV (fromInteger (natVal (Proxy :: Proxy i')))

main = do
  let v :: V 5 Int
      v = V $ createArray 5 0 $ \a -> do
        writeArray a 1 3
        writeArray a 2 7
        writeArray a 3 10
        writeArray a 4 1000
  print $ v `indexV` 0 -- 0
  print $ v `indexV` 3 -- 10
  -- print $ v `indexV` 5 -- does not compile!

Building 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.

I use Array for convenience but this’d work for any internal V representation.