Safe Haskell | None |
---|---|

Language | Haskell2010 |

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
- toList :: forall n a. InlineInduction n => Vec n a -> [a]
- fromList :: InlineInduction n => [a] -> Maybe (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
- tabulate :: InlineInduction n => (Fin n -> a) -> Vec n a
- cons :: a -> Vec n a -> Vec (S n) a
- snoc :: forall n a. InlineInduction n => Vec n a -> a -> Vec (S n) a
- head :: Vec (S n) a -> a
- tail :: Vec (S n) a -> Vec n a
- reverse :: forall n a. InlineInduction n => Vec 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
- repeat :: InlineInduction n => x -> Vec n x
- 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

# Construction

# Conversions

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

Convert `Vec`

to list.

`>>>`

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

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

Convert list `[a]`

to

.
Returns `Vec`

n a`Nothing`

if input list is too short.

`>>>`

Just ('f' ::: 'o' ::: 'o' ::: VNil)`fromListPrefix "foo" :: Maybe (Vec N.Nat3 Char)`

`>>>`

Just ('q' ::: 'u' ::: 'u' ::: VNil)`fromListPrefix "quux" :: Maybe (Vec N.Nat3 Char)`

`>>>`

Nothing`fromListPrefix "xy" :: Maybe (Vec N.Nat3 Char)`

reifyList :: [a] -> (forall n. InlineInduction n => Vec n a -> r) -> r Source #

Reify any list `[a]`

to

.`Vec`

n a

`>>>`

3`reifyList "foo" length`

# Indexing

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

Indexing.

`>>>`

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

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

Tabulating, inverse of `!`

.

`>>>`

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

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`

.

# Reverse

# 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' ::: 'c' ::: 'd' ::: VNil`('a' ::: 'b' ::: VNil) ++ ('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 `++`

.

`>>>`

('a' ::: VNil,'b' ::: 'c' ::: VNil)`split ('a' ::: 'b' ::: 'c' ::: VNil) :: (Vec N.Nat1 Char, Vec N.Nat2 Char)`

`>>>`

'a' ::: 'b' ::: 'c' ::: VNil`uncurry (++) (split ('a' ::: 'b' ::: 'c' ::: VNil) :: (Vec N.Nat1 Char, Vec N.Nat2 Char))`

concatMap :: forall a b n m. (InlineInduction m, InlineInduction n) => (a -> Vec m b) -> Vec n a -> Vec (Mult n m) b Source #

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

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

Inverse of `concat`

.

`>>>`

Just ((1 ::: 2 ::: 3 ::: VNil) ::: (4 ::: 5 ::: 6 ::: VNil) ::: VNil)`chunks <$> fromListPrefix [1..] :: Maybe (Vec N.Nat2 (Vec N.Nat3 Int))`

`>>>`

`let idVec x = x :: Vec N.Nat2 (Vec N.Nat3 Int)`

`>>>`

Just (1 ::: 2 ::: 3 ::: 4 ::: 5 ::: 6 ::: VNil)`concat . idVec . chunks <$> fromListPrefix [1..]`

# Folds

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

# Mapping

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

`>>>`

False ::: True ::: VNil`map not $ True ::: False ::: VNil`

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

`>>>`

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

traverse :: forall n f a b. (Applicative f, InlineInduction n) => (a -> f b) -> Vec n a -> f (Vec n b) Source #

traverse1 :: forall n f a b. (Apply f, InlineInduction n) => (a -> f b) -> Vec (S n) a -> f (Vec (S n) b) Source #

itraverse :: forall n f a b. (Applicative f, InlineInduction n) => (Fin n -> a -> f b) -> Vec n a -> f (Vec n b) Source #

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 `Vec`

s with a function.

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

Zip two `Vec`

s. with a function that also takes the elements' indices.

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

Repeat value

`>>>`

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

*Since: 0.2.1*

# Monadic

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

Monadic join.

`>>>`

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

# Universe

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

`>>>`

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

But with the spine, it won't:

`>>>`

'x'`head $ setHead 'x' $ ensureSpine v`