KnownNat-indexed vectors

To get good performance you probably want to regularly cache the contents (and why use Natural instead of Int?):

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

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeAbstractions #-}
module T where

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

newtype V n x = V {unV :: Int -> x} deriving (Functor)

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)

But why not just use arrays at that point?

1 Like