diff --git a/src/Data/NumIdr/Homogeneous.idr b/src/Data/NumIdr/Homogeneous.idr index 724e666..ebde046 100644 --- a/src/Data/NumIdr/Homogeneous.idr +++ b/src/Data/NumIdr/Homogeneous.idr @@ -99,11 +99,11 @@ getTranslationVector mat with (viewShape mat) export -scalingH : Num a => {n : _} -> a -> HMatrix' n a +scalingH : {n : _} -> Num a => a -> HMatrix' n a scalingH x = indexSet [last,last] 1 $ repeatDiag x 0 export -translationH : Num a => {n : _} -> Vector n a -> HMatrix' n a +translationH : {n : _} -> Num a => Vector n a -> HMatrix' n a translationH = hmatrix identity export diff --git a/src/Data/NumIdr/Matrix.idr b/src/Data/NumIdr/Matrix.idr index 3a456c1..493e0cd 100644 --- a/src/Data/NumIdr/Matrix.idr +++ b/src/Data/NumIdr/Matrix.idr @@ -59,15 +59,9 @@ fromDiag ds o = fromFunction [m,n] (\[i,j] => maybe o (`index` ds) $ i `eq` j) eq (FS _) FZ = Nothing -||| The `n`-dimensional identity matrix. -export -identity : Num a => {n : _} -> Matrix' n a -identity = repeatDiag 1 0 - - ||| Construct the matrix that scales a vector by the given value. export -scaling : Num a => {n : _} -> a -> Matrix' n a +scaling : {n : _} -> Num a => a -> Matrix' n a scaling x = repeatDiag x 0 ||| Calculate the rotation matrix of an angle. @@ -157,5 +151,7 @@ Num a => Mult (Matrix m n a) (Matrix n p a) (Matrix m p a) where (\k => m1 !! [i,k] * m2 !! [k,j]) range) export -{n : _} -> Num a => MultNeutral (Matrix' n a) where - neutral = identity +{n : _} -> Num a => MultGroup (Matrix' n a) where + identity = repeatDiag 1 0 + + inverse = ?matrixInverse diff --git a/src/Data/NumIdr/Multiply.idr b/src/Data/NumIdr/Multiply.idr index 0485a1a..c7e0e46 100644 --- a/src/Data/NumIdr/Multiply.idr +++ b/src/Data/NumIdr/Multiply.idr @@ -16,32 +16,40 @@ public export interface Mult a b c | a,b where (*.) : a -> b -> c -||| An interface for monoids using the `*.` operator. +public export +Mult' : Type -> Type +Mult' a = Mult a a 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` public export -interface Mult a a a => MultNeutral a where - neutral : a +interface Mult' a => MultGroup a where + identity : a + inverse : a -> a ||| Multiplication forms a semigroup public export -[MultSemigroup] Mult a a a => Semigroup a where +[MultSemigroup] Mult' a => Semigroup a where (<+>) = (*.) -||| Multiplication with a neutral element forms a monoid +||| Multiplication with an identity element forms a monoid public export -[MultMonoid] MultNeutral a => Monoid a using MultSemigroup where - neutral = Multiply.neutral +[MultMonoid] MultGroup a => Monoid a using MultSemigroup where + neutral = identity ||| Raise a multiplicative value (e.g. a matrix or a transformation) to a natural ||| number power. public export -power : MultNeutral a => Nat -> a -> a -power 0 _ = neutral +power : MultGroup a => Nat -> a -> a +power 0 _ = identity power 1 x = x power (S n@(S _)) x = x *. power n x @@ -50,5 +58,5 @@ power (S n@(S _)) x = x *. power n x ||| ||| This is the operator form of `power`. public export -(^) : MultNeutral a => a -> Nat -> a +(^) : MultGroup a => a -> Nat -> a (^) = flip power