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

Safe HaskellNone
LanguageHaskell2010

Data.Vec.DataFamily.SpineStrict

Contents

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

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

SNatI n => Arbitrary1 (Vec n) Source # 
Instance details

Defined in Data.Vec.DataFamily.SpineStrict

Methods

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

liftShrink :: (a -> [a]) -> Vec n a -> [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 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 => 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 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 #

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

(SNatI n, Function a) => Function (Vec n a) Source # 
Instance details

Defined in Data.Vec.DataFamily.SpineStrict

Methods

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

(SNatI n, Arbitrary a) => Arbitrary (Vec n a) Source # 
Instance details

Defined in Data.Vec.DataFamily.SpineStrict

Methods

arbitrary :: Gen (Vec n a) #

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

(SNatI n, CoArbitrary a) => CoArbitrary (Vec n a) Source # 
Instance details

Defined in Data.Vec.DataFamily.SpineStrict

Methods

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

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

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)

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.

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

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 #

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

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

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

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.

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

But with the spine, it won't:

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