vec-0.3: Vec: length-indexed (sized) list

Data.Vec.DataFamily.SpineStrict

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)

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

# Documentation

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

Vector, i.e. length-indexed list.

Instances
 InlineInduction n => Monad (Vec n) Source # Instance detailsDefined 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 detailsDefined in Data.Vec.DataFamily.SpineStrict Methodsfmap :: (a -> b) -> Vec n a -> Vec n b #(<$) :: a -> Vec n b -> Vec n a # Source # Instance detailsDefined in Data.Vec.DataFamily.SpineStrict Methodspure :: 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 detailsDefined in Data.Vec.DataFamily.SpineStrict Methodsfold :: 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 # Source # Instance detailsDefined in Data.Vec.DataFamily.SpineStrict Methodstraverse :: 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) Source # Instance detailsDefined in Data.Vec.DataFamily.SpineStrict MethodsliftArbitrary :: Gen a -> Gen (Vec n a) #liftShrink :: (a -> [a]) -> Vec n a -> [Vec n a] # Source # Instance detailsDefined in Data.Vec.DataFamily.SpineStrict Methodsdistribute :: 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) # Source # Instance detailsDefined in Data.Vec.DataFamily.SpineStrict Associated Typestype Rep (Vec n) :: Type # Methodstabulate :: (Rep (Vec n) -> a) -> Vec n a #index :: Vec n a -> Rep (Vec n) -> a # (InlineInduction m, n ~ S m) => Traversable1 (Vec n) Source # Instance detailsDefined in Data.Vec.DataFamily.SpineStrict Methodstraverse1 :: 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 detailsDefined in Data.Vec.DataFamily.SpineStrict Methodsfold1 :: Semigroup m => Vec n m -> m #foldMap1 :: Semigroup m => (a -> m) -> Vec n a -> m #toNonEmpty :: Vec n a -> NonEmpty a # InlineInduction n => Apply (Vec n) Source # Instance detailsDefined 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 n => Bind (Vec n) Source # Instance detailsDefined 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 # (Eq a, InlineInduction n) => Eq (Vec n a) Source # >>> 'a' ::: 'b' ::: VNil == 'a' ::: 'c' ::: VNil False  Instance detailsDefined 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 detailsDefined in Data.Vec.DataFamily.SpineStrict Methodscompare :: 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 detailsDefined in Data.Vec.DataFamily.SpineStrict MethodsshowsPrec :: 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 detailsDefined 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 detailsDefined in Data.Vec.DataFamily.SpineStrict Methodsmempty :: 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) Source # Instance detailsDefined in Data.Vec.DataFamily.SpineStrict Methodsfunction :: (Vec n a -> b) -> Vec n a :-> b # (SNatI n, Arbitrary a) => Arbitrary (Vec n a) Source # Instance detailsDefined in Data.Vec.DataFamily.SpineStrict Methodsarbitrary :: Gen (Vec n a) #shrink :: Vec n a -> [Vec n a] # (SNatI n, CoArbitrary a) => CoArbitrary (Vec n a) Source # Instance detailsDefined in Data.Vec.DataFamily.SpineStrict Methodscoarbitrary :: Vec n a -> Gen b -> Gen b # (NFData a, InlineInduction n) => NFData (Vec n a) Source # Instance detailsDefined in Data.Vec.DataFamily.SpineStrict Methodsrnf :: Vec n a -> () # (Hashable a, InlineInduction n) => Hashable (Vec n a) Source # Instance detailsDefined in Data.Vec.DataFamily.SpineStrict MethodshashWithSalt :: Int -> Vec n a -> Int #hash :: Vec n a -> Int # data Vec Z a Source # Instance detailsDefined in Data.Vec.DataFamily.SpineStrict data Vec Z a = VNil type Rep (Vec n) Source # Instance detailsDefined in Data.Vec.DataFamily.SpineStrict type Rep (Vec n) = Fin n data Vec (S n) a Source # Instance detailsDefined in Data.Vec.DataFamily.SpineStrict data Vec (S n) a = a ::: !(Vec n a) # Construction 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. 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


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'


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

Tabulating, inverse of !.

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


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

Cons an element in front of a Vec.

snoc :: forall n a. InlineInduction n => Vec n a -> a -> Vec (S n) a Source #

Add a single element at the end 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.

# Reverse

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

Reverse Vec.

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


Since: 0.2.1

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

repeat :: InlineInduction n => x -> Vec n x Source #

Repeat value

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


Since: 0.2.1

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

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

>>> 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. If we have an undefined Vec, >>> let v = error "err" :: Vec N.Nat3 Char  And insert data into it later: >>> let setHead :: a -> Vec ('S n) a -> Vec ('S n) a; setHead x (_ ::: xs) = x ::: xs  Then without a spine, it will fail: >>> head$ setHead 'x' v
*** Exception: err

>>> head $setHead 'x'$ ensureSpine v
'x'