Modulevec-0.5.1.1Haskell2010

Data.Vec.Lazy

Lazy (in elements and spine) length-indexed list: Vec.

Contents

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

Synopsis

data Vec
value empty
value singleton
value withDict
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 reverse
value dfoldr
value dfoldl
value dfoldl'
value ++
value split
value concatMap
value concat
value chunks
value take
value drop
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 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
Exports54
LanguageHaskell2010
LicenceBSD-3-Clause
SourceLazy.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

valuewithDict :: Vec n a -> (SNatI n => r) -> r

Source#

O(n). Recover SNatI (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:

Example1 expression

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

Conversions

valuetoPull :: 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 :: Vec n a -> [a]

Source#

Convert Vec to list.

Example1 expression

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

valuetoNonEmpty :: 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(!) :: 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 :: 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 :: 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 :: Vec ('S n) a -> Vec n a

Source#

The elements before the last of a Vec.

Reverse

valuereverse :: Vec n a -> Vec n a

Source#

Reverse Vec.

Example1 expression

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

Dependent folds

valuedfoldr

:: forall (m :: Nat). a -> f m -> f ('S m)
-> f 'Z
-> Vec n a
-> f n

Source#

Dependent right fold.

This could been called an indexed fold, but that name is already used.

valuedfoldl

:: forall (m :: Nat). f m -> a -> f ('S m)
-> f 'Z
-> Vec n a
-> f n

Source#

Dependent left fold.

valuedfoldl'

:: forall (m :: Nat). f m -> a -> f ('S m)
-> f 'Z
-> Vec n a
-> f n

Source#

Dependent strict left fold.

Concatenation and splitting

value(++) :: 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 :: (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 :: 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)

Take and drop

valuetake :: LE n m => Vec m a -> Vec n a

Source#

Example2 expressions

>>> let xs = 'a' ::: 'b' ::: 'c' ::: 'd' ::: 'e' ::: VNil>>> take xs :: Vec N.Nat3 Char'a' ::: 'b' ::: 'c' ::: VNil

valuedrop :: (LE n m, SNatI m) => Vec m a -> Vec n a

Source#

Example2 expressions

>>> let xs = 'a' ::: 'b' ::: 'c' ::: 'd' ::: 'e' ::: VNil>>> drop xs :: Vec N.Nat3 Char'c' ::: 'd' ::: 'e' ::: VNil

Folds

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

Source#

See Foldable.

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

Source#

See Foldable1.

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

Source#

See I.FoldableWithIndex.

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

Source#

There is no type-class for this :(

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

Source#

Right fold.

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

Source#

Right fold with an index.

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

Source#

Strict left fold.

Special folds

valuelength :: 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 => Vec n a -> a

Source#

Non-strict sum.

valueproduct :: Num a => Vec n a -> a

Source#

Non-strict product.

Mapping

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

Source#

Example1 expression

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

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

Source#

Repeat a value.

Example1 expression

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

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.

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