First pass of statically-lengthed vectors

FixedVector.hs

{-# LANGUAGE DataKinds, KindSignatures, TypeOperators, ScopedTypeVariables, TypeFamilies #-}

import Prelude hiding (length)
import qualified Data.Vector as V
import qualified GHC.TypeLits as T
import qualified Data.Proxy as P

newtype FVec a (n :: T.Nat) = FVec (V.Vector a) deriving (Show, Eq)

type a ^ n = FVec a n

empty :: a ^ 0
empty = FVec V.empty

singleton :: a -> a ^ 1
singleton = FVec . V.singleton

length :: forall a n. (T.KnownNat n) => a ^ n -> Integer
length _ = T.natVal (P.Proxy :: P.Proxy n)

intLength :: forall a n. (T.KnownNat n) => a ^ n -> Int
intLength = fromInteger . length

replicate :: forall a n. (T.KnownNat n) => a -> a ^ n
replicate = FVec . V.replicate (intLength (undefined :: a ^ n))

generate :: forall a n. (T.KnownNat n) => (Int -> a) -> a ^ n
generate = FVec . V.generate (intLength (undefined :: a ^ n))

iterate :: forall a n. (T.KnownNat n) => (a -> a) -> a -> a ^ n
iterate f = FVec . V.iterateN (intLength (undefined :: a ^ n)) f

(<>) :: a ^ m -> a ^ n -> a ^ (m T.+ n)
(FVec x) <> (FVec y) = FVec (x V.++ y)

trimEnd :: forall a m n. (T.KnownNat n) => (n T.<= m) => a ^ m -> a ^ n
trimEnd (FVec x) = FVec $ V.unsafeTake (intLength (undefined :: a ^ n)) x

trimStart :: forall a m n. (T.KnownNat m, T.KnownNat n) => (n T.<= m) => a ^ m -> a ^ n
trimStart (FVec x) = FVec $ V.unsafeDrop toDrop x
        where
        toDrop = intLength (undefined :: a ^ m) - intLength (undefined :: a ^ n)


fiveEls :: Int ^ 5
fiveEls = FVec $ V.fromList [1..5]

-- no need to specify how many to drop as it's
-- determined by the result type
fourEls, fourEls' :: Int ^ 4
fourEls = trimStart fiveEls
fourEls' = trimEnd fiveEls