-- |
-- Module      : Vector
-- License     : BSD-3-Clause
-- Copyright   : (c) 2025 Olivier Chéron
--
-- A vector of lifted elements with the vector dimension at type level.
-- Backed by type t'SmallArray' from primitive.
--
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Vector
    ( Vector, Vector.concatMap, Vector.dot
    , Vector.fold1ZipWith, Vector.biMulFoldIndexWith, Vector.toNormalForm
    , Vector.create, Vector.index
#ifdef ML_KEM_TESTING
    , Vector.replicateM
#endif
    ) where

import Data.Primitive.SmallArray

import Control.DeepSeq (NFData(..))
#ifdef ML_KEM_TESTING
import Control.Monad
#endif
import Control.Monad.ST

#if !(MIN_VERSION_base(4,20,0))
import Data.List (foldl')
#endif
import Data.Proxy

import Base
import Iterate
import Math

type Array = SmallArray
type MArray ty s = SmallMutableArray s ty

newtype Vector (n :: Nat) a = Vector { forall (n :: Nat) a. Vector n a -> Array a
unVector :: Array a }
    deriving (Vector n a -> Vector n a -> Bool
(Vector n a -> Vector n a -> Bool)
-> (Vector n a -> Vector n a -> Bool) -> Eq (Vector n a)
forall (n :: Nat) a. Eq a => Vector n a -> Vector n a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (n :: Nat) a. Eq a => Vector n a -> Vector n a -> Bool
== :: Vector n a -> Vector n a -> Bool
$c/= :: forall (n :: Nat) a. Eq a => Vector n a -> Vector n a -> Bool
/= :: Vector n a -> Vector n a -> Bool
Eq, Int -> Vector n a -> ShowS
[Vector n a] -> ShowS
Vector n a -> String
(Int -> Vector n a -> ShowS)
-> (Vector n a -> String)
-> ([Vector n a] -> ShowS)
-> Show (Vector n a)
forall (n :: Nat) a. Show a => Int -> Vector n a -> ShowS
forall (n :: Nat) a. Show a => [Vector n a] -> ShowS
forall (n :: Nat) a. Show a => Vector n a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (n :: Nat) a. Show a => Int -> Vector n a -> ShowS
showsPrec :: Int -> Vector n a -> ShowS
$cshow :: forall (n :: Nat) a. Show a => Vector n a -> String
show :: Vector n a -> String
$cshowList :: forall (n :: Nat) a. Show a => [Vector n a] -> ShowS
showList :: [Vector n a] -> ShowS
Show)

instance Functor (Vector n) where
    fmap :: forall a b. (a -> b) -> Vector n a -> Vector n b
fmap = (a -> b) -> Vector n a -> Vector n b
forall a b (n :: Nat). (a -> b) -> Vector n a -> Vector n b
mapVector
    {-# INLINE fmap #-}

instance (Add a, KnownNat n) => Add (Vector n a) where
    zero :: Vector n a
zero = (Offset a -> a) -> Vector n a
forall (n :: Nat) a. KnownNat n => (Offset a -> a) -> Vector n a
create (a -> Offset a -> a
forall a b. a -> b -> a
const a
forall a. Add a => a
zero)
    {-# INLINE zero #-}
    .+ :: Vector n a -> Vector n a -> Vector n a
(.+) = (a -> a -> a) -> Vector n a -> Vector n a -> Vector n a
forall a b c (n :: Nat).
(a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
Vector.zipWith a -> a -> a
forall a. Add a => a -> a -> a
(.+)
    {-# INLINE (.+) #-}
    .- :: Vector n a -> Vector n a -> Vector n a
(.-) = (a -> a -> a) -> Vector n a -> Vector n a -> Vector n a
forall a b c (n :: Nat).
(a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
Vector.zipWith a -> a -> a
forall a. Add a => a -> a -> a
(.-)
    {-# INLINE (.-) #-}
    neg :: Vector n a -> Vector n a
neg = (a -> a) -> Vector n a -> Vector n a
forall a b (n :: Nat). (a -> b) -> Vector n a -> Vector n b
mapVector a -> a
forall a. Add a => a -> a
neg
    {-# INLINE neg #-}

arrayCreate :: forall ty. CountOf ty -> (Offset ty -> ty) -> Array ty
arrayCreate :: forall ty. CountOf ty -> (Offset ty -> ty) -> Array ty
arrayCreate CountOf ty
n Offset ty -> ty
initializer = (forall s. ST s (Array ty)) -> Array ty
forall a. (forall s. ST s a) -> a
runST (CountOf ty -> ST s (MArray ty (PrimState (ST s)))
forall (prim :: * -> *) ty.
PrimMonad prim =>
CountOf ty -> prim (MArray ty (PrimState prim))
arrayNew CountOf ty
n ST s (SmallMutableArray s ty)
-> (SmallMutableArray s ty -> ST s (Array ty)) -> ST s (Array ty)
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Offset ty -> ty)
-> MArray ty (PrimState (ST s)) -> ST s (Array ty)
forall (prim :: * -> *).
PrimMonad prim =>
(Offset ty -> ty) -> MArray ty (PrimState prim) -> prim (Array ty)
iter Offset ty -> ty
initializer)
  where
    iter :: PrimMonad prim => (Offset ty -> ty) -> MArray ty (PrimState prim) -> prim (Array ty)
    iter :: forall (prim :: * -> *).
PrimMonad prim =>
(Offset ty -> ty) -> MArray ty (PrimState prim) -> prim (Array ty)
iter Offset ty -> ty
f MArray ty (PrimState prim)
ma = Offset ty -> prim (Array ty)
loop Offset ty
0
      where
        loop :: Offset ty -> prim (Array ty)
loop s :: Offset ty
s@(Offset Int
i)
            | Offset ty
s Offset ty -> CountOf ty -> Bool
forall ty. Offset ty -> CountOf ty -> Bool
.==# CountOf ty
n = MArray ty (PrimState prim) -> prim (Array ty)
forall (m :: * -> *) a.
PrimMonad m =>
SmallMutableArray (PrimState m) a -> m (SmallArray a)
unsafeFreezeSmallArray MArray ty (PrimState prim)
ma
            | Bool
otherwise = MArray ty (PrimState prim) -> Int -> ty -> prim ()
forall (m :: * -> *) a.
PrimMonad m =>
SmallMutableArray (PrimState m) a -> Int -> a -> m ()
writeSmallArray MArray ty (PrimState prim)
ma Int
i (Offset ty -> ty
f Offset ty
s) prim () -> prim (Array ty) -> prim (Array ty)
forall a b. prim a -> prim b -> prim b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Offset ty -> prim (Array ty)
loop (Offset ty
s Offset ty -> Offset ty -> Offset ty
forall a. Num a => a -> a -> a
+ Offset ty
1)
        {-# INLINE loop #-}
    {-# INLINE iter #-}

arrayLength :: Array ty -> CountOf ty
arrayLength :: forall ty. Array ty -> CountOf ty
arrayLength = Int -> CountOf ty
forall ty. Int -> CountOf ty
CountOf (Int -> CountOf ty) -> (Array ty -> Int) -> Array ty -> CountOf ty
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Array ty -> Int
forall a. SmallArray a -> Int
sizeofSmallArray

arrayMap :: (a -> b) -> Array a -> Array b
arrayMap :: forall a b. (a -> b) -> Array a -> Array b
arrayMap a -> b
f Array a
a = CountOf b -> (Offset b -> b) -> Array b
forall ty. CountOf ty -> (Offset ty -> ty) -> Array ty
arrayCreate (Int -> CountOf b
forall ty. Int -> CountOf ty
CountOf Int
sz) ((Offset b -> b) -> Array b) -> (Offset b -> b) -> Array b
forall a b. (a -> b) -> a -> b
$ \(Offset Int
i) -> a -> b
f (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ Array a -> Offset a -> a
forall a. Array a -> Offset a -> a
arrayIndex Array a
a (Int -> Offset a
forall ty. Int -> Offset ty
Offset Int
i)
  where CountOf Int
sz = Array a -> CountOf a
forall ty. Array ty -> CountOf ty
arrayLength Array a
a

arrayNew :: PrimMonad prim => CountOf ty -> prim (MArray ty (PrimState prim))
arrayNew :: forall (prim :: * -> *) ty.
PrimMonad prim =>
CountOf ty -> prim (MArray ty (PrimState prim))
arrayNew (CountOf Int
c) = Int -> ty -> prim (SmallMutableArray (PrimState prim) ty)
forall (m :: * -> *) a.
PrimMonad m =>
Int -> a -> m (SmallMutableArray (PrimState m) a)
newSmallArray Int
c ty
forall {a}. a
placeholder
  where placeholder :: a
placeholder = String -> a
forall a. HasCallStack => String -> a
error String
"arrayNew: unexpected evaluation"

create :: forall n a. KnownNat n => (Offset a -> a) -> Vector n a
create :: forall (n :: Nat) a. KnownNat n => (Offset a -> a) -> Vector n a
create = (Offset a -> a) -> Vector n a
forall (n :: Nat) a a'.
KnownNat n =>
(Offset a' -> a) -> Vector n a
genericCreate
{-# INLINE create #-}

genericCreate :: forall n a a'. KnownNat n => (Offset a' -> a) -> Vector n a
genericCreate :: forall (n :: Nat) a a'.
KnownNat n =>
(Offset a' -> a) -> Vector n a
genericCreate Offset a' -> a
f = Array a -> Vector n a
forall (n :: Nat) a. Array a -> Vector n a
Vector (Array a -> Vector n a) -> Array a -> Vector n a
forall a b. (a -> b) -> a -> b
$ CountOf a -> (Offset a -> a) -> Array a
forall ty. CountOf ty -> (Offset ty -> ty) -> Array ty
arrayCreate (Int -> CountOf a
forall ty. Int -> CountOf ty
CountOf Int
sz) (\(Offset !Int
i) -> Offset a' -> a
f (Int -> Offset a'
forall ty. Int -> Offset ty
Offset Int
i))
  where !sz :: Int
sz = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
{-# INLINE [0] genericCreate #-}

genericCreateZipLeft :: KnownNat n => (a -> b -> c) -> (Offset a' -> a) -> Vector n b -> Vector n c
genericCreateZipLeft :: forall (n :: Nat) a b c a'.
KnownNat n =>
(a -> b -> c) -> (Offset a' -> a) -> Vector n b -> Vector n c
genericCreateZipLeft a -> b -> c
f Offset a' -> a
g Vector n b
a = (Offset a' -> c) -> Vector n c
forall (n :: Nat) a a'.
KnownNat n =>
(Offset a' -> a) -> Vector n a
genericCreate ((Offset a' -> c) -> Vector n c) -> (Offset a' -> c) -> Vector n c
forall a b. (a -> b) -> a -> b
$ \off :: Offset a'
off@(Offset Int
i) -> a -> b -> c
f (Offset a' -> a
g Offset a'
off) (Vector n b -> Offset b -> b
forall (n :: Nat) a. Vector n a -> Offset a -> a
index Vector n b
a (Int -> Offset b
forall ty. Int -> Offset ty
Offset Int
i))
{-# INLINE [0] genericCreateZipLeft #-}

genericCreateZipRight :: KnownNat n => (a -> b -> c) -> (Offset b' -> b) -> Vector n a -> Vector n c
genericCreateZipRight :: forall (n :: Nat) a b c b'.
KnownNat n =>
(a -> b -> c) -> (Offset b' -> b) -> Vector n a -> Vector n c
genericCreateZipRight a -> b -> c
f Offset b' -> b
g Vector n a
a = (Offset b' -> c) -> Vector n c
forall (n :: Nat) a a'.
KnownNat n =>
(Offset a' -> a) -> Vector n a
genericCreate ((Offset b' -> c) -> Vector n c) -> (Offset b' -> c) -> Vector n c
forall a b. (a -> b) -> a -> b
$ \off :: Offset b'
off@(Offset Int
i) -> a -> b -> c
f (Vector n a -> Offset a -> a
forall (n :: Nat) a. Vector n a -> Offset a -> a
index Vector n a
a (Int -> Offset a
forall ty. Int -> Offset ty
Offset Int
i)) (Offset b' -> b
g Offset b'
off)
{-# INLINE [0] genericCreateZipRight #-}

mapVector :: (a -> b) -> Vector n a -> Vector n b
mapVector :: forall a b (n :: Nat). (a -> b) -> Vector n a -> Vector n b
mapVector a -> b
f = Array b -> Vector n b
forall (n :: Nat) a. Array a -> Vector n a
Vector (Array b -> Vector n b)
-> (Vector n a -> Array b) -> Vector n a -> Vector n b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> b) -> Array a -> Array b
forall a b. (a -> b) -> Array a -> Array b
arrayMap a -> b
f (Array a -> Array b)
-> (Vector n a -> Array a) -> Vector n a -> Array b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector n a -> Array a
forall (n :: Nat) a. Vector n a -> Array a
unVector
{-# INLINE [0] mapVector #-}

arrayIndex :: Array a -> Offset a -> a
#ifdef ML_KEM_TESTING
arrayIndex a off@(Offset i) =
    checkBounds (arrayLength a) off $ indexSmallArray a i

replicateM :: forall n m a. (KnownNat n, Applicative m) => m a -> m (Vector n a)
replicateM f = Vector . smallArrayFromList <$> Control.Monad.replicateM sz f
  where !sz = fromIntegral $ natVal (Proxy :: Proxy n)
#else
arrayIndex :: forall a. Array a -> Offset a -> a
arrayIndex Array a
a (Offset Int
i) = Array a -> Int -> a
forall a. SmallArray a -> Int -> a
indexSmallArray Array a
a Int
i
#endif

index :: Vector n a -> Offset a -> a
index :: forall (n :: Nat) a. Vector n a -> Offset a -> a
index = Array a -> Offset a -> a
forall a. Array a -> Offset a -> a
arrayIndex (Array a -> Offset a -> a)
-> (Vector n a -> Array a) -> Vector n a -> Offset a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector n a -> Array a
forall (n :: Nat) a. Vector n a -> Array a
unVector

concatMap :: Monoid b => (a -> b) -> Vector n a -> b
concatMap :: forall b a (n :: Nat). Monoid b => (a -> b) -> Vector n a -> b
concatMap a -> b
f = [b] -> b
forall a. Monoid a => [a] -> a
mconcat ([b] -> b) -> (Vector n a -> [b]) -> Vector n a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> Vector n a -> [b]
forall a b (n :: Nat). (a -> b) -> Vector n a -> [b]
mapToList a -> b
f
{-# INLINE concatMap #-}

mapToList :: (a -> b) -> Vector n a -> [b]
mapToList :: forall a b (n :: Nat). (a -> b) -> Vector n a -> [b]
mapToList a -> b
f (Vector Array a
a) = (Int -> b) -> [Int] -> [b]
forall a b. (a -> b) -> [a] -> [b]
Prelude.map (a -> b
f (a -> b) -> (Int -> a) -> Int -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Array a -> Offset a -> a
forall a. Array a -> Offset a -> a
arrayIndex Array a
a (Offset a -> a) -> (Int -> Offset a) -> Int -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Offset a
forall ty. Int -> Offset ty
Offset) (Int -> [Int]
offsets Int
sa)
  where CountOf Int
sa = Array a -> CountOf a
forall ty. Array ty -> CountOf ty
arrayLength Array a
a

zipWith :: (a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
zipWith :: forall a b c (n :: Nat).
(a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
zipWith a -> b -> c
f (Vector Array a
a) (Vector !Array b
b) = Array c -> Vector n c
forall (n :: Nat) a. Array a -> Vector n a
Vector (Array c -> Vector n c) -> Array c -> Vector n c
forall a b. (a -> b) -> a -> b
$
    CountOf c -> (Offset c -> c) -> Array c
forall ty. CountOf ty -> (Offset ty -> ty) -> Array ty
arrayCreate (Int -> CountOf c
forall ty. Int -> CountOf ty
CountOf Int
sa) ((Offset c -> c) -> Array c) -> (Offset c -> c) -> Array c
forall a b. (a -> b) -> a -> b
$ \(Offset Int
i) ->
        a -> b -> c
f (Array a -> Offset a -> a
forall a. Array a -> Offset a -> a
arrayIndex Array a
a (Int -> Offset a
forall ty. Int -> Offset ty
Offset Int
i)) (Array b -> Offset b -> b
forall a. Array a -> Offset a -> a
arrayIndex Array b
b (Int -> Offset b
forall ty. Int -> Offset ty
Offset Int
i))
  where
    CountOf Int
sa = Array a -> CountOf a
forall ty. Array ty -> CountOf ty
arrayLength Array a
a
{-# INLINE [0] zipWith #-}

fold1ZipWith :: (c -> a -> b -> c) -> (a -> b -> c) -> Vector n a -> Vector n b -> c
fold1ZipWith :: forall c a b (n :: Nat).
(c -> a -> b -> c)
-> (a -> b -> c) -> Vector n a -> Vector n b -> c
fold1ZipWith c -> a -> b -> c
f a -> b -> c
g (Vector Array a
a) (Vector !Array b
b) =
    (c -> Int -> c) -> c -> [Int] -> c
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' c -> Int -> c
ff c
gg (Int -> Int -> [Int]
offsetsFrom Int
1 Int
sa)
  where
    ff :: c -> Int -> c
ff c
x Int
i = c -> a -> b -> c
f c
x (Array a -> Offset a -> a
forall a. Array a -> Offset a -> a
arrayIndex Array a
a (Int -> Offset a
forall ty. Int -> Offset ty
Offset Int
i)) (Array b -> Offset b -> b
forall a. Array a -> Offset a -> a
arrayIndex Array b
b (Int -> Offset b
forall ty. Int -> Offset ty
Offset Int
i))
    gg :: c
gg = a -> b -> c
g (Array a -> Offset a -> a
forall a. Array a -> Offset a -> a
arrayIndex Array a
a Offset a
0) (Array b -> Offset b -> b
forall a. Array a -> Offset a -> a
arrayIndex Array b
b Offset b
0)
    CountOf !Int
sa = Array a -> CountOf a
forall ty. Array ty -> CountOf ty
arrayLength Array a
a
{-# INLINE fold1ZipWith #-}

biMulFoldIndexWith :: BiMulAdd b a => (Offset ty -> t -> (b, a)) -> a -> Vector n t -> a
biMulFoldIndexWith :: forall b a ty t (n :: Nat).
BiMulAdd b a =>
(Offset ty -> t -> (b, a)) -> a -> Vector n t -> a
biMulFoldIndexWith Offset ty -> t -> (b, a)
f a
c (Vector Array t
a) =
    a -> [(b, a)] -> a
forall b a (t :: * -> *).
(BiMulAdd b a, Foldable t) =>
a -> t (b, a) -> a
forall (t :: * -> *). Foldable t => a -> t (b, a) -> a
biMulFold a
c ((Int -> (b, a)) -> [Int] -> [(b, a)]
forall a b. (a -> b) -> [a] -> [b]
map Int -> (b, a)
g ([Int] -> [(b, a)]) -> [Int] -> [(b, a)]
forall a b. (a -> b) -> a -> b
$ Int -> [Int]
offsets Int
sa)
  where
    g :: Int -> (b, a)
g Int
i = Offset ty -> t -> (b, a)
f (Int -> Offset ty
forall ty. Int -> Offset ty
Offset Int
i) (Array t -> Offset t -> t
forall a. Array a -> Offset a -> a
arrayIndex Array t
a (Int -> Offset t
forall ty. Int -> Offset ty
Offset Int
i))
    CountOf !Int
sa = Array t -> CountOf t
forall ty. Array ty -> CountOf ty
arrayLength Array t
a
{-# INLINE biMulFoldIndexWith #-}

dot :: BiMulAdd b a => Vector n b -> Vector n a -> a
dot :: forall b a (n :: Nat).
BiMulAdd b a =>
Vector n b -> Vector n a -> a
dot (Vector Array b
b) (Vector Array a
a) =
    a -> [(b, a)] -> a
forall b a (t :: * -> *).
(BiMulAdd b a, Foldable t) =>
a -> t (b, a) -> a
forall (t :: * -> *). Foldable t => a -> t (b, a) -> a
biMulFold (Array b -> Offset b -> b
forall a. Array a -> Offset a -> a
arrayIndex Array b
b Offset b
0 b -> a -> a
forall b a. BiMul b a => b -> a -> a
..* Array a -> Offset a -> a
forall a. Array a -> Offset a -> a
arrayIndex Array a
a Offset a
0) ((Int -> (b, a)) -> [Int] -> [(b, a)]
forall a b. (a -> b) -> [a] -> [b]
map Int -> (b, a)
g ([Int] -> [(b, a)]) -> [Int] -> [(b, a)]
forall a b. (a -> b) -> a -> b
$ Int -> Int -> [Int]
offsetsFrom Int
1 Int
sb)
  where
    g :: Int -> (b, a)
g Int
i = (Array b -> Offset b -> b
forall a. Array a -> Offset a -> a
arrayIndex Array b
b (Int -> Offset b
forall ty. Int -> Offset ty
Offset Int
i), Array a -> Offset a -> a
forall a. Array a -> Offset a -> a
arrayIndex Array a
a (Int -> Offset a
forall ty. Int -> Offset ty
Offset Int
i))
    CountOf !Int
sb = Array b -> CountOf b
forall ty. Array ty -> CountOf ty
arrayLength Array b
b
{-# INLINE dot #-}

toNormalForm :: NFData a => Vector n a -> ()
toNormalForm :: forall a (n :: Nat). NFData a => Vector n a -> ()
toNormalForm = (() -> a -> ()) -> () -> SmallArray a -> ()
forall b a. (b -> a -> b) -> b -> SmallArray a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\()
acc a
x -> ()
acc () -> () -> ()
forall a b. a -> b -> b
`seq` a -> ()
forall a. NFData a => a -> ()
rnf a
x) () (SmallArray a -> ())
-> (Vector n a -> SmallArray a) -> Vector n a -> ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector n a -> SmallArray a
forall (n :: Nat) a. Vector n a -> Array a
unVector

{-# RULES
"mapVector/mapVector" [~0] forall f g a. mapVector f (mapVector g a) = mapVector (f . g) a
"mapVector/genericCreate" [~0] forall f g. mapVector f (genericCreate g) = genericCreate (f . g)
"zipWith/genericCreate left" [~0] forall f g b. Vector.zipWith f (genericCreate g) b = genericCreateZipLeft f g b
"zipWith/genericCreate right" [~0] forall f g a. Vector.zipWith f a (genericCreate g) = genericCreateZipRight f g a
"genericCreateZipLeft/mapVector" [~0] forall f g h b. genericCreateZipLeft f g (mapVector h b) = genericCreateZipLeft (\aa bb -> f aa (h bb)) g b
"genericCreateZipRight/mapVector" [~0] forall f g h a. genericCreateZipRight f g (mapVector h a) = genericCreateZipRight (f . h) g a
"genericCreateZipLeft/genericCreate" [~0] forall f g h. genericCreateZipLeft f g (genericCreate h) = genericCreate $ \(Offset i) -> f (g (Offset i)) (h (Offset i))
"genericCreateZipRight/genericCreate" [~0] forall f g h. genericCreateZipRight f g (genericCreate h) = genericCreate $ \(Offset i) -> f (h (Offset i)) (g (Offset i))
"zipWith/mapVector left" [~0] forall f g a. Vector.zipWith f (mapVector g a) = Vector.zipWith (f . g) a
"zipWith/mapVector right" [~0] forall f g a b. Vector.zipWith f a (mapVector g b) = Vector.zipWith (\aa bb -> f aa (g bb)) a b
"mapVector/zipWith" [~0] forall f g a b. mapVector f (Vector.zipWith g a b) = Vector.zipWith (\aa bb -> f (g aa bb)) a b
  #-}