TypeUnary.Vec

Experiment in length-typed vectors

Documentation

module TypeUnary.Nat

Vectors

data Vec where

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

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

Type-safe head for vectors

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

Type-safe tail for vectors

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

Equivalent to monad join for vectors

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

Concatenation of vectors

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

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

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

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

type Vec0 = Vec N0

type Vec1 = Vec N1

type Vec2 = Vec N2

type Vec3 = Vec N3

type Vec4 = Vec N4

type Vec5 = Vec N5

type Vec6 = Vec N6

type Vec7 = Vec N7

type Vec8 = Vec N8

type Vec9 = Vec N9

type Vec10 = Vec N10

type Vec11 = Vec N11

type Vec12 = Vec N12

type Vec13 = Vec N13

type Vec14 = Vec N14

type Vec15 = Vec N15

type Vec16 = Vec N16

vec1 :: a -> Vec1 a

vec2 :: a -> a -> Vec2 a

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

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

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

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

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

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

un1 :: Vec1 a -> a

Extract element

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

Extract elements

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

Extract elements

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

Extract elements

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

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

get0

Arguments

:: Vec (N1 :+: n) a

-> a

Get first element

get1

Arguments

:: Vec (N2 :+: n) a

-> a

Get second element

get2

Arguments

:: Vec (N3 :+: n) a

-> a

Get third element

get3

Arguments

:: Vec (N4 :+: n) a

-> a

Get fourth element

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

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

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

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

set0

Arguments

:: a

-> Vec (N1 :+: n) a

-> Vec (N1 :+: n) a

Set first element

set1

Arguments

:: a

-> Vec (N2 :+: n) a

-> Vec (N2 :+: n) a

Set second element

set2

Arguments

:: a

-> Vec (N3 :+: n) a

-> Vec (N3 :+: n) a

Set third element

set3

Arguments

:: a

-> Vec (N4 :+: n) a

-> Vec (N4 :+: n) a

Set fourth element

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

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 a

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) a

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

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

Swizzling. Extract multiple elements simultaneously.

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

Split a vector

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

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 a

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)

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 c

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

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

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)

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 d

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)

Unzip a vector of pairs into a pair of vectors

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

Matrix transposition. Specialization of sequenceA.

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

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 where

Methods

toVec :: c -> Vec n a

Instances

IsNat n => ToVec [a] n a

ToVec (Vec n a) n a