From 95a13ffd91e749df9c9768c5536390a274c6721b Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Thu, 4 Aug 2022 15:18:12 -0400
Subject: [PATCH] Separate MultMonoid interface from MultGroup

---
 src/Data/NumIdr/Matrix.idr   | 12 ++++++------
 src/Data/NumIdr/Multiply.idr | 36 ++++++++++++++++++++++--------------
 2 files changed, 28 insertions(+), 20 deletions(-)

diff --git a/src/Data/NumIdr/Matrix.idr b/src/Data/NumIdr/Matrix.idr
index 1e5f582..1c933de 100644
--- a/src/Data/NumIdr/Matrix.idr
+++ b/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}
-        (\j => mat !! [i,j] * v !! j) range)
+      (\[i] => sum $ map (\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}
-        (\k => m1 !! [i,k] * m2 !! [k,j]) range)
+      (\[i,j] => sum $ map (\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
diff --git a/src/Data/NumIdr/Multiply.idr b/src/Data/NumIdr/Multiply.idr
index c7e0e46..a9ee327 100644
--- a/src/Data/NumIdr/Multiply.idr
+++ b/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`
-||| * `neutral *. x == x`
-||| * `x *. inverse x == neutral`
-||| * `inverse x *. x == neutral`
+||| * `x *. inverse x == identity`
+||| * `inverse x *. x == identity`
 public export
-interface Mult' a => MultGroup a where
-  identity : a
+interface MultMonoid a => MultGroup a where
   inverse : a -> a
 
 
-||| Multiplication forms a semigroup
-public export
-[MultSemigroup] Mult' a => Semigroup a where
-  (<+>) = (*.)
+namespace Semigroup
+  ||| Multiplication forms a semigroup
+  public export
+  [Mult] Mult' a => Semigroup a where
+    (<+>) = (*.)
 
-||| Multiplication with an identity element forms a monoid
-public export
-[MultMonoid] MultGroup a => Monoid a using MultSemigroup where
-  neutral = identity
+namespace Monoid
+  ||| Multiplication with an identity element forms a monoid
+  public export
+  [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