Safe Haskell	None
Language	Haskell2010

Data.Vec.DataFamily.SpineStrict

Contents

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

Description

Spine-strict length-indexed list defined as data-family: Vec.

Data family variant allows lazy pattern matching. On the other hand, the Vec value doesn't "know" its length (i.e. there isn't withDict).

Agda

If you happen to familiar with Agda, then the difference between GADT and data-family version is maybe clearer:

module Vec where

open import Data.Nat
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

-- "GADT"
data Vec (A : Set) : ℕ → Set where
  []  : Vec A 0
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

infixr 50 _∷_

exVec : Vec ℕ 2
exVec = 13 ∷ 37 ∷ []

-- "data family"
data Unit : Set where
  [] : Unit

data _×_ (A B : Set) : Set where
  _∷_ : A → B → A × B

infixr 50 _×_

VecF : Set → ℕ → Set
VecF A zero    = Unit
VecF A (suc n) = A × VecF A n

exVecF : VecF ℕ 2
exVecF = 13 ∷ 37 ∷ []

reduction : VecF ℕ 2 ≡ ℕ × ℕ × Unit
reduction = refl

Synopsis

data family Vec (n :: Nat) a
empty :: Vec Z a
singleton :: a -> Vec (S Z) a
toPull :: forall n a. InlineInduction n => Vec n a -> Vec n a
fromPull :: forall n a. InlineInduction n => Vec n a -> Vec n a
_Pull :: InlineInduction n => Iso (Vec n a) (Vec n b) (Vec n a) (Vec n b)
toList :: forall n a. InlineInduction n => Vec n a -> [a]
fromList :: InlineInduction n => [a] -> Maybe (Vec n a)
_Vec :: InlineInduction n => Prism' [a] (Vec n a)
fromListPrefix :: InlineInduction n => [a] -> Maybe (Vec n a)
reifyList :: [a] -> (forall n. InlineInduction n => Vec n a -> r) -> r
(!) :: InlineInduction n => Vec n a -> Fin n -> a
ix :: forall n a. InlineInduction n => Fin n -> Lens' (Vec n a) a
_Cons :: Iso (Vec (S n) a) (Vec (S n) b) (a, Vec n a) (b, Vec n b)
_head :: Lens' (Vec (S n) a) a
_tail :: Lens' (Vec (S n) a) (Vec n a)
cons :: a -> Vec n a -> Vec (S n) a
head :: Vec (S n) a -> a
tail :: Vec (S n) a -> Vec n a
(++) :: forall n m a. InlineInduction n => Vec n a -> Vec m a -> Vec (Plus n m) a
split :: InlineInduction n => Vec (Plus n m) a -> (Vec n a, Vec m a)
concatMap :: forall a b n m. (InlineInduction m, InlineInduction n) => (a -> Vec m b) -> Vec n a -> Vec (Mult n m) b
concat :: (InlineInduction m, InlineInduction n) => Vec n (Vec m a) -> Vec (Mult n m) a
chunks :: (InlineInduction n, InlineInduction m) => Vec (Mult n m) a -> Vec n (Vec m a)
foldMap :: (Monoid m, InlineInduction n) => (a -> m) -> Vec n a -> m
foldMap1 :: forall s a n. (Semigroup s, InlineInduction n) => (a -> s) -> Vec (S n) a -> s
ifoldMap :: forall a n m. (Monoid m, InlineInduction n) => (Fin n -> a -> m) -> Vec n a -> m
ifoldMap1 :: forall a n s. (Semigroup s, InlineInduction n) => (Fin (S n) -> a -> s) -> Vec (S n) a -> s
foldr :: forall a b n. InlineInduction n => (a -> b -> b) -> b -> Vec n a -> b
ifoldr :: forall a b n. InlineInduction n => (Fin n -> a -> b -> b) -> b -> Vec n a -> b
length :: forall n a. InlineInduction n => Vec n a -> Int
null :: forall n a. SNatI n => Vec n a -> Bool
sum :: (Num a, InlineInduction n) => Vec n a -> a
product :: (Num a, InlineInduction n) => Vec n a -> a
map :: forall a b n. InlineInduction n => (a -> b) -> Vec n a -> Vec n b
imap :: InlineInduction n => (Fin n -> a -> b) -> Vec n a -> Vec n b
traverse :: forall n f a b. (Applicative f, InlineInduction n) => (a -> f b) -> Vec n a -> f (Vec n b)
traverse1 :: forall n f a b. (Apply f, InlineInduction n) => (a -> f b) -> Vec (S n) a -> f (Vec (S n) b)
itraverse :: forall n f a b. (Applicative f, InlineInduction n) => (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
itraverse_ :: forall n f a b. (Applicative f, InlineInduction n) => (Fin n -> a -> f b) -> Vec n a -> f ()
zipWith :: forall a b c n. InlineInduction n => (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
izipWith :: InlineInduction n => (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
bind :: InlineInduction n => Vec n a -> (a -> Vec n b) -> Vec n b
join :: InlineInduction n => Vec n (Vec n a) -> Vec n a
universe :: InlineInduction n => Vec n (Fin n)
ensureSpine :: InlineInduction n => Vec n a -> Vec n a

Documentation

data family Vec (n :: Nat) a infixr 5 Source #

Vector, i.e. length-indexed list.

Instances

InlineInduction n => Monad (Vec n) Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict 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 # fail :: String -> Vec n a #
InlineInduction n => Functor (Vec n) Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict Methods fmap :: (a -> b) -> Vec n a -> Vec n b # (<$) :: a -> Vec n b -> Vec n a #
InlineInduction n => Applicative (Vec n) Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict 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 #
InlineInduction n => Foldable (Vec n) Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict Methods fold :: Monoid m => Vec n m -> 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 #
InlineInduction n => Traversable (Vec n) Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict 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) #
InlineInduction n => Distributive (Vec n) Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict 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) #
InlineInduction n => Representable (Vec n) Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict Associated Types type Rep (Vec n) :: Type # Methods tabulate :: (Rep (Vec n) -> a) -> Vec n a # index :: Vec n a -> Rep (Vec n) -> a #
InlineInduction n => Apply (Vec n) Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict 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 #
(InlineInduction m, n ~ S m) => Traversable1 (Vec n) Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict 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) #
(InlineInduction m, n ~ S m) => Foldable1 (Vec n) Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict Methods fold1 :: Semigroup m => Vec n m -> m # foldMap1 :: Semigroup m => (a -> m) -> Vec n a -> m # toNonEmpty :: Vec n a -> NonEmpty a #
InlineInduction n => Bind (Vec n) Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict Methods (>>-) :: Vec n a -> (a -> Vec n b) -> Vec n b # join :: Vec n (Vec n a) -> Vec n a #
InlineInduction n => FunctorWithIndex (Fin n) (Vec n) Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict Methods imap :: (Fin n -> a -> b) -> Vec n a -> Vec n b # imapped :: IndexedSetter (Fin n) (Vec n a) (Vec n b) a b #
InlineInduction n => FoldableWithIndex (Fin n) (Vec n) Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict Methods ifoldMap :: Monoid m => (Fin n -> a -> m) -> Vec n a -> m # ifolded :: IndexedFold (Fin n) (Vec n a) a # 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 #
InlineInduction n => TraversableWithIndex (Fin n) (Vec n) Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict Methods itraverse :: Applicative f => (Fin n -> a -> f b) -> Vec n a -> f (Vec n b) # itraversed :: IndexedTraversal (Fin n) (Vec n a) (Vec n b) a b #
(Eq a, InlineInduction n) => Eq (Vec n a) Source #	`>>>` `'a' ::: 'b' ::: VNil == 'a' ::: 'c' ::: VNil`False
Instance details Defined in Data.Vec.DataFamily.SpineStrict Methods (==) :: Vec n a -> Vec n a -> Bool # (/=) :: Vec n a -> Vec n a -> Bool #
(Ord a, InlineInduction n) => Ord (Vec n a) Source #	`>>>` `compare ('a' ::: 'b' ::: VNil) ('a' ::: 'c' ::: VNil)`LT
Instance details Defined in Data.Vec.DataFamily.SpineStrict 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, InlineInduction n) => Show (Vec n a) Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict Methods showsPrec :: Int -> Vec n a -> ShowS # show :: Vec n a -> String # showList :: [Vec n a] -> ShowS #
(Semigroup a, InlineInduction n) => Semigroup (Vec n a) Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict 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, InlineInduction n) => Monoid (Vec n a) Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict Methods mempty :: Vec n a # mappend :: Vec n a -> Vec n a -> Vec n a # mconcat :: [Vec n a] -> Vec n a #
(NFData a, InlineInduction n) => NFData (Vec n a) Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict Methods rnf :: Vec n a -> () #
(Hashable a, InlineInduction n) => Hashable (Vec n a) Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict Methods hashWithSalt :: Int -> Vec n a -> Int # hash :: Vec n a -> Int #
InlineInduction n => Ixed (Vec n a) Source #	`Vec` doesn't have `At` instance, as we cannot remove value from `Vec`. See `ix` in Data.Vec.DataFamily.SpineStrict module for an `Lens` (not `Traversal`).
Instance details Defined in Data.Vec.DataFamily.SpineStrict Methods ix :: Index (Vec n a) -> Traversal' (Vec n a) (IxValue (Vec n a)) #
InlineInduction n => Each (Vec n a) (Vec n b) a b Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict Methods each :: Traversal (Vec n a) (Vec n b) a b #
Field1 (Vec (S n) a) (Vec (S n) a) a a Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict Methods _1 :: Lens (Vec (S n) a) (Vec (S n) a) a a #
Field2 (Vec (S (S n)) a) (Vec (S (S n)) a) a a Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict Methods _2 :: Lens (Vec (S (S n)) a) (Vec (S (S n)) a) a a #
Field3 (Vec (S (S (S n))) a) (Vec (S (S (S n))) a) a a Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict Methods _3 :: Lens (Vec (S (S (S n))) a) (Vec (S (S (S n))) a) a a #
Field4 (Vec (S (S (S (S n)))) a) (Vec (S (S (S (S n)))) a) a a Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict Methods _4 :: Lens (Vec (S (S (S (S n)))) a) (Vec (S (S (S (S n)))) a) a a #
Field5 (Vec (S (S (S (S (S n))))) a) (Vec (S (S (S (S (S n))))) a) a a Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict Methods _5 :: Lens (Vec (S (S (S (S (S n))))) a) (Vec (S (S (S (S (S n))))) a) a a #
Field6 (Vec (S (S (S (S (S (S n)))))) a) (Vec (S (S (S (S (S (S n)))))) a) a a Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict Methods _6 :: Lens (Vec (S (S (S (S (S (S n)))))) a) (Vec (S (S (S (S (S (S n)))))) a) a a #
Field7 (Vec (S (S (S (S (S (S (S n))))))) a) (Vec (S (S (S (S (S (S (S n))))))) a) a a Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict Methods _7 :: Lens (Vec (S (S (S (S (S (S (S n))))))) a) (Vec (S (S (S (S (S (S (S n))))))) a) a a #
Field8 (Vec (S (S (S (S (S (S (S (S n)))))))) a) (Vec (S (S (S (S (S (S (S (S n)))))))) a) a a Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict Methods _8 :: Lens (Vec (S (S (S (S (S (S (S (S n)))))))) a) (Vec (S (S (S (S (S (S (S (S n)))))))) a) a a #
Field9 (Vec (S (S (S (S (S (S (S (S (S n))))))))) a) (Vec (S (S (S (S (S (S (S (S (S n))))))))) a) a a Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict Methods _9 :: Lens (Vec (S (S (S (S (S (S (S (S (S n))))))))) a) (Vec (S (S (S (S (S (S (S (S (S n))))))))) a) a a #
data Vec Z a Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict data Vec Z a = VNil
type Rep (Vec n) Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict type Rep (Vec n) = Fin n
data Vec (S n) a Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict data Vec (S n) a = a ::: !(Vec n a)
type Index (Vec n a) Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict type Index (Vec n a) = Fin n
type IxValue (Vec n a) Source #
Instance details Defined in Data.Vec.DataFamily.SpineStrict type IxValue (Vec n a) = a

