Separate MultMonoid interface from MultGroup

src/Data/NumIdr/Matrix.idr

@@ -140,18 +140,18 @@ export
 Num a => Mult (Matrix m n a) (Vector n a) (Vector m a) where
   mat *. v with (viewShape mat)
     _ | Shape [m,n] = fromFunction [m]
-      (\[i] => foldMap @{%search} @{Additive}
+      (\[i] => sum $ map (\j => mat!![i,j] * v!!j) range)
-        (\j => mat !! [i,j] * v !! j) range)
 
 export
 Num a => Mult (Matrix m n a) (Matrix n p a) (Matrix m p a) where
   m1 *. m2 with (viewShape m1, viewShape m2)
     _ | (Shape [m,n], Shape [n,p]) = fromFunction [m,p]
-      (\[i,j] => foldMap @{%search} @{Additive}
+      (\[i,j] => sum $ map (\k => m1!![i,k] * m2!![k,j]) range)
-        (\k => m1 !! [i,k] * m2 !! [k,j]) range)
 
 export
-{n : _} -> Num a => MultGroup (Matrix' n a) where
+{n : _} -> Num a => MultMonoid (Matrix' n a) where
   identity = repeatDiag 1 0
 
-  inverse = ?matrixInverse
+
+export
+{n : _} -> Neg a => Fractional a => MultGroup (Matrix' n a) where

src/Data/NumIdr/Multiply.idr

@@ -21,28 +21,36 @@ Mult' : Type -> Type
 Mult' a = Mult a a a
 
 
+||| An interface for monoids using the `*.` operator.
+|||
+||| An instance of this interface must satisfy:
+||| * `x *. identity == x`
+||| * `identity *. x == x`
+public export
+interface Mult' a => MultMonoid a where
+  identity : a
+
 ||| An interface for groups using the `*.` operator.
 |||
 ||| An instance of this interface must satisfy:
-||| * `x *. neutral == x`
+||| * `x *. inverse x == identity`
-||| * `neutral *. x == x`
+||| * `inverse x *. x == identity`
-||| * `x *. inverse x == neutral`
-||| * `inverse x *. x == neutral`
 public export
-interface Mult' a => MultGroup a where
+interface MultMonoid a => MultGroup a where
-  identity : a
   inverse : a -> a
 
 
-||| Multiplication forms a semigroup
+namespace Semigroup
-public export
+  ||| Multiplication forms a semigroup
-[MultSemigroup] Mult' a => Semigroup a where
+  public export
-  (<+>) = (*.)
+  [Mult] Mult' a => Semigroup a where
+    (<+>) = (*.)
 
-||| Multiplication with an identity element forms a monoid
+namespace Monoid
-public export
+  ||| Multiplication with an identity element forms a monoid
-[MultMonoid] MultGroup a => Monoid a using MultSemigroup where
+  public export
-  neutral = identity
+  [Mult] MultMonoid a => Monoid a using Semigroup.Mult where
+    neutral = identity
 
 
 ||| Raise a multiplicative value (e.g. a matrix or a transformation) to a natural