Modulevec-0.5.1Haskell2010

Data.Vec.DataFamily.SpineStrict

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

46 values

Packagevec-0.5.1
Exports49
LanguageHaskell2010
LicenceBSD-3-Clause
SourceSpineStrict.hs

data familydata family Vec (n :: Nat) a

Vector, i.e. length-indexed list.

Instances31Monad, Functor, Applicative, Foldable, Traversable, Foldable1, …

SNatI n => Monad (Vec n)Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => Functor (Vec n)Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => Applicative (Vec n)Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => Foldable (Vec n)Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => Traversable (Vec n)Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
(SNatI m, n ~ 'S m) => Foldable1 (Vec n)Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => Eq1 (Vec n)Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => Ord1 (Vec n)Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => Show1 (Vec n)Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => Arbitrary1 (Vec n)Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => Distributive (Vec n)Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => Apply (Vec n)Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => Bind (Vec n)Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
(SNatI m, n ~ 'S m) => Traversable1 (Vec n)Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => Representable (Vec n)Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => FoldableWithIndex (Fin n) (Vec n)Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => FunctorWithIndex (Fin n) (Vec n)Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => TraversableWithIndex (Fin n) (Vec n)Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
(Eq a, SNatI n) => Eq (Vec n a)Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
Example1 expression
```
>>> 'a' ::: 'b' ::: VNil == 'a' ::: 'c' ::: VNilFalse
```
(Ord a, SNatI n) => Ord (Vec n a)Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
Example1 expression
```
>>> compare ('a' ::: 'b' ::: VNil) ('a' ::: 'c' ::: VNil)LT
```
(Show a, SNatI n) => Show (Vec n a)Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
(Semigroup a, SNatI n) => Semigroup (Vec n a)Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
(Monoid a, SNatI n) => Monoid (Vec n a)Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
(NFData a, SNatI n) => NFData (Vec n a)Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
(SNatI n, Arbitrary a) => Arbitrary (Vec n a)Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
(SNatI n, CoArbitrary a) => CoArbitrary (Vec n a)Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
(SNatI n, Function a) => Function (Vec n a)Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
(Hashable a, SNatI n) => Hashable (Vec n a)Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
type Rep (Vec n) = Fin nDefined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
data Vec 'Z
- VNil
Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict
data Vec ('S n)
- a ::: Vec n a
Defined in vec-0.5.1 · Data.Vec.DataFamily.SpineStrict

constructora ::: Vec n a

constructorVNil

Construction

2 declarations

valueempty :: Vec 'Z a

Empty Vec.

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

Vec with exactly one element.

Example1 expression

>>> singleton TrueTrue ::: VNil

Conversions

7 declarations

valuetoPull :: SNatI n => Vec n a -> Vec n a

Convert to pull Vec.

valuefromPull :: SNatI n => Vec n a -> Vec n a

Convert from pull Vec.

valuetoList :: SNatI n => Vec n a -> [a]

Convert Vec to list.

Example1 expression

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

valuetoNonEmpty :: SNatI n => Vec ('S n) a -> NonEmpty a

Example1 expression

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

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

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)

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

Reify any list [a] to Vec n a.

Example1 expression

>>> reifyList "foo" length3

Indexing

8 declarations

value(!) :: SNatI n => Vec n a -> Fin n -> a

Indexing.

Example1 expression

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

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

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

Cons an element in front of a Vec.

valuesnoc :: SNatI n => Vec n a -> a -> Vec ('S n) a

Add a single element at the end of a Vec.

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

The first element of a Vec.

valuelast :: SNatI n => Vec ('S n) a -> a

The last element of a Vec.

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

The elements after the head of a Vec.

valueinit :: SNatI n => Vec ('S n) a -> Vec n a

The elements before the last of a Vec.

Reverse

1 declaration

valuereverse :: SNatI n => Vec n a -> Vec n a

Reverse Vec.

Example1 expression

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

Concatenation and splitting

5 declarations

value(++) :: SNatI n => Vec n a -> Vec m a -> Vec (Plus n m) a

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)

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

:: (SNatI m, SNatI n)
=> 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.

Example1 expression

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

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

concatMap id

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

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)

Folds

6 declarations

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

See Foldable.

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

See Foldable1.

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

See I.FoldableWithIndex.

valueifoldMap1

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

There is no type-class for this :(

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

Right fold.

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

Right fold with an index.

Special folds

4 declarations

valuelength :: SNatI n => Vec n a -> Int

Yield the length of a Vec. O(n)

valuenull :: SNatI n => Vec n a -> Bool

Test whether a Vec is empty. O(1)

valuesum :: (Num a, SNatI n) => Vec n a -> a

Non-strict sum.

valueproduct :: (Num a, SNatI n) => Vec n a -> a

Non-strict product.

Mapping

6 declarations

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

Example1 expression

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

valueimap :: SNatI n => (Fin n -> a -> b) -> Vec n a -> Vec n b

Example1 expression

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

valuetraverse :: (Applicative f, SNatI n) => (a -> f b) -> Vec n a -> f (Vec n b)

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

valuetraverse1

:: (Apply f, SNatI n)
=> a -> f b
-> Vec ('S n) a
-> f (Vec ('S n) b)

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

valueitraverse

:: (Applicative f, SNatI n)
=> 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.

valueitraverse_

:: (Applicative f, SNatI n)
=> 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

3 declarations

valuezipWith :: SNatI n => (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c

Zip two Vecs with a function.

valueizipWith

:: SNatI n
=> 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.

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

Repeat value

Example1 expression

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

Monadic

2 declarations

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

Monadic bind.

valuejoin :: SNatI n => Vec n (Vec n a) -> Vec n a

Monadic join.

Example1 expression

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

Universe

1 declaration

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

Get all Fin n in a Vec n.

Example1 expression

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

Extras

1 declaration

valueensureSpine :: SNatI n => Vec n a -> Vec n a

Ensure spine.

If we have an undefined Vec,

Example1 expression

>>> let v = error "err" :: Vec N.Nat3 Char

And insert data into it later:

Example1 expression

>>> let setHead :: a -> Vec ('S n) a -> Vec ('S n) a; setHead x (_ ::: xs) = x ::: xs

Then without a spine, it will fail:

Example1 expression

>>> head $ setHead 'x' v*** Exception: err...

But with the spine, it won't:

Example1 expression

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