Data.Vector.Sized

Size-parameterized vector types and functions.

Documentation

data Vector a n where

Constructors

Nil :: Vector a Z

:- :: a -> Vector a n -> Vector a (S n)

Instances

Monomorphicable Nat (Vector a)

Eq a => Eq (Vector a n)

Show a => Show (Vector a n)

sLength :: Vector a n -> SNat n

length :: Vector a n -> Int

append :: Vector a n -> Vector a m -> Vector a (n :+: m)

foldr :: (a -> b -> b) -> b -> Vector a n -> b

foldl :: (a -> b -> a) -> a -> Vector b n -> a

singleton :: a -> Vector a (S Z)

zipWith :: (a -> b -> c) -> Vector a n -> Vector b m -> Vector c (Min n m)

zipWithSame :: (a -> b -> c) -> Vector a n -> Vector b n -> Vector c n

toList :: Vector a n -> [a]

fromList :: SNat n -> [a] -> Maybe (Vector a n)

unsafeFromList :: SNat n -> [a] -> Vector a n

fromList' :: SingRep n => [a] -> Maybe (Vector a n)

unsafeFromList' :: SingRep n => [a] -> Vector a n

all :: (a -> Bool) -> Vector a n -> Bool

splitAt :: (n :<<= m) ~ True => SNat n -> Vector a m -> (Vector a n, Vector a (m :-: n))

takeAtMost :: SNat n -> Vector a m -> Vector a (Min n m)

splitAtMost :: SNat n -> Vector a m -> (Vector a (Min n m), Vector a (m :-: n))

drop :: (n :<<= m) ~ True => SNat n -> Vector a m -> Vector a (m :-: n)

take :: (n :<<= m) ~ True => SNat n -> Vector a m -> Vector a n

map :: (a -> b) -> Vector a n -> Vector b n

head :: Vector a (S n) -> a

tail :: Vector a (S n) -> Vector a n

index :: (n :<<= m) ~ True => SNat n -> Vector a (S m) -> a