Modulevec-0.5.1.1Haskell2010

Data.Vec.Pull

Pull/representable Vec n a = Fin n -> a.

The module tries to have same API as Data.Vec.Lazy, missing bits: withDict, toPull, fromPull, traverse (and variants), (++), concat and split.

Contents

Construction
Conversions
Indexing
Reverse
Folds
Special folds
Mapping
Zipping
Monadic
Universe

Synopsis

newtype Vec
value empty
value singleton
value toList
value toNonEmpty
value fromList
value fromListPrefix
value reifyList
value !
value tabulate
value cons
value snoc
value head
value last
value tail
value init
value reverse
value foldMap
value foldMap1
value ifoldMap
value ifoldMap1
value foldr
value ifoldr
value foldl'
value length
value null
value sum
value product
value map
value imap
value zipWith
value izipWith
value repeat
value bind
value join
value universe

Packagevec-0.5.1.1
Exports36
LanguageHaskell2010
LicenceBSD-3-Clause
SourcePull.hs

newtypenewtype Vec (n :: Nat) a

Source#

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

Construction

valueempty :: Vec 'Z a

Source#

Empty Vec.

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

Source#

Vec with exactly one element.

Example1 expression

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

Conversions

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

Source#

Convert Vec to list.

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

Source#

Convert Vec to NonEmpty.

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

Source#

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)

Source#

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

Source#

Reify any list [a] to Vec n a.

Example1 expression

>>> reifyList "foo" length3

Indexing

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

Source#

Indexing.

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

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

Source#

Cons an element in front of a Vec.

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

Source#

Add a single element at the end of a Vec.

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

Source#

The first element of a Vec.

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

Source#

The last element of a Vec.

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

Source#

The elements after the head of a Vec.

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

Source#

The elements before the last of a Vec.

Reverse

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

Source#

Reverse Vec.

Folds

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

Source#

See Foldable.

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

Source#

See Foldable1.

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

Source#

See I.FoldableWithIndex.

valueifoldMap1

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

Source#

There is no type-class for this :(

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

Source#

Right fold.

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

Source#

Right fold with an index.

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

Source#

Strict left fold.

Special folds

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

Source#

Yield the length of a Vec.

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

Source#

Test whether a Vec is empty.

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

Source#

Strict sum.

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

Source#

Strict product.

Mapping

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

Source#

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

Source#

Example1 expression

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

Zipping

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

Source#

Zip two Vecs with a function.

valueizipWith :: (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c

Source#

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

valuerepeat :: x -> Vec n x

Source#

Repeat value

Monadic

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

Source#

Monadic bind.

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

Source#

Monadic join.

Universe

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

Source#

Get all Fin n in a Vec n.

Example1 expression

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