TypeUnary.Vec

Experiment in length-typed vectors

Type-level numbers

data Z

Type-level representation of zero

Instances

IsNat Z

data S n

Type-level representation of successor

Instances

IsNat n => IsNat (S n)

type family a :+: b

Sum of type-level numbers

type N0 = Z

type N1 = S N0

type N2 = S N1

type N3 = S N2

type N4 = S N3

type N5 = S N4

type N6 = S N5

type N7 = S N6

type N8 = S N7

type N9 = S N8

type N10 = S N9

type N11 = S N10

type N12 = S N11

type N13 = S N12

type N14 = S N13

type N15 = S N14

type N16 = S N15

Typed natural numbers

data Nat where

Constructors

Zero :: Nat Z

Succ :: IsNat n => Nat n -> Nat (S n)

Instances

Show (Nat n)

zero :: Nat N0

one :: Nat N1

two :: Nat N2

three :: Nat N3

four :: Nat N4

withIsNat :: (IsNat n => Nat n -> a) -> Nat n -> a

natSucc :: Nat n -> Nat (S n)

natIsNat :: Nat n -> IsNat n => Nat n

natToZ :: Nat n -> Integer

Interpret a Nat as an Integer

natEq :: Nat m -> Nat n -> Maybe (m :=: n)

Equality test

natAdd :: Nat m -> Nat n -> Nat (m :+: n)

Sum of naturals

data m :<: n

Proof that m < n

data Index lim

A number under the given limit, with proof

Constructors

forall n . IsNat n => Index (n :<: lim) (Nat n)

Instances

Eq (Index lim)

succI :: Index m -> Index (S m)

index0 :: Index (S m)

index1 :: Index (S (S m))

index2 :: Index (S (S (S m)))

index3 :: Index (S (S (S (S m))))

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

Functor (Vec n)

IsNat n => Applicative (Vec n)

Foldable (Vec n)

Traversable (Vec n)

Eq a => Eq (Vec n a)

Enumerate the elements of a vector. See also elemsV vElems :: Vec n a -> [a] vElems ZVec = [] vElems (a :< as) = a : vElems as

Ord a => Ord (Vec n a)

Show a => Show (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

class IsNat n where

n a vector length.

Methods

nat :: Nat n

pureV :: a -> Vec n a

elemsV :: [a] -> Vec n a

peekV :: Storable a => Ptr a -> IO (Vec n a)

pokeV :: Storable a => Ptr a -> Vec n a -> IO ()

Instances

IsNat Z

IsNat n => IsNat (S n)

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

Concatenation of vectors

indices :: Nat n -> Vec n (Index n)

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

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

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

get0 :: Vec (S n) a -> Vec1 a

get1 :: Vec (S (S n)) a -> Vec1 a

get2 :: Vec (S (S (S n))) a -> Vec1 a

get3 :: Vec (S (S (S (S n)))) a -> Vec1 a

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

General indexing, taking a proof that the index is within bounds.

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

class ToVec c n a | c -> n a where

Methods

toVec :: c -> Vec n a

Instances

ToVec (Vec n a) n a