Data.Vec.Pull · vec-0.5.1 · horizon-platform

newtypenewtype Vec (n :: Nat) a

Easily fuseable Vec.

It on purpose doesn't have bad (fusion-wise) instances, like Traversable. Generally, there aren't functions which would be bad consumers or bad producers.

Constructors

Vec
- unVec :: Fin n -> a

Instances16Monad, Functor, Applicative, Foldable, Foldable1, Distributive, …

Monad (Vec n)Defined in vec-0.5.1 · Data.Vec.Pull
Functor (Vec n)Defined in vec-0.5.1 · Data.Vec.Pull
Applicative (Vec n)Defined in vec-0.5.1 · Data.Vec.Pull
SNatI n => Foldable (Vec n)Defined in vec-0.5.1 · Data.Vec.Pull
(SNatI m, n ~ 'S m) => Foldable1 (Vec n)Defined in vec-0.5.1 · Data.Vec.Pull
Distributive (Vec n)Defined in vec-0.5.1 · Data.Vec.Pull
Apply (Vec n)Defined in vec-0.5.1 · Data.Vec.Pull
Bind (Vec n)Defined in vec-0.5.1 · Data.Vec.Pull
Representable (Vec n)Defined in vec-0.5.1 · Data.Vec.Pull
SNatI n => FoldableWithIndex (Fin n) (Vec n)Defined in vec-0.5.1 · Data.Vec.Pull
FunctorWithIndex (Fin n) (Vec n)Defined in vec-0.5.1 · Data.Vec.Pull
(Eq a, SNatI n) => Eq (Vec n a)Defined in vec-0.5.1 · Data.Vec.Pull
Semigroup a => Semigroup (Vec n a)Defined in vec-0.5.1 · Data.Vec.Pull
Monoid a => Monoid (Vec n a)Defined in vec-0.5.1 · Data.Vec.Pull
n ~ 'Z => Boring (Vec n a)Defined in vec-0.5.1 · Data.Vec.Pull
type Rep (Vec n) = Fin nDefined in vec-0.5.1 · Data.Vec.Pull

Construction

2 declarations

valueempty :: Vec 'Z a

#

Empty Vec.

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

#

Vec with exactly one element.

Example1 expression

>>> L.fromPull $ singleton TrueTrue ::: VNil

Conversions

5 declarations

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

#

Convert Vec to list.

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

#

Convert Vec to NonEmpty.

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

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

Example1 expression

>>> L.fromPull <$> fromList "quux" :: Maybe (L.Vec N.Nat3 Char)Nothing

Example1 expression

>>> L.fromPull <$> fromList "xy" :: Maybe (L.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

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

Example1 expression

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

Example1 expression

>>> L.fromPull <$> fromListPrefix "xy" :: Maybe (L.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(!) :: Vec n a -> Fin n -> a

#

Indexing.

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

#

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.

Reverse

1 declaration

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

#

Reverse Vec.

Folds

7 declarations

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

#

See Foldable.

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

#

See 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.

valuefoldl' :: SNatI n => (b -> a -> b) -> b -> Vec n a -> b

#

Strict left fold.

Special folds

4 declarations

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

#

Yield the length of a Vec.

valuenull :: SNatI n => Vec n a -> Bool

#

Test whether a Vec is empty.

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

#

Strict sum.

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

#

Strict product.

Mapping

2 declarations

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

#

Example1 expression

>>> L.fromPull $ map not $ L.toPull $ True L.::: False L.::: L.VNilFalse ::: True ::: VNil

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

#

Example1 expression

>>> L.fromPull $ imap (,) $ L.toPull $ 'a' L.::: 'b' L.::: 'c' L.::: L.VNil(0,'a') ::: (1,'b') ::: (2,'c') ::: VNil

Zipping

3 declarations

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

#

Zip two Vecs with a function.

valueizipWith :: (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 :: x -> Vec n x

#

Repeat value

Monadic

2 declarations

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

#

Monadic bind.

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

#

Monadic join.

Universe

1 declaration

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

#

Get all Fin n in a Vec n.

Example1 expression

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