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

Language | Haskell2010 |

Lazy (in elements and spine) length-indexed list: `Vec`

.

## Synopsis

- data Vec (n :: Nat) a where
- empty :: Vec Z a
- singleton :: a -> Vec (S Z) a
- withDict :: Vec n a -> (InlineInduction n => r) -> r
- toPull :: Vec n a -> Vec n a
- fromPull :: forall n a. SNatI n => Vec n a -> Vec n a
- toList :: Vec n a -> [a]
- fromList :: SNatI n => [a] -> Maybe (Vec n a)
- fromListPrefix :: SNatI n => [a] -> Maybe (Vec n a)
- reifyList :: [a] -> (forall n. InlineInduction n => Vec n a -> r) -> r
- (!) :: Vec n a -> Fin n -> a
- tabulate :: SNatI n => (Fin n -> a) -> Vec n a
- cons :: a -> Vec n a -> Vec (S n) a
- snoc :: Vec n a -> a -> Vec (S n) a
- head :: Vec (S n) a -> a
- tail :: Vec (S n) a -> Vec n a
- reverse :: Vec n a -> Vec n a
- (++) :: Vec n a -> Vec m a -> Vec (Plus n m) a
- split :: SNatI n => Vec (Plus n m) a -> (Vec n a, Vec m a)
- concatMap :: (a -> Vec m b) -> Vec n a -> Vec (Mult n m) b
- concat :: Vec n (Vec m a) -> Vec (Mult n m) a
- chunks :: (SNatI n, SNatI m) => Vec (Mult n m) a -> Vec n (Vec m a)
- foldMap :: Monoid m => (a -> m) -> Vec n a -> m
- foldMap1 :: Semigroup s => (a -> s) -> Vec (S n) a -> s
- ifoldMap :: Monoid m => (Fin n -> a -> m) -> Vec n a -> m
- ifoldMap1 :: Semigroup s => (Fin (S n) -> a -> s) -> Vec (S n) a -> s
- foldr :: forall a b n. (a -> b -> b) -> b -> Vec n a -> b
- ifoldr :: forall a b n. (Fin n -> a -> b -> b) -> b -> Vec n a -> b
- foldl' :: forall a b n. (b -> a -> b) -> b -> Vec n a -> b
- length :: Vec n a -> Int
- null :: Vec n a -> Bool
- sum :: Num a => Vec n a -> a
- product :: Num a => Vec n a -> a
- map :: (a -> b) -> Vec n a -> Vec n b
- imap :: (Fin n -> a -> b) -> Vec n a -> Vec n b
- traverse :: forall n f a b. Applicative f => (a -> f b) -> Vec n a -> f (Vec n b)
- traverse1 :: forall n f a b. Apply f => (a -> f b) -> Vec (S n) a -> f (Vec (S n) b)
- itraverse :: Applicative f => (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
- itraverse_ :: Applicative f => (Fin n -> a -> f b) -> Vec n a -> f ()
- zipWith :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
- izipWith :: (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
- repeat :: SNatI n => x -> Vec n x
- bind :: Vec n a -> (a -> Vec n b) -> Vec n b
- join :: Vec n (Vec n a) -> Vec n a
- universe :: SNatI n => Vec n (Fin n)
- class VecEach s t a b | s -> a, t -> b, s b -> t, t a -> s where
- mapWithVec :: (forall n. InlineInduction n => Vec n a -> Vec n b) -> s -> t
- traverseWithVec :: Applicative f => (forall n. InlineInduction n => Vec n a -> f (Vec n b)) -> s -> f t

# Documentation

data Vec (n :: Nat) a where Source #

Vector, i.e. length-indexed list.

## Instances

SNatI n => Monad (Vec n) Source # | |

Functor (Vec n) Source # | |

SNatI n => Applicative (Vec n) Source # | |

Foldable (Vec n) Source # | |

Defined in Data.Vec.Lazy 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 # elem :: Eq a => a -> Vec n a -> Bool # maximum :: Ord a => Vec n a -> a # minimum :: Ord a => Vec n a -> a # | |

Traversable (Vec n) Source # | |

SNatI n => Arbitrary1 (Vec n) Source # | |

Defined in Data.Vec.Lazy liftArbitrary :: Gen a -> Gen (Vec n a) # liftShrink :: (a -> [a]) -> Vec n a -> [Vec n a] # | |

SNatI n => Distributive (Vec n) Source # | |

SNatI n => Representable (Vec n) Source # | |

n ~ S m => Traversable1 (Vec n) Source # | |

n ~ S m => Foldable1 (Vec n) Source # | |

Apply (Vec n) Source # | |

Bind (Vec n) Source # | |

Eq a => Eq (Vec n a) Source # | |

Ord a => Ord (Vec n a) Source # | |

Show a => Show (Vec n a) Source # | |

Semigroup a => Semigroup (Vec n a) Source # | |

(Monoid a, SNatI n) => Monoid (Vec n a) Source # | |

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

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

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

Defined in Data.Vec.Lazy coarbitrary :: Vec n a -> Gen b -> Gen b # | |

NFData a => NFData (Vec n a) Source # | |

Defined in Data.Vec.Lazy | |

Hashable a => Hashable (Vec n a) Source # | |

Defined in Data.Vec.Lazy | |

type Rep (Vec n) Source # | |

Defined in Data.Vec.Lazy |

# Construction

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

*O(n)*. Recover `InlineInduction`

(and `SNatI`

) dictionary from a `Vec`

value.

Example: `reflect`

is constrained with

, but if we have a
`SNatI`

n

, we can recover that dictionary:`Vec`

n a

`>>>`

1`let f :: forall n a. Vec n a -> N.Nat; f v = withDict v (N.reflect (Proxy :: Proxy n)) in f (True ::: VNil)`

*Note:* using `InlineInduction`

will be suboptimal, as if GHC has no
opportunity to optimise the code, the recusion won't be unfold.
How bad such code will perform? I don't know, we'll need benchmarks.

# Conversions

toList :: Vec n a -> [a] Source #

Convert `Vec`

to list.

`>>>`

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

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

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

Tabulating, inverse of `!`

.

`>>>`

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

# Reverse

# Concatenation and splitting

(++) :: 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 :: SNatI 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))`

chunks :: (SNatI n, SNatI 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

ifoldMap1 :: Semigroup s => (Fin (S n) -> a -> s) -> Vec (S n) a -> s Source #

There is no type-class for this :(

ifoldr :: forall a b n. (Fin n -> a -> b -> b) -> b -> Vec n a -> b Source #

Right fold with an index.

# Special folds

# Mapping

map :: (a -> b) -> Vec n a -> Vec n b Source #

`>>>`

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

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

`>>>`

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

itraverse_ :: Applicative f => (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

izipWith :: (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 :: SNatI n => x -> Vec n x Source #

Repeat a value.

`>>>`

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

*Since: 0.2.1*

# Monadic

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

Monadic join.

`>>>`

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

# Universe

# VecEach

class VecEach s t a b | s -> a, t -> b, s b -> t, t a -> s where Source #

Write functions on `Vec`

. Use them with tuples.

`VecEach`

can be used to avoid "this function won't change the length of the
list" in DSLs.

**bad:** Instead of

[x, y] <- badDslMagic ["foo", "bar"] -- list!

**good:** we can write

(x, y) <- betterDslMagic ("foo", "bar") -- homogenic tuple!

where `betterDslMagic`

can be defined using `traverseWithVec`

.

Moreally `lens`

`Each`

should be a superclass, but
there's no strict need for it.

mapWithVec :: (forall n. InlineInduction n => Vec n a -> Vec n b) -> s -> t Source #

traverseWithVec :: Applicative f => (forall n. InlineInduction n => Vec n a -> f (Vec n b)) -> s -> f t Source #

## Instances

(a ~ a', b ~ b') => VecEach (a, a') (b, b') a b Source # | |

Defined in Data.Vec.Lazy mapWithVec :: (forall (n :: Nat). InlineInduction n => Vec n a -> Vec n b) -> (a, a') -> (b, b') Source # traverseWithVec :: Applicative f => (forall (n :: Nat). InlineInduction n => Vec n a -> f (Vec n b)) -> (a, a') -> f (b, b') Source # | |

(a ~ a2, a ~ a3, b ~ b2, b ~ b3) => VecEach (a, a2, a3) (b, b2, b3) a b Source # | |

Defined in Data.Vec.Lazy mapWithVec :: (forall (n :: Nat). InlineInduction n => Vec n a -> Vec n b) -> (a, a2, a3) -> (b, b2, b3) Source # traverseWithVec :: Applicative f => (forall (n :: Nat). InlineInduction n => Vec n a -> f (Vec n b)) -> (a, a2, a3) -> f (b, b2, b3) Source # | |

(a ~ a2, a ~ a3, a ~ a4, b ~ b2, b ~ b3, b ~ b4) => VecEach (a, a2, a3, a4) (b, b2, b3, b4) a b Source # | |

Defined in Data.Vec.Lazy mapWithVec :: (forall (n :: Nat). InlineInduction n => Vec n a -> Vec n b) -> (a, a2, a3, a4) -> (b, b2, b3, b4) Source # traverseWithVec :: Applicative f => (forall (n :: Nat). InlineInduction n => Vec n a -> f (Vec n b)) -> (a, a2, a3, a4) -> f (b, b2, b3, b4) Source # |