Construction

empty :: Vec Z a Source #

Empty Vec.

singleton :: a -> Vec (S Z) a Source #

Vec with exactly one element.

>>> singleton True
True ::: VNil

Conversions

toPull :: forall n a. InlineInduction n => Vec n a -> Vec n a Source #

Convert to pull Vec.

fromPull :: forall n a. InlineInduction n => Vec n a -> Vec n a Source #

Convert from pull Vec.

_Pull :: InlineInduction n => Iso (Vec n a) (Vec n b) (Vec n a) (Vec n b) Source #

An Iso from toPull and fromPull.

toList :: forall n a. InlineInduction n => Vec n a -> [a] Source #

Convert Vec to list.

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

fromList :: InlineInduction n => [a] -> Maybe (Vec n a) Source #

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

_Vec :: InlineInduction n => Prism' [a] (Vec n a) Source #

Prism from list.

>>> "foo" ^? _Vec :: Maybe (Vec N.Nat3 Char)
Just ('f' ::: 'o' ::: 'o' ::: VNil)

>>> "foo" ^? _Vec :: Maybe (Vec N.Nat2 Char)
Nothing

>>> _Vec # (True ::: False ::: VNil)
[True,False]

fromListPrefix :: InlineInduction n => [a] -> Maybe (Vec n a) Source #

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. InlineInduction n => Vec n a -> r) -> r Source #

Reify any list [a] to Vec n a.

>>> reifyList "foo" length
3

Indexing

(!) :: InlineInduction n => Vec n a -> Fin n -> a Source #

Indexing.

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

ix :: forall n a. InlineInduction n => Fin n -> Lens' (Vec n a) a Source #

Index lens.

>>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. ix (FS FZ)
'b'

>>> ('a' ::: 'b' ::: 'c' ::: VNil) & ix (FS FZ) .~ 'x'
'a' ::: 'x' ::: 'c' ::: VNil

_Cons :: Iso (Vec (S n) a) (Vec (S n) b) (a, Vec n a) (b, Vec n b) Source #

Match on non-empty Vec.

Note: lens _Cons is a Prism. In fact, Vec n a cannot have an instance of Cons as types don't match.

_head :: Lens' (Vec (S n) a) a Source #

Head lens. Note: lens _head is a Traversal'.

>>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. _head
'a'

>>> ('a' ::: 'b' ::: 'c' ::: VNil) & _head .~ 'x'
'x' ::: 'b' ::: 'c' ::: VNil

_tail :: Lens' (Vec (S n) a) (Vec n a) Source #

Head lens. Note: lens _head is a Traversal'.

cons :: a -> Vec n a -> Vec (S n) a Source #

Cons an element in front of a Vec.

head :: Vec (S n) a -> a Source #

The first element of a Vec.

tail :: Vec (S n) a -> Vec n a Source #

The elements after the head of a Vec.

Concatenation and splitting

(++) :: forall n m a. InlineInduction n => Vec n a -> Vec m a -> Vec (Plus n m) a infixr 5 Source #

Append two Vec.

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

split :: InlineInduction n => Vec (Plus n m) a -> (Vec n a, Vec m a) Source #

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 :: forall a b n m. (InlineInduction m, InlineInduction 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.

>>> concatMap (\x -> x ::: x ::: VNil) ('a' ::: 'b' ::: VNil)
'a' ::: 'a' ::: 'b' ::: 'b' ::: VNil

concat :: (InlineInduction m, InlineInduction n) => Vec n (Vec m a) -> Vec (Mult n m) a Source #

concatMap id

chunks :: (InlineInduction n, InlineInduction m) => Vec (Mult n m) a -> Vec n (Vec m a) Source #

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)

Folds

foldMap :: (Monoid m, InlineInduction n) => (a -> m) -> Vec n a -> m Source #

See Foldable.

foldMap1 :: forall s a n. (Semigroup s, InlineInduction n) => (a -> s) -> Vec (S n) a -> s Source #

See Foldable1.

ifoldMap :: forall a n m. (Monoid m, InlineInduction n) => (Fin n -> a -> m) -> Vec n a -> m Source #

See FoldableWithIndex.

ifoldMap1 :: forall a n s. (Semigroup s, InlineInduction n) => (Fin (S n) -> a -> s) -> Vec (S n) a -> s Source #

There is no type-class for this :(

foldr :: forall a b n. InlineInduction n => (a -> b -> b) -> b -> Vec n a -> b Source #

Right fold.

ifoldr :: forall a b n. InlineInduction n => (Fin n -> a -> b -> b) -> b -> Vec n a -> b Source #

Right fold with an index.

Special folds

length :: forall n a. InlineInduction n => Vec n a -> Int Source #

Yield the length of a Vec. O(n)

null :: forall n a. SNatI n => Vec n a -> Bool Source #

Test whether a Vec is empty. O(1)

sum :: (Num a, InlineInduction n) => Vec n a -> a Source #

Non-strict sum.

product :: (Num a, InlineInduction n) => Vec n a -> a Source #

Non-strict product.

Mapping

map :: forall a b n. InlineInduction n => (a -> b) -> Vec n a -> Vec n b Source #

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

imap :: InlineInduction n => (Fin n -> a -> b) -> Vec n a -> Vec n b Source #

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

traverse :: forall n f a b. (Applicative f, InlineInduction 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.

traverse1 :: forall n f a b. (Apply f, InlineInduction 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.

itraverse :: forall n f a b. (Applicative f, InlineInduction 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.

itraverse_ :: forall n f a b. (Applicative f, InlineInduction 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

zipWith :: forall a b c n. InlineInduction n => (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c Source #

Zip two Vecs with a function.

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

Monadic

bind :: InlineInduction n => Vec n a -> (a -> Vec n b) -> Vec n b Source #

Monadic bind.

join :: InlineInduction n => Vec n (Vec n a) -> Vec n a Source #

Monadic join.

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

Universe

universe :: InlineInduction n => Vec n (Fin n) Source #

Get all Fin n in a Vec n.

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

Extras

ensureSpine :: InlineInduction n => Vec n a -> Vec n a Source #

Ensure spine.

>>> view (ix F.fin1) $ set (ix F.fin1) 'x' (error "err" :: Vec N.Nat2 Char)
*** Exception: err
...

>>> view (ix F.fin1) $ set (ix F.fin1) 'x' $ ensureSpine (error "err" :: Vec N.Nat2 Char)
'x'