Vector, i.e. length-indexed list.

Empty Vec.

Vec with exactly one element.

>>> singleton True
True ::: VNil

Convert to pull Vec.

Convert from pull Vec.

Convert Vec to list.

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

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

Since: 0.4

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

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

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

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

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

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

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

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

Reify any list [a] to Vec n a.

>>> reifyList "foo" length
3

Indexing.

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

Tabulating, inverse of !.

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

Cons an element in front of a Vec.

Add a single element at the end of a Vec.

The first element of a Vec.

The last element of a Vec.

Since: 0.4

The elements after the head of a Vec.

The elements before the last of a Vec.

Since: 0.4

Reverse Vec.

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

Since: 0.2.1

Append two Vec.

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

Split vector into two parts. Inverse of ++.

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

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

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

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

concatMap id

Inverse of concat.

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

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

See Foldable.

See Foldable1.

See FoldableWithIndex.

There is no type-class for this :(

Right fold.

Right fold with an index.

Yield the length of a Vec. O(n)

Test whether a Vec is empty. O(1)

Non-strict sum.

Non-strict product.

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

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

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

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

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

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

Zip two Vecs with a function.

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

Repeat value

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

Since: 0.2.1

Monadic bind.

Monadic join.

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

Get all Fin n in a Vec n.

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

Ensure spine.

If we have an undefined Vec,

>>> let v = error "err" :: Vec N.Nat3 Char

And insert data into it later:

>>> let setHead :: a -> Vec ('S n) a -> Vec ('S n) a; setHead x (_ ::: xs) = x ::: xs

Then without a spine, it will fail:

>>> head $ setHead 'x' v
*** Exception: err
...

But with the spine, it won't:

>>> head $ setHead 'x' $ ensureSpine v
'x'