{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE TypeApplications #-} module Noether.Algebra.Vector.Generic where import qualified Data.Vector.Generic as G import Noether.Lemmata.TypeFu import qualified Prelude as P import Noether.Algebra.Actions import Noether.Algebra.Multiple import Noether.Algebra.Single gBinaryOpK :: forall v a s op z. (MagmaK op a s, G.Vector v a, Coercible v z) => Proxy op -> z a -> z a -> z a gBinaryOpK o x y = coerce (G.zipWith binop (coerce x :: v a) (coerce y :: v a)) where binop = binaryOpK o (Proxy @s) gCancelK :: forall v a s op z. (CancellativeK op a s, G.Vector v a, Coercible v z) => Proxy op -> z a -> z a gCancelK o x = coerce (G.map cancelK' (coerce x :: v a)) where cancelK' = cancelK o (Proxy @s) gActK :: forall v a b s lr op z. (ActsK lr op a b s, G.Vector v b, Coercible v z) => Proxy op -> a -> z b -> z b gActK o a x = coerce (G.map (actK' a) (coerce x :: v b)) where actK' = actK o (Proxy @s) (Proxy @lr) gNeutralK :: forall n v a s op b. (NeutralK op a s, KnownNat n, G.Vector v a, Coercible v (b n)) => Proxy op -> b n a gNeutralK o = coerce (G.replicate count neutralValue :: v a) where count = P.fromIntegral (natVal (Proxy @n)) neutralValue = neutralK o (Proxy @s)