Vector, i.e. length-indexed list.

Empty Vec.

Vec with exactly one element.

>>> singleton True
True ::: VNil

O(n). Recover InlineInduction (and SNatI) dictionary from a Vec value.

Example: reflect is constrained with SNatI n, but if we have a Vec n a, we can recover that dictionary:

>>> let f :: forall n a. Vec n a -> N.Nat; f v = withDict v (N.reflect (Proxy :: Proxy n)) in f (True ::: VNil)
1

Note: using InlineInduction will be suboptimal, as if GHC has no opportunity to optimise the code, the recusion won't be unfold. How bad such code will perform? I don't know, we'll need benchmarks.

Convert to pull Vec.

Convert from pull Vec.

An Iso from toPull and fromPull.

Convert Vec to list.

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

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

Prism from list.

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

>>> "foo" ^? _Vec :: Maybe (Vec N.Nat2 Char)
Nothing

>>> _Vec # (True ::: False ::: VNil)
[True,False]

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'

Index lens.

>>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. ix (FS FZ)
'b'

>>> ('a' ::: 'b' ::: 'c' ::: VNil) & ix (FS FZ) .~ 'x'
'a' ::: 'x' ::: 'c' ::: VNil

Match on non-empty Vec.

Note: lens _Cons is a Prism. In fact, Vec n a cannot have an instance of Cons as types don't match.

Head lens. Note: lens _head is a Traversal'.

>>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. _head
'a'

>>> ('a' ::: 'b' ::: 'c' ::: VNil) & _head .~ 'x'
'x' ::: 'b' ::: 'c' ::: VNil

Head lens. Note: lens _head is a Traversal'.

Cons an element in front of a Vec.

The first element of a Vec.

The elements after the head of a Vec.

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.

Strict left fold.

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.

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

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.