0 | module Data.NumIdr.Interfaces
  1 |
  2 | %default total
  3 |
  4 |
  5 | --------------------------------------------------------------------------------
  6 | -- Field
  7 | --------------------------------------------------------------------------------
  8 |
  9 |
 10 | ||| An interface synonym for types which form a field, such as `Double`.
 11 | public export
 12 | Field : Type -> Type
 13 | Field a = (Eq a, Neg a, Fractional a)
 14 |
 15 |
 16 | ||| An interface for number types which allow for LUP decomposition to be performed.
 17 | |||
 18 | ||| The function `abslt` is required for the internal decomposition algorithm.
 19 | ||| An instance of this interface must satisfy:
 20 | ||| * The relation `abslt` is a preorder.
 21 | ||| * `0` is a minimum of `abslt`.
 22 | public export
 23 | interface (Eq a, Neg a, Fractional a) => FieldCmp a where
 24 |   constructor MkFieldCmp
 25 |   ||| Compare the absolute values of two inputs.
 26 |   abslt : a -> a -> Bool
 27 |
 28 |
 29 | export
 30 | FieldCmp Double where
 31 |   abslt = (<) `on` abs
 32 |
 33 | -- Alternative implementations of `Eq` and `FieldCmp` that compare approximately,
 34 | -- useful when working with flating point numbers
 35 | namespace Eq
 36 |   export
 37 |   WithEpsilon : (Neg a, Abs a, Ord a) => a -> Eq a
 38 |   WithEpsilon ep = MkEq (\x,y => abs (x - y) < ep) (\x,y => abs (x - y) >= ep)
 39 |
 40 | namespace FieldCmp
 41 |   export
 42 |   WithEpsilon : (Neg a, Fractional a, Abs a, Ord a) => a -> FieldCmp a
 43 |   WithEpsilon ep = MkFieldCmp @{WithEpsilon ep} ((<) `on` abs)
 44 |
 45 | --------------------------------------------------------------------------------
 46 | -- Multiplication
 47 | --------------------------------------------------------------------------------
 48 |
 49 | infixl 9 *.
 50 | infixr 10 ^
 51 |
 52 | ||| A generalized multiplication/application operator. This interface is
 53 | ||| necessary since the standard multiplication operator is homogenous.
 54 | |||
 55 | ||| All instances of this interface must collectively satisfy these axioms:
 56 | ||| * If `(x *. y) *. z` is defined, then `x *. (y *. z)` is defined and equal.
 57 | ||| * If `x *. (y *. z)` is defined, then `(x *. y) *. z` is defined and equal.
 58 | public export
 59 | interface Mult a b c | a,b where
 60 |   constructor MkMult
 61 |   ||| A generalized multiplication/application operator for matrices and
 62 |   ||| vector transformations.
 63 |   (*.) : a -> b -> c
 64 |
 65 | ||| A synonym for `Mult a a a`, or homogenous multiplication.
 66 | public export
 67 | Mult' : Type -> Type
 68 | Mult' a = Mult a a a
 69 |
 70 |
 71 | ||| An interface for monoids using the `*.` operator.
 72 | |||
 73 | ||| An instance of this interface must satisfy:
 74 | ||| * `x *. identity == x`
 75 | ||| * `identity *. x == x`
 76 | public export
 77 | interface Mult' a => MultMonoid a where
 78 |   constructor MkMultMonoid
 79 |   ||| Construct an identity matrix or transformation.
 80 |   |||
 81 |   ||| NOTE: Creating an identity element for an `n`-dimensional transformation
 82 |   ||| usually requires `n` to be available at runtime.
 83 |   identity : a
 84 |
 85 | ||| An interface for groups using the `*.` operator.
 86 | |||
 87 | ||| An instance of this interface must satisfy:
 88 | ||| * `x *. inverse x == identity`
 89 | ||| * `inverse x *. x == identity`
 90 | public export
 91 | interface MultMonoid a => MultGroup a where
 92 |   constructor MkMultGroup
 93 |   ||| Calculate the inverse of the matrix or transformation.
 94 |   |||
 95 |   ||| WARNING: This function will not check if an inverse exists for the given
 96 |   ||| input, and will happily divide by zero or return results containing NaN.
 97 |   ||| To avoid this, use `tryInverse` instead.
 98 |   inverse : a -> a
 99 |
100 |
101 | namespace Semigroup
102 |   ||| Multiplication forms a semigroup
103 |   public export
104 |   [Mult] Mult' a => Semigroup a where
105 |     (<+>) = (*.)
106 |
107 | namespace Monoid
108 |   ||| Multiplication with an identity element forms a monoid
109 |   public export
110 |   [Mult] MultMonoid a => Monoid a using Semigroup.Mult where
111 |     neutral = identity
112 |
113 |
114 | ||| Raise a multiplicative value (e.g. a matrix or a transformation) to a natural
115 | ||| number power.
116 | public export
117 | power : MultMonoid a => Nat -> a -> a
118 | power 0 _ = identity
119 | power 1 x = x
120 | power (S n@(S _)) x = x *. power n x
121 |
122 | ||| Raise a multiplicative value (e.g. a matrix or a transformation) to a natural
123 | ||| number power.
124 | |||
125 | ||| This is the operator form of `power`.
126 | public export %inline
127 | (^) : MultMonoid a => a -> Nat -> a
128 | a ^ n = power n a
129 |