Data.Utils.Vector

This module defines fixed-length vectors and some basic typeclass instances and operations for them.

Documentation

data Vector :: Nat -> * -> *

Vector n a is the type of vectors of length n with elements of type a.

Instances

Functor (Vector n)

KnownNat n => Applicative (Vector n)

Foldable (Vector n)

Traversable (Vector n)

Eq a => Eq (Vector n a)

(KnownNat n, Read a) => Read (Vector n a)

Show a => Show (Vector n a)

NFData a => NFData (Vector n a)

(<%>) :: Num a => Vector n a -> Vector n a -> a

The scalar product of two vectors of the same length.

>>> :set -XDataKinds
>>> cons 1 (cons 2 nil) <%> cons 3 (cons 4 nil) :: Int
11

nil :: Vector 0 a

The vector of length zero.

cons :: forall a n. a -> Vector n a -> Vector (n + 1) a

Prepends the specified element to the specified vector.

>>> cons False (cons True nil)
[False,True]

generate :: forall n a. KnownNat n => (Int -> a) -> Vector n a

Generates a vector by applying the given function to each index.

>>> :set -XDataKinds
>>> generate id :: Vector 3 Int
[0,1,2]

(!?) :: Vector n a -> Int -> Maybe a

Gets the vector element at the specified index if the index is valid, otherwise Nothing.

>>> cons 'x' nil !? 0
Just 'x'

>>> cons 'x' nil !? 1
Nothing

(!) :: Vector n a -> Int -> a

Gets the vector element at the specified index, throws an exception if the index is invalid.

>>> cons 'x' nil ! 0
'x'

vhead :: 1 <= n => Vector n a -> a

Gets the first element of a vector of length greater than zero.

>>> vhead (cons 'x' (cons 'y' nil))
'x'

vtail :: forall a n. 1 <= n => Vector n a -> Vector (n - 1) a

For a vector of length greater than zero, gets the vector with its first element removed.

>>> vtail (cons 'x' (cons 'y' nil))
"y"

(<+>) :: (Num a, KnownNat n) => Vector n a -> Vector n a -> Vector n a infixl 6

Adds two vectors of the same length.

>>> :set -XDataKinds
>>> (cons 1 (cons 2 nil)) <+> (cons 3 (cons 4 nil)) :: Vector 2 Int
[4,6]

(<->) :: (Num a, KnownNat n) => Vector n a -> Vector n a -> Vector n a infixl 6

Subtracts two vectors of the same length.

>>> :set -XDataKinds
>>> (cons 1 (cons 2 nil)) <-> (cons 3 (cons 4 nil)) :: Vector 2 Int
[-2,-2]

sqNorm :: Num a => Vector n a -> a

Calculates the squared euclidean norm of a vector, i.e. the scalar product of the vector by itself.

>>> :set -XDataKinds
>>> sqNorm (cons 3 (cons 4 nil)) :: Int
25

sqDiff :: (Num a, KnownNat n) => Vector n a -> Vector n a -> a

Calculates the squared euclidean distance between two vectors of the same length.

>>> :set -XDataKinds
>>> sqDiff (cons 1 (cons 2 nil)) (cons 3 (cons 4 nil)) :: Int
8

class KnownNat n

This class gives the integer associated with a type-level natural. There are instances of the class for every concrete literal: 0, 1, 2, etc.

Since: 4.7.0.0

Minimal complete definition

natSing

natVal :: KnownNat n => proxy n -> Integer

Since: 4.7.0.0