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

Contents

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

Synopsis

data family Vec
constructor :::
constructor VNil
value empty
value singleton
value toPull
value fromPull
value toList
value toNonEmpty
value fromList
value fromListPrefix
value reifyList
value !
value tabulate
value cons
value snoc
value head
value last
value tail
value init
value reverse
value ++
value split
value concatMap
value concat
value chunks
value foldMap
value foldMap1
value ifoldMap
value ifoldMap1
value foldr
value ifoldr
value length
value null
value sum
value product
value map
value imap
value traverse
value traverse1
value itraverse
value itraverse_
value zipWith
value izipWith
value repeat
value bind
value join
value universe
value ensureSpine

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

data familydata family Vec (n :: Nat) a

Source#

Vector, i.e. length-indexed list.

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

SNatI n => Monad (Vec n)Defined in vec-0.5.1.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => Functor (Vec n)Defined in vec-0.5.1.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => Applicative (Vec n)Defined in vec-0.5.1.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => Foldable (Vec n)Defined in vec-0.5.1.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => Traversable (Vec n)Defined in vec-0.5.1.1 · Data.Vec.DataFamily.SpineStrict
(SNatI m, n ~ 'S m) => Foldable1 (Vec n)Defined in vec-0.5.1.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => Eq1 (Vec n)Defined in vec-0.5.1.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => Ord1 (Vec n)Defined in vec-0.5.1.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => Show1 (Vec n)Defined in vec-0.5.1.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => Arbitrary1 (Vec n)Defined in vec-0.5.1.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => Distributive (Vec n)Defined in vec-0.5.1.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => Apply (Vec n)Defined in vec-0.5.1.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => Bind (Vec n)Defined in vec-0.5.1.1 · Data.Vec.DataFamily.SpineStrict
(SNatI m, n ~ 'S m) => Traversable1 (Vec n)Defined in vec-0.5.1.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => Representable (Vec n)Defined in vec-0.5.1.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => FoldableWithIndex (Fin n) (Vec n)Defined in vec-0.5.1.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => FunctorWithIndex (Fin n) (Vec n)Defined in vec-0.5.1.1 · Data.Vec.DataFamily.SpineStrict
SNatI n => TraversableWithIndex (Fin n) (Vec n)Defined in vec-0.5.1.1 · Data.Vec.DataFamily.SpineStrict
(Eq a, SNatI n) => Eq (Vec n a)Defined in vec-0.5.1.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.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.1 · Data.Vec.DataFamily.SpineStrict
(Semigroup a, SNatI n) => Semigroup (Vec n a)Defined in vec-0.5.1.1 · Data.Vec.DataFamily.SpineStrict
(Monoid a, SNatI n) => Monoid (Vec n a)Defined in vec-0.5.1.1 · Data.Vec.DataFamily.SpineStrict
(NFData a, SNatI n) => NFData (Vec n a)Defined in vec-0.5.1.1 · Data.Vec.DataFamily.SpineStrict
(SNatI n, Arbitrary a) => Arbitrary (Vec n a)Defined in vec-0.5.1.1 · Data.Vec.DataFamily.SpineStrict
(SNatI n, CoArbitrary a) => CoArbitrary (Vec n a)Defined in vec-0.5.1.1 · Data.Vec.DataFamily.SpineStrict
(SNatI n, Function a) => Function (Vec n a)Defined in vec-0.5.1.1 · Data.Vec.DataFamily.SpineStrict
(Hashable a, SNatI n) => Hashable (Vec n a)Defined in vec-0.5.1.1 · Data.Vec.DataFamily.SpineStrict
type Rep (Vec n) = Fin nDefined in vec-0.5.1.1 · Data.Vec.DataFamily.SpineStrict
data Vec 'Z
- VNil
Defined in vec-0.5.1.1 · Data.Vec.DataFamily.SpineStrict
data Vec ('S n)
- a ::: Vec n a
Defined in vec-0.5.1.1 · Data.Vec.DataFamily.SpineStrict

constructora ::: Vec n a

constructorVNil

Construction

valueempty :: Vec 'Z a

Source#

Empty Vec.

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

Source#

Vec with exactly one element.

Example1 expression

>>> singleton TrueTrue ::: VNil

Conversions

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

Source#

Convert to pull Vec.

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

Source#

Convert from pull Vec.

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

Source#

Convert Vec to list.

Example1 expression

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

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

Source#

Example1 expression

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

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

Source#

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)

Source#

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

Source#

Reify any list [a] to Vec n a.

Example1 expression

>>> reifyList "foo" length3

Indexing

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

Source#

Indexing.

Example1 expression

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

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

Source#

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

Source#

Cons an element in front of a Vec.

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

Source#

Add a single element at the end of a Vec.

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

Source#

The first element of a Vec.

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

Source#

The last element of a Vec.

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

Source#

The elements after the head of a Vec.

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

Source#

The elements before the last of a Vec.

Reverse

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

Source#

Reverse Vec.

Example1 expression

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

Concatenation and splitting

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

Source#

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)

Source#

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

Source#

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

Source#

concatMap id

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

Source#

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

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

Source#

See Foldable.

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

Source#

See Foldable1.

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

Source#

See I.FoldableWithIndex.

valueifoldMap1

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

Source#

There is no type-class for this :(

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

Source#

Right fold.

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

Source#

Right fold with an index.

Special folds

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

Source#

Yield the length of a Vec. O(n)

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

Source#

Test whether a Vec is empty. O(1)

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

Source#

Non-strict sum.

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

Source#

Non-strict product.

Mapping

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

Source#

Example1 expression

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

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

Source#

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)

Source#

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)

Source#

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)

Source#

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

Source#

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

Zipping

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

Source#

Zip two Vecs with a function.

valueizipWith

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

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

Source#

Repeat value

Example1 expression

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

Monadic

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

Source#

Monadic bind.

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

Source#

Monadic join.

Example1 expression

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

Universe

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

Source#

Get all Fin n in a Vec n.

Example1 expression

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

Extras

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

Source#

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'