KnownNat-indexed vectors

I’m highly interested in this given I’ve been dealing with vectors matrices and tensors lately. Fun stuff.

I’ve been taking an approach that uses a type family to dispatch to a specific implementation for efficiency. It works, but that is about all I can say about it - I more or less took my functor / foldable / traversable implementation straight from vector, so its not very fancy.

type family V (n :: Nat) (a :: Type) :: Type where
    V 0 a = V0 a
    V 1 a = V1 a
    V 2 a = V2 a
    V 3 a = V3 a
    -- ...
    V n a = BigV n a

data V0 a = V0

data V1 a = V1
    {-# UNPACK #-} !a

data V2 a = V2
    {-# UNPACK #-} !a
    {-# UNPACK #-} !a

data V3 a = V3
    {-# UNPACK #-} !a
    {-# UNPACK #-} !a
    {-# UNPACK #-} !a

-- MemVector is roughly ~ Ptr (MemRep a), from my `memalloc` -backed vector classes
newtype BigV (n :: Nat) a = BigV (MemVector n a)

mixphix:

In this case the instances map/fold/traverse over both of the dimensions, @m and @n. What’s more, the Kronecker product is super easy to exhibit