Data.Vec.Lazy.Inline · vec-0.5.1

datadata Vec (n :: Nat) a where

#

Vector, i.e. length-indexed list.

Constructors

VNil :: Vec 'Z a
(:::) :: a -> Vec n1 a -> Vec ('S n1) ainfixr 5

Instances30Monad, Functor, Applicative, Foldable, Traversable, Foldable1, …

SNatI n => Monad (Vec n)Defined in vec-0.5.1 · Data.Vec.Lazy
Functor (Vec n)Defined in vec-0.5.1 · Data.Vec.Lazy
SNatI n => Applicative (Vec n)Defined in vec-0.5.1 · Data.Vec.Lazy
Foldable (Vec n)Defined in vec-0.5.1 · Data.Vec.Lazy
Traversable (Vec n)Defined in vec-0.5.1 · Data.Vec.Lazy
n ~ 'S m => Foldable1 (Vec n)Defined in vec-0.5.1 · Data.Vec.Lazy
Eq1 (Vec n)Defined in vec-0.5.1 · Data.Vec.Lazy
Ord1 (Vec n)Defined in vec-0.5.1 · Data.Vec.Lazy
Show1 (Vec n)Defined in vec-0.5.1 · Data.Vec.Lazy
SNatI n => Arbitrary1 (Vec n)Defined in vec-0.5.1 · Data.Vec.Lazy
SNatI n => Distributive (Vec n)Defined in vec-0.5.1 · Data.Vec.Lazy
Apply (Vec n)Defined in vec-0.5.1 · Data.Vec.Lazy
Bind (Vec n)Defined in vec-0.5.1 · Data.Vec.Lazy
n ~ 'S m => Traversable1 (Vec n)Defined in vec-0.5.1 · Data.Vec.Lazy
SNatI n => Representable (Vec n)Defined in vec-0.5.1 · Data.Vec.Lazy
FoldableWithIndex (Fin n) (Vec n)Defined in vec-0.5.1 · Data.Vec.Lazy
FunctorWithIndex (Fin n) (Vec n)Defined in vec-0.5.1 · Data.Vec.Lazy
TraversableWithIndex (Fin n) (Vec n)Defined in vec-0.5.1 · Data.Vec.Lazy
Eq a => Eq (Vec n a)Defined in vec-0.5.1 · Data.Vec.Lazy
Ord a => Ord (Vec n a)Defined in vec-0.5.1 · Data.Vec.Lazy
Show a => Show (Vec n a)Defined in vec-0.5.1 · Data.Vec.Lazy
Semigroup a => Semigroup (Vec n a)Defined in vec-0.5.1 · Data.Vec.Lazy
(Monoid a, SNatI n) => Monoid (Vec n a)Defined in vec-0.5.1 · Data.Vec.Lazy
NFData a => NFData (Vec n a)Defined in vec-0.5.1 · Data.Vec.Lazy
(SNatI n, Arbitrary a) => Arbitrary (Vec n a)Defined in vec-0.5.1 · Data.Vec.Lazy
(SNatI n, CoArbitrary a) => CoArbitrary (Vec n a)Defined in vec-0.5.1 · Data.Vec.Lazy
(SNatI n, Function a) => Function (Vec n a)Defined in vec-0.5.1 · Data.Vec.Lazy
Hashable a => Hashable (Vec n a)Defined in vec-0.5.1 · Data.Vec.Lazy
n ~ 'Z => Boring (Vec n a)Defined in vec-0.5.1 · Data.Vec.Lazy
type Rep (Vec n) = Fin nDefined in vec-0.5.1 · Data.Vec.Lazy

Construction

2 declarations

valueempty :: Vec 'Z a

#

Empty Vec.

valuesingleton :: a -> Vec ('S 'Z) a

#

Vec with exactly one element.

Example1 expression

>>> singleton TrueTrue ::: VNil

Conversions

7 declarations

valuetoPull :: SNatI n => Vec n a -> Vec n a

#

Convert to pull Vec.

valuefromPull :: SNatI n => Vec n a -> Vec n a

#

Convert from pull Vec.

valuetoList :: SNatI n => Vec n a -> [a]

#

Convert Vec to list.

Example1 expression

>>> toList $ 'f' ::: 'o' ::: 'o' ::: VNil"foo"

valuetoNonEmpty :: SNatI n => Vec ('S n) a -> NonEmpty a

#

Example1 expression

>>> toNonEmpty $ 1 ::: 2 ::: 3 ::: VNil1 :| [2,3]

valuefromList :: SNatI n => [a] -> Maybe (Vec n a)

#

Convert list [a] to Vec n a. Returns Nothing if lengths don't match exactly.

Example1 expression

>>> fromList "foo" :: Maybe (Vec N.Nat3 Char)Just ('f' ::: 'o' ::: 'o' ::: VNil)

Example1 expression

>>> fromList "quux" :: Maybe (Vec N.Nat3 Char)Nothing

Example1 expression

>>> fromList "xy" :: Maybe (Vec N.Nat3 Char)Nothing

valuefromListPrefix :: SNatI n => [a] -> Maybe (Vec n a)

#

Convert list [a] to Vec n a. Returns Nothing if input list is too short.

Example1 expression

>>> fromListPrefix "foo" :: Maybe (Vec N.Nat3 Char)Just ('f' ::: 'o' ::: 'o' ::: VNil)

Example1 expression

>>> fromListPrefix "quux" :: Maybe (Vec N.Nat3 Char)Just ('q' ::: 'u' ::: 'u' ::: VNil)

Example1 expression

>>> fromListPrefix "xy" :: Maybe (Vec N.Nat3 Char)Nothing

valuereifyList :: [a] -> (forall (n :: Nat). SNatI n => Vec n a -> r) -> r

#

Reify any list [a] to Vec n a.

Example1 expression

>>> reifyList "foo" length3

Indexing

8 declarations

value(!) :: SNatI n => Vec n a -> Fin n -> a

#

Indexing.

Example1 expression

>>> ('a' ::: 'b' ::: 'c' ::: VNil) ! FS FZ'b'

valuetabulate :: SNatI n => (Fin n -> a) -> Vec n a

#

Tabulating, inverse of !.

Example1 expression

>>> tabulate id :: Vec N.Nat3 (Fin N.Nat3)0 ::: 1 ::: 2 ::: VNil

valuecons :: a -> Vec n a -> Vec ('S n) a

#

Cons an element in front of a Vec.

valuesnoc :: SNatI n => Vec n a -> a -> Vec ('S n) a

#

Add a single element at the end of a Vec.

valuehead :: Vec ('S n) a -> a

#

The first element of a Vec.

valuelast :: SNatI n => Vec ('S n) a -> a

#

The last element of a Vec.

valuetail :: Vec ('S n) a -> Vec n a

#

The elements after the head of a Vec.

valueinit :: SNatI n => Vec ('S n) a -> Vec n a

#

The elements before the last of a Vec.

Concatenation and splitting

5 declarations

value(++) :: SNatI n => Vec n a -> Vec m a -> Vec (Plus n m) a

#

Append two Vec.

Example1 expression

>>> ('a' ::: 'b' ::: VNil) ++ ('c' ::: 'd' ::: VNil)'a' ::: 'b' ::: 'c' ::: 'd' ::: VNil

valuesplit :: SNatI n => Vec (Plus n m) a -> (Vec n a, Vec m a)

#

Split vector into two parts. Inverse of ++.

Example1 expression

>>> split ('a' ::: 'b' ::: 'c' ::: VNil) :: (Vec N.Nat1 Char, Vec N.Nat2 Char)('a' ::: VNil,'b' ::: 'c' ::: VNil)

Example1 expression

>>> uncurry (++) (split ('a' ::: 'b' ::: 'c' ::: VNil) :: (Vec N.Nat1 Char, Vec N.Nat2 Char))'a' ::: 'b' ::: 'c' ::: VNil

valueconcatMap

:: (SNatI m, SNatI n)
=> a -> Vec m b
-> Vec n a
-> Vec (Mult n m) b

#

Map over all the elements of a Vec and concatenate the resulting Vecs.

Example1 expression

>>> concatMap (\x -> x ::: x ::: VNil) ('a' ::: 'b' ::: VNil)'a' ::: 'a' ::: 'b' ::: 'b' ::: VNil

valueconcat :: (SNatI m, SNatI n) => Vec n (Vec m a) -> Vec (Mult n m) a

#

concatMap id

valuechunks :: (SNatI n, SNatI m) => Vec (Mult n m) a -> Vec n (Vec m a)

#

Inverse of concat.

Example1 expression

>>> chunks <$> fromListPrefix [1..] :: Maybe (Vec N.Nat2 (Vec N.Nat3 Int))Just ((1 ::: 2 ::: 3 ::: VNil) ::: (4 ::: 5 ::: 6 ::: VNil) ::: VNil)

Example2 expressions

>>> let idVec x = x :: Vec N.Nat2 (Vec N.Nat3 Int)>>> concat . idVec . chunks <$> fromListPrefix [1..]Just (1 ::: 2 ::: 3 ::: 4 ::: 5 ::: 6 ::: VNil)

Reverse

1 declaration

valuereverse :: SNatI n => Vec n a -> Vec n a

#

Reverse Vec.

Example1 expression

>>> reverse ('a' ::: 'b' ::: 'c' ::: VNil)'c' ::: 'b' ::: 'a' ::: VNil

Folds

6 declarations

valuefoldMap :: (Monoid m, SNatI n) => (a -> m) -> Vec n a -> m

#

See I.Foldable.

valuefoldMap1 :: (Semigroup s, SNatI n) => (a -> s) -> Vec ('S n) a -> s

#

See I.Foldable1.

valueifoldMap :: (Monoid m, SNatI n) => (Fin n -> a -> m) -> Vec n a -> m

#

See I.FoldableWithIndex.

valueifoldMap1

:: (Semigroup s, SNatI n)
=> Fin ('S n) -> a -> s
-> Vec ('S n) a
-> s

#

There is no type-class for this :(

valuefoldr :: SNatI n => (a -> b -> b) -> b -> Vec n a -> b

#

Right fold.

valueifoldr :: SNatI n => (Fin n -> a -> b -> b) -> b -> Vec n a -> b

#

Right fold with an index.

Special folds

4 declarations

valuelength :: SNatI n => Vec n a -> Int

#

Yield the length of a Vec. O(n)

valuenull :: Vec n a -> Bool

#

Test whether a Vec is empty. O(1)

valuesum :: (Num a, SNatI n) => Vec n a -> a

#

Non-strict sum.

valueproduct :: (Num a, SNatI n) => Vec n a -> a

#

Non-strict product.

Mapping

6 declarations

valuemap :: SNatI n => (a -> b) -> Vec n a -> Vec n b

#

Example1 expression

>>> map not $ True ::: False ::: VNilFalse ::: True ::: VNil

valueimap :: SNatI n => (Fin n -> a -> b) -> Vec n a -> Vec n b

#

Example1 expression

>>> imap (,) $ 'a' ::: 'b' ::: 'c' ::: VNil(0,'a') ::: (1,'b') ::: (2,'c') ::: VNil

valuetraverse :: (Applicative f, SNatI n) => (a -> f b) -> Vec n a -> f (Vec n b)

#

Apply an action to every element of a Vec, yielding a Vec of results.

valuetraverse1

:: (Apply f, SNatI n)
=> a -> f b
-> Vec ('S n) a
-> f (Vec ('S n) b)

#

Apply an action to non-empty Vec, yielding a Vec of results.

valueitraverse

:: (Applicative f, SNatI n)
=> Fin n -> a -> f b
-> Vec n a
-> f (Vec n b)

#

Apply an action to every element of a Vec and its index, yielding a Vec of results.

valueitraverse_

:: (Applicative f, SNatI n)
=> Fin n -> a -> f b
-> Vec n a
-> f ()

#

Apply an action to every element of a Vec and its index, ignoring the results.

Zipping

3 declarations

valuezipWith :: SNatI n => (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c

#

Zip two Vecs with a function.

valueizipWith

:: SNatI n
=> Fin n -> a -> b -> c
-> Vec n a
-> Vec n b
-> Vec n c

#

Zip two Vecs. with a function that also takes the elements' indices.

valuerepeat :: SNatI n => x -> Vec n x

#

Repeat value

Example1 expression

>>> repeat 'x' :: Vec N.Nat3 Char'x' ::: 'x' ::: 'x' ::: VNil

Monadic

2 declarations

valuebind :: SNatI n => Vec n a -> (a -> Vec n b) -> Vec n b

#

Monadic bind.

valuejoin :: SNatI n => Vec n (Vec n a) -> Vec n a

#

Monadic join.

Example1 expression

>>> join $ ('a' ::: 'b' ::: VNil) ::: ('c' ::: 'd' ::: VNil) ::: VNil'a' ::: 'd' ::: VNil

Universe

1 declaration

valueuniverse :: SNatI n => Vec n (Fin n)

#

Get all Fin n in a Vec n.

Example1 expression

>>> universe :: Vec N.Nat3 (Fin N.Nat3)0 ::: 1 ::: 2 ::: VNil

VecEach

1 declaration

classclass VecEach s t a b | s -> a, t -> b, s b -> t, t a -> s where

#

Write functions on Vec. Use them with tuples.

VecEach can be used to avoid "this function won't change the length of the list" in DSLs.

bad: Instead of

[x, y] <- badDslMagic ["foo", "bar"]  -- list!

good: we can write

(x, y) <- betterDslMagic ("foo", "bar") -- homogenic tuple!

where betterDslMagic can be defined using traverseWithVec.

Moreally lens Each should be a superclass, but there's no strict need for it.

Methods

mapWithVec :: (forall (n :: Nat). SNatI n => Vec n a -> Vec n b) -> s -> t
traverseWithVec :: Applicative f => (forall (n :: Nat). SNatI n => Vec n a -> f (Vec n b)) -> s -> f t

Instances3VecEach

(a ~ a', b ~ b') => VecEach (a, a') (b, b') a bDefined in vec-0.5.1 · Data.Vec.Lazy
(a ~ a2, a ~ a3, b ~ b2, b ~ b3) => VecEach (a, a2, a3) (b, b2, b3) a bDefined in vec-0.5.1 · Data.Vec.Lazy
(a ~ a2, a ~ a3, a ~ a4, b ~ b2, b ~ b3, b ~ b4) => VecEach (a, a2, a3, a4) (b, b2, b3, b4) a bDefined in vec-0.5.1 · Data.Vec.Lazy