Data.Vec.Lazy

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

Documentation

data Vec (n :: Nat) a where

Vector, i.e. length-indexed list.

Constructors

VNil :: Vec 'Z a

(:::) :: a -> Vec n a -> Vec ('S n) a infixr 5

Instances

SNatI n => Monad (Vec n)

Defined in Data.Vec.Lazy

Methods

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

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

return :: a -> Vec n a

Functor (Vec n)

Defined in Data.Vec.Lazy

Methods

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

(<$) :: a -> Vec n b -> Vec n a

SNatI n => Applicative (Vec n)

Defined in Data.Vec.Lazy

Methods

pure :: a -> Vec n a

(<*>) :: Vec n (a -> b) -> Vec n a -> Vec n b

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

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

(<*) :: Vec n a -> Vec n b -> Vec n a

Foldable (Vec n)

Defined in Data.Vec.Lazy

Methods

fold :: Monoid m => Vec n m -> m

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

foldMap' :: Monoid m => (a -> m) -> Vec n a -> m

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

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

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

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

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

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

toList :: Vec n a -> [a]

null :: Vec n a -> Bool

length :: Vec n a -> Int

elem :: Eq a => a -> Vec n a -> Bool

maximum :: Ord a => Vec n a -> a

minimum :: Ord a => Vec n a -> a

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

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

Traversable (Vec n)

Defined in Data.Vec.Lazy

Methods

traverse :: Applicative f => (a -> f b) -> Vec n a -> f (Vec n b)

sequenceA :: Applicative f => Vec n (f a) -> f (Vec n a)

mapM :: Monad m => (a -> m b) -> Vec n a -> m (Vec n b)

sequence :: Monad m => Vec n (m a) -> m (Vec n a)

SNatI n => Arbitrary1 (Vec n)

Defined in Data.Vec.Lazy

Methods

liftArbitrary :: Gen a -> Gen (Vec n a)

liftShrink :: (a -> [a]) -> Vec n a -> [Vec n a]

SNatI n => Distributive (Vec n)

Defined in Data.Vec.Lazy

Methods

distribute :: Functor f => f (Vec n a) -> Vec n (f a)

collect :: Functor f => (a -> Vec n b) -> f a -> Vec n (f b)

distributeM :: Monad m => m (Vec n a) -> Vec n (m a)

collectM :: Monad m => (a -> Vec n b) -> m a -> Vec n (m b)

SNatI n => Representable (Vec n)

Defined in Data.Vec.Lazy

Associated Types

type Rep (Vec n)

Methods

tabulate :: (Rep (Vec n) -> a) -> Vec n a

index :: Vec n a -> Rep (Vec n) -> a

Eq1 (Vec n)

Since: 0.4

Defined in Data.Vec.Lazy

Methods

liftEq :: (a -> b -> Bool) -> Vec n a -> Vec n b -> Bool

Ord1 (Vec n)

Since: 0.4

Defined in Data.Vec.Lazy

Methods

liftCompare :: (a -> b -> Ordering) -> Vec n a -> Vec n b -> Ordering

Show1 (Vec n)

Since: 0.4

Defined in Data.Vec.Lazy

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Vec n a -> ShowS

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Vec n a] -> ShowS

n ~ 'S m => Traversable1 (Vec n)

Defined in Data.Vec.Lazy

Methods

traverse1 :: Apply f => (a -> f b) -> Vec n a -> f (Vec n b)

sequence1 :: Apply f => Vec n (f b) -> f (Vec n b)

n ~ 'S m => Foldable1 (Vec n)

Defined in Data.Vec.Lazy

Methods

fold1 :: Semigroup m => Vec n m -> m

foldMap1 :: Semigroup m => (a -> m) -> Vec n a -> m

toNonEmpty :: Vec n a -> NonEmpty a

Apply (Vec n)

Defined in Data.Vec.Lazy

Methods

(<.>) :: Vec n (a -> b) -> Vec n a -> Vec n b

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

(<.) :: Vec n a -> Vec n b -> Vec n a

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

Bind (Vec n)

Defined in Data.Vec.Lazy

Methods

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

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

FunctorWithIndex (Fin n) (Vec n)

Since: 0.4

Defined in Data.Vec.Lazy

Methods

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

FoldableWithIndex (Fin n) (Vec n)

Since: 0.4

Defined in Data.Vec.Lazy

Methods

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

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

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

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

ifoldr' :: (Fin n -> a -> b -> b) -> b -> Vec n a -> b

ifoldl' :: (Fin n -> b -> a -> b) -> b -> Vec n a -> b

TraversableWithIndex (Fin n) (Vec n)

Since: 0.4

Defined in Data.Vec.Lazy

Methods

itraverse :: Applicative f => (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)

Eq a => Eq (Vec n a)

Defined in Data.Vec.Lazy

Methods

(==) :: Vec n a -> Vec n a -> Bool

(/=) :: Vec n a -> Vec n a -> Bool

Ord a => Ord (Vec n a)

Defined in Data.Vec.Lazy

Methods

compare :: Vec n a -> Vec n a -> Ordering

(<) :: Vec n a -> Vec n a -> Bool

(<=) :: Vec n a -> Vec n a -> Bool

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

(>=) :: Vec n a -> Vec n a -> Bool

max :: Vec n a -> Vec n a -> Vec n a

min :: Vec n a -> Vec n a -> Vec n a

Show a => Show (Vec n a)

Defined in Data.Vec.Lazy

Methods

showsPrec :: Int -> Vec n a -> ShowS

show :: Vec n a -> String

showList :: [Vec n a] -> ShowS

Semigroup a => Semigroup (Vec n a)

Defined in Data.Vec.Lazy

Methods

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

sconcat :: NonEmpty (Vec n a) -> Vec n a

stimes :: Integral b => b -> Vec n a -> Vec n a

(Monoid a, SNatI n) => Monoid (Vec n a)

Defined in Data.Vec.Lazy

Methods

mempty :: Vec n a

mappend :: Vec n a -> Vec n a -> Vec n a

mconcat :: [Vec n a] -> Vec n a

(SNatI n, Function a) => Function (Vec n a)

Defined in Data.Vec.Lazy

Methods

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

(SNatI n, Arbitrary a) => Arbitrary (Vec n a)

Defined in Data.Vec.Lazy

Methods

arbitrary :: Gen (Vec n a)

shrink :: Vec n a -> [Vec n a]

(SNatI n, CoArbitrary a) => CoArbitrary (Vec n a)

Defined in Data.Vec.Lazy

Methods

coarbitrary :: Vec n a -> Gen b -> Gen b

NFData a => NFData (Vec n a)

Defined in Data.Vec.Lazy

Methods

rnf :: Vec n a -> ()

Hashable a => Hashable (Vec n a)

Defined in Data.Vec.Lazy

Methods

hashWithSalt :: Int -> Vec n a -> Int

hash :: Vec n a -> Int

type Rep (Vec n)

Defined in Data.Vec.Lazy

type Rep (Vec n) = Fin n

Construction

empty :: Vec 'Z a

Empty Vec.

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

Vec with exactly one element.

>>> singleton True
True ::: VNil

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

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:

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

toPull :: Vec n a -> Vec n a

Convert to pull Vec.

fromPull :: forall n a. SNatI n => Vec n a -> Vec n a

Convert from pull Vec.

toList :: Vec n a -> [a]

Convert Vec to list.

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

toNonEmpty :: Vec ('S n) a -> NonEmpty a

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

Since: 0.4

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

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

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

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

reifyList :: [a] -> (forall n. SNatI n => Vec n a -> r) -> r

Reify any list [a] to Vec n a.

>>> reifyList "foo" length
3

Indexing

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

Indexing.

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

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

Tabulating, inverse of !.

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

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

Cons an element in front of a Vec.

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

Add a single element at the end of a Vec.

Since: 0.2.1

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

The first element of a Vec.

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

The last element of a Vec.

Since: 0.4

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

The elements after the head of a Vec.

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

The elements before the last of a Vec.

Since: 0.4

Reverse

reverse :: Vec n a -> Vec n a

Reverse Vec.

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

Since: 0.2.1

Concatenation and splitting

(++) :: Vec n a -> Vec m a -> Vec (Plus n m) a infixr 5

Append two Vec.

>>> ('a' ::: 'b' ::: VNil) ++ ('c' ::: 'd' ::: VNil)
'a' ::: 'b' ::: 'c' ::: 'd' ::: VNil

split :: SNatI n => Vec (Plus n m) a -> (Vec n a, Vec m a)

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

concatMap :: (a -> Vec m b) -> Vec n a -> Vec (Mult n m) b

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

concat :: Vec n (Vec m a) -> Vec (Mult n m) a

concatMap id

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

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)

Take and drop

take :: forall n m a. LE n m => Vec m a -> Vec n a

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

drop :: forall n m a. (LE n m, SNatI m) => Vec m a -> Vec n a

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

Folds

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

See Foldable.

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

See Foldable1.

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

See FoldableWithIndex.

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

There is no type-class for this :(

foldr :: forall a b n. (a -> b -> b) -> b -> Vec n a -> b

Right fold.

ifoldr :: forall a b n. (Fin n -> a -> b -> b) -> b -> Vec n a -> b

Right fold with an index.

foldl' :: forall a b n. (b -> a -> b) -> b -> Vec n a -> b

Strict left fold.

Special folds

length :: Vec n a -> Int

Yield the length of a Vec. O(n)

null :: Vec n a -> Bool

Test whether a Vec is empty. O(1)

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

Non-strict sum.

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

Non-strict product.

Mapping

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

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

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

>>> imap (,) $ 'a' ::: 'b' ::: 'c' ::: VNil
(0,'a') ::: (1,'b') ::: (2,'c') ::: VNil

traverse :: forall n f a b. Applicative f => (a -> f b) -> Vec n a -> f (Vec n b)

Apply an action to every element of a Vec, yielding a Vec of results.

traverse1 :: forall n f a b. Apply f => (a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b)

Apply an action to non-empty Vec, yielding a Vec of results.

itraverse :: Applicative f => (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)

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

itraverse_ :: Applicative f => (Fin n -> a -> f b) -> Vec n a -> f ()

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

Zipping

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

Zip two Vecs with a function.

izipWith :: (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.

repeat :: SNatI n => x -> Vec n x

Repeat a value.

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

Since: 0.2.1

Monadic

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

Monadic bind.

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

Monadic join.

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

Universe

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

Get all Fin n in a Vec n.

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

VecEach

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

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. SNatI n => Vec n a -> Vec n b) -> s -> t

traverseWithVec :: Applicative f => (forall n. SNatI n => Vec n a -> f (Vec n b)) -> s -> f t

Instances

(a ~ a', b ~ b') => VecEach (a, a') (b, b') a b

Defined in Data.Vec.Lazy

Methods

mapWithVec :: (forall (n :: Nat). SNatI n => Vec n a -> Vec n b) -> (a, a') -> (b, b')

traverseWithVec :: Applicative f => (forall (n :: Nat). SNatI n => Vec n a -> f (Vec n b)) -> (a, a') -> f (b, b')

(a ~ a2, a ~ a3, b ~ b2, b ~ b3) => VecEach (a, a2, a3) (b, b2, b3) a b

Defined in Data.Vec.Lazy

Methods

mapWithVec :: (forall (n :: Nat). SNatI n => Vec n a -> Vec n b) -> (a, a2, a3) -> (b, b2, b3)

traverseWithVec :: Applicative f => (forall (n :: Nat). SNatI n => Vec n a -> f (Vec n b)) -> (a, a2, a3) -> f (b, b2, b3)

(a ~ a2, a ~ a3, a ~ a4, b ~ b2, b ~ b3, b ~ b4) => VecEach (a, a2, a3, a4) (b, b2, b3, b4) a b

Defined in Data.Vec.Lazy

Methods

mapWithVec :: (forall (n :: Nat). SNatI n => Vec n a -> Vec n b) -> (a, a2, a3, a4) -> (b, b2, b3, b4)

traverseWithVec :: Applicative f => (forall (n :: Nat). SNatI n => Vec n a -> f (Vec n b)) -> (a, a2, a3, a4) -> f (b, b2, b3, b4)