type-unary-0.2.8: Type-level and typed unary natural numbers, inequality proofs, vectors

Stability experimental conal@conal.net None

TypeUnary.Vec

Contents

Description

Experiment in length-typed vectors

Synopsis

# Vectors

data Vec whereSource

Vectors with type-determined length, having empty vector (`ZVec`) and vector cons ('(:<)').

Constructors

 ZVec :: Vec Z a :< :: a -> Vec n a -> Vec (S n) a

Instances

 IsNat n => Monad (Vec n) Functor (Vec n) IsNat n => Applicative (Vec n) Foldable (Vec n) Traversable (Vec n) (IsNat n, Enum applicative_arg) => Enum (Vec n applicative_arg) Eq a => Eq (Vec n a) (IsNat n, Floating applicative_arg) => Floating (Vec n applicative_arg) (IsNat n, Fractional applicative_arg) => Fractional (Vec n applicative_arg) (IsNat n, Integral applicative_arg) => Integral (Vec n applicative_arg) (IsNat n, Num applicative_arg) => Num (Vec n applicative_arg) Ord a => Ord (Vec n a) (IsNat n, Num applicative_arg, Ord applicative_arg) => Real (Vec n applicative_arg) (IsNat n, RealFloat applicative_arg) => RealFloat (Vec n applicative_arg) (IsNat n, RealFrac applicative_arg) => RealFrac (Vec n applicative_arg) Show a => Show (Vec n a) (IsNat n, Monoid a) => Monoid (Vec n a) (IsNat n, Storable a) => Storable (Vec n a) (IsNat n, Num a) => VectorSpace (Vec n a) (IsNat n, Num a) => InnerSpace (Vec n a) (IsNat n, Num a) => AdditiveGroup (Vec n a) ToVec (Vec n a) n a

unConsV :: Vec (S n) a -> (a, Vec n a)Source

Type-safe un-cons for vectors

headV :: Vec (S n) a -> aSource

tailV :: Vec (S n) a -> Vec n aSource

Type-safe tail for vectors

joinV :: Vec n (Vec n a) -> Vec n aSource

Equivalent to monad `join` for vectors

(<+>) :: Vec m a -> Vec n a -> Vec (m :+: n) aSource

Concatenation of vectors

indices :: IsNat n => Vec n (Index n)Source

Indices under `n`: `index0` :< `index1` :< ...

iota :: (IsNat n, Num a, Enum a) => Vec n aSource

Vector of ints from 0 to n-1. Named for APL iota operation (but 0 based).

vec1 :: a -> Vec1 aSource

vec2 :: a -> a -> Vec2 aSource

vec3 :: a -> a -> a -> Vec3 aSource

vec4 :: a -> a -> a -> a -> Vec4 aSource

vec5 :: a -> a -> a -> a -> a -> Vec5 aSource

vec6 :: a -> a -> a -> a -> a -> a -> Vec6 aSource

vec7 :: a -> a -> a -> a -> a -> a -> a -> Vec7 aSource

vec8 :: a -> a -> a -> a -> a -> a -> a -> a -> Vec8 aSource

un1 :: Vec1 a -> aSource

Extract element

un2 :: Vec2 a -> (a, a)Source

Extract elements

un3 :: Vec3 a -> (a, a, a)Source

Extract elements

un4 :: Vec4 a -> (a, a, a, a)Source

Extract elements

get :: Index n -> Vec n a -> aSource

Extract a vector element, taking a proof that the index is within bounds.

Arguments

 :: Vec (N1 :+: n) a -> a Get first element

Arguments

 :: Vec (N2 :+: n) a -> a Get second element

Arguments

 :: Vec (N3 :+: n) a -> a Get third element

Arguments

 :: Vec (N4 :+: n) a -> a Get fourth element

update :: Index n -> (a -> a) -> Vec n a -> Vec n aSource

Update a vector element, taking a proof that the index is within bounds.

set :: Index n -> a -> Vec n a -> Vec n aSource

Replace a vector element, taking a proof that the index is within bounds.

Arguments

 :: a -> Vec (N1 :+: n) a -> Vec (N1 :+: n) a Set first element

Arguments

 :: a -> Vec (N2 :+: n) a -> Vec (N2 :+: n) a Set second element

Arguments

 :: a -> Vec (N3 :+: n) a -> Vec (N3 :+: n) a Set third element

Arguments

 :: a -> Vec (N4 :+: n) a -> Vec (N4 :+: n) a Set fourth element

getI :: (IsNat n, Show i, Integral i) => i -> Vec n a -> aSource

Variant of `get` in which the index size is checked at run-time instead of compile-time.

setI :: (IsNat n, Show i, Integral i) => i -> a -> Vec n a -> Vec n aSource

Variant of `set` in which the index size is checked at run-time instead of compile-time.

flattenV :: IsNat n => Vec n (Vec m a) -> Vec (n :*: m) aSource

Flatten a vector of vectors (a 2D array) into a vector

chunkV :: (IsNat n, IsNat m) => Vec (n :*: m) a -> Vec n (Vec m a)Source

Chunk a vector into a vector of vectors (a 2D array)

swizzle :: Vec n (Index m) -> Vec m a -> Vec n aSource

Swizzling. Extract multiple elements simultaneously.

split :: IsNat n => Vec (n :+: m) a -> (Vec n a, Vec m a)Source

Split a vector

deleteV :: Eq a => a -> Vec (S n) a -> Vec n aSource

Delete exactly one occurrence of an element from a vector, raising an error if the element isn't present.

elemsV :: IsNat n => [a] -> Vec n aSource

Convert a list into a vector. Error if the list is too short or too long

zipV :: Vec n a -> Vec n b -> Vec n (a, b)Source

Zip two vectors into one. Like `liftA2 '(,)'`, but the former requires `IsNat n`.

zipWithV :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n cSource

Unzip one vector into two. Like `liftA2`, but the former requires `IsNat n`.

unzipV :: Vec n (a, b) -> (Vec n a, Vec n b)Source

Unzip a vector of pairs into a pair of vectors

zipV3 :: Vec n a -> Vec n b -> Vec n c -> Vec n (a, b, c)Source

Zip three vectors into one. Like `liftA3 '(,)'`, but the former requires `IsNat n`.

zipWithV3 :: (a -> b -> c -> d) -> Vec n a -> Vec n b -> Vec n c -> Vec n dSource

Unzip one vector into two. Like `liftA2`, but the former requires `IsNat n`.

unzipV3 :: Vec n (a, b, c) -> (Vec n a, Vec n b, Vec n c)Source

Unzip a vector of pairs into a pair of vectors

transpose :: IsNat n => Vec m (Vec n a) -> Vec n (Vec m a)Source

Matrix transposition. Specialization of `sequenceA`.

cross :: Vec m a -> Vec n b -> Vec m (Vec n (a, b))Source

Cross-product of two vectors, in the set-theory sense, not the geometric sense. You can `flattenV` the resulting vector of vectors.

class ToVec c n a whereSource

Methods

toVec :: c -> Vec n aSource

Instances

 IsNat n => ToVec [a] n a ToVec (Vec n a) n a