Data.NumIdr.Interfaces

Definitions

Field : Type -> Type

  An interface synonym for types which form a field, such as `Double`.

Totality: total
Visibility: public export

interface FieldCmp : Type -> Type

  An interface for number types which allow for LUP decomposition to be performed.
  
  The function `abslt` is required for the internal decomposition algorithm.
  An instance of this interface must satisfy:
  * The relation `abslt` is a preorder.
  * `0` is a minimum of `abslt`.

Parameters: a
Constraints: Eq a, Neg a, Fractional a
Constructor: 

MkFieldCmp

Methods:

abslt : a -> a -> Bool

  Compare the absolute values of two inputs.

Implementation: 

FieldCmp Double

abslt : FieldCmp a => a -> a -> Bool

  Compare the absolute values of two inputs.

Totality: total
Visibility: public export

WithEpsilon : (Neg a, (Abs a, Ord a)) => a -> Eq a

Totality: total
Visibility: export

WithEpsilon : (Neg a, (Fractional a, (Abs a, Ord a))) => a -> FieldCmp a

Totality: total
Visibility: export

interface Mult : Type -> Type -> Type -> Type

  A generalized multiplication/application operator. This interface is
  necessary since the standard multiplication operator is homogenous.
  
  All instances of this interface must collectively satisfy these axioms:
  * If `(x *. y) *. z` is defined, then `x *. (y *. z)` is defined and equal.
  * If `x *. (y *. z)` is defined, then `(x *. y) *. z` is defined and equal.

Parameters: a, b, c
Constructor: 

MkMult

Methods:

(*.) : a -> b -> c

  A generalized multiplication/application operator for matrices and
  vector transformations.

Fixity Declaration: infixl operator, level 9

Implementations:

Num a => Mult (Scalar a) (Scalar a) (Scalar a)

Num a => Mult a (Array s a) (Array s a)

Num a => Mult (Array s a) a (Array s a)

Num a => Mult (Matrix m n a) (Vector n a) (Vector m a)

Num a => Mult (Matrix m n a) (Matrix n p a) (Matrix m p a)

Num a => Mult (Matrix m n a) (Point n a) (Point m a)

Num a => Mult (Transform ty n a) (Point n a) (Point n a)

Num a => Mult (Transform ty n a) (Vector n a) (Vector n a)

Num a => Mult (Transform t1 n a) (Transform t2 n a) (Transform (transMult t1 t2) n a)

Mult (Permutation n) (Permutation n) (Permutation n)

(*.) : Mult a b c => a -> b -> c

  A generalized multiplication/application operator for matrices and
  vector transformations.

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 9

Mult' : Type -> Type

  A synonym for `Mult a a a`, or homogenous multiplication.

Totality: total
Visibility: public export

interface MultMonoid : Type -> Type

  An interface for monoids using the `*.` operator.
  
  An instance of this interface must satisfy:
  * `x *. identity == x`
  * `identity *. x == x`

Parameters: a
Constraints: Mult' a
Constructor: 

MkMultMonoid

Methods:

identity : a

  Construct an identity matrix or transformation.
  
  NOTE: Creating an identity element for an `n`-dimensional transformation
  usually requires `n` to be available at runtime.

Implementations:

Num a => MultMonoid (Scalar a)

Num a => MultMonoid (Matrix' n a)

Num a => MultMonoid (Transform ty n a)

MultMonoid (Permutation n)

identity : MultMonoid a => a

  Construct an identity matrix or transformation.
  
  NOTE: Creating an identity element for an `n`-dimensional transformation
  usually requires `n` to be available at runtime.

Totality: total
Visibility: public export

interface MultGroup : Type -> Type

  An interface for groups using the `*.` operator.
  
  An instance of this interface must satisfy:
  * `x *. inverse x == identity`
  * `inverse x *. x == identity`

Parameters: a
Constraints: MultMonoid a
Constructor: 

MkMultGroup

Methods:

inverse : a -> a

  Calculate the inverse of the matrix or transformation.
  
  WARNING: This function will not check if an inverse exists for the given
  input, and will happily divide by zero or return results containing NaN.
  To avoid this, use `tryInverse` instead.

Implementations:

Fractional a => MultGroup (Scalar a)

FieldCmp a => MultGroup (Matrix' n a)

FieldCmp a => MultGroup (Transform ty n a)

MultGroup (Permutation n)

inverse : MultGroup a => a -> a

  Calculate the inverse of the matrix or transformation.
  
  WARNING: This function will not check if an inverse exists for the given
  input, and will happily divide by zero or return results containing NaN.
  To avoid this, use `tryInverse` instead.

Totality: total
Visibility: public export

power : MultMonoid a => Nat -> a -> a

  Raise a multiplicative value (e.g. a matrix or a transformation) to a natural
  number power.

Totality: total
Visibility: public export

(^) : MultMonoid a => a -> Nat -> a

  Raise a multiplicative value (e.g. a matrix or a transformation) to a natural
  number power.
  
  This is the operator form of `power`.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 10