Modulevec-0.5.1.1Haskell2010

Data.Vec.Lazy.Inline

A variant of Data.Vec.Lazy with functions written using SNatI. The hypothesis is that these (goursive) functions could be fully unrolled, if the Vec size n is known at compile time.

The module has the same API as Data.Vec.Lazy (sans L.withDict and foldl'). Note: instance methods aren't changed, the Vec type is the same.

Contents

Construction
Conversions
Indexing
Concatenation and splitting
Reverse
Folds
Special folds
Mapping
Zipping
Monadic
Universe
VecEach

Synopsis

data Vec
value empty
value singleton
value toPull
value fromPull
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 ++
value split
value concatMap
value concat
value chunks
value reverse
value foldMap
value foldMap1
value ifoldMap
value ifoldMap1
value foldr
value ifoldr
value length
value null
value sum
value product
value map
value imap
value traverse
value traverse1
value itraverse
value itraverse_
value zipWith
value izipWith
value repeat
value bind
value join
value universe
class VecEach

Packagevec-0.5.1.1
Exports47
LanguageHaskell2010
LicenceBSD-3-Clause
SourceInline.hs

datadata Vec (n :: Nat) a where

Source#

Vector, i.e. length-indexed list.

Constructors

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

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

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

Construction

valueempty :: Vec 'Z a

Source#

Empty Vec.

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

Source#

Vec with exactly one element.

Example1 expression

>>> singleton TrueTrue ::: VNil

Conversions

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

Source#

Convert to pull Vec.

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

Source#

Convert from pull Vec.

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

Source#

Convert Vec to list.

Example1 expression

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

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

Source#

Example1 expression

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

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

>>> 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)

Source#

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

Source#

Reify any list [a] to Vec n a.

Example1 expression

>>> reifyList "foo" length3

Indexing

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

Source#

Indexing.

Example1 expression

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

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

Source#

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

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.

Concatenation and splitting

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

Source#

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)

Source#

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

Source#

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

Source#

concatMap id

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

Source#

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

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

Source#

Reverse Vec.

Example1 expression

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

Folds

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

Source#

See I.Foldable.

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

Source#

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

Special folds

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

Source#

Yield the length of a Vec. O(n)

valuenull :: Vec n a -> Bool

Source#

Test whether a Vec is empty. O(1)

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

Source#

Non-strict sum.

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

Source#

Non-strict product.

Mapping

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

Source#

Example1 expression

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

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

Source#

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)

Source#

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)

Source#

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)

Source#

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 ()

Source#

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

Zipping

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

Source#

Zip two Vecs with a function.

valueizipWith

:: SNatI n
=> 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 :: SNatI n => x -> Vec n x

Source#

Repeat value

Example1 expression

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

Monadic

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

Source#

Monadic bind.

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

Source#

Monadic join.

Example1 expression

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

Universe

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

Source#

Get all Fin n in a Vec n.

Example1 expression

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

VecEach

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

Source#

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.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.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.1 · Data.Vec.Lazy