Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
A variant of Data.Vec.Lazy with functions written using SNatI
.
The hypothesis is that these (goursive) functions could be fully unrolled,
if the Vec
size n
is known at compile time.
The module has the same API as Data.Vec.Lazy (sans withDict
and foldl'
).
Note: instance methods aren't changed, the Vec
type is the same.
Synopsis
- data Vec (n :: Nat) a where
- empty :: Vec 'Z a
- singleton :: a -> Vec ('S 'Z) a
- toPull :: forall n a. SNatI n => Vec n a -> Vec n a
- fromPull :: forall n a. SNatI n => Vec n a -> Vec n a
- toList :: forall n a. SNatI n => Vec n a -> [a]
- toNonEmpty :: forall n a. SNatI n => Vec ('S n) a -> NonEmpty a
- fromList :: SNatI n => [a] -> Maybe (Vec n a)
- fromListPrefix :: SNatI n => [a] -> Maybe (Vec n a)
- reifyList :: [a] -> (forall n. SNatI n => Vec n a -> r) -> r
- (!) :: SNatI n => 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 :: forall n a. SNatI n => Vec n a -> a -> Vec ('S n) a
- head :: Vec ('S n) a -> a
- last :: forall n a. SNatI n => Vec ('S n) a -> a
- tail :: Vec ('S n) a -> Vec n a
- init :: forall n a. SNatI n => Vec ('S n) a -> Vec n a
- (++) :: forall n m a. SNatI n => 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 :: forall a b n m. (SNatI m, SNatI n) => (a -> Vec m b) -> Vec n a -> Vec (Mult n m) b
- concat :: (SNatI m, SNatI n) => 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)
- reverse :: forall n a. SNatI n => Vec n a -> Vec n a
- foldMap :: (Monoid m, SNatI n) => (a -> m) -> Vec n a -> m
- foldMap1 :: forall s a n. (Semigroup s, SNatI n) => (a -> s) -> Vec ('S n) a -> s
- ifoldMap :: forall a n m. (Monoid m, SNatI n) => (Fin n -> a -> m) -> Vec n a -> m
- ifoldMap1 :: forall a n s. (Semigroup s, SNatI n) => (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s
- foldr :: forall a b n. SNatI n => (a -> b -> b) -> b -> Vec n a -> b
- ifoldr :: forall a b n. SNatI n => (Fin n -> a -> b -> b) -> b -> Vec n a -> b
- length :: forall n a. SNatI n => Vec n a -> Int
- null :: Vec n a -> Bool
- sum :: (Num a, SNatI n) => Vec n a -> a
- product :: (Num a, SNatI n) => Vec n a -> a
- map :: forall a b n. SNatI n => (a -> b) -> Vec n a -> Vec n b
- imap :: SNatI n => (Fin n -> a -> b) -> Vec n a -> Vec n b
- traverse :: forall n f a b. (Applicative f, SNatI n) => (a -> f b) -> Vec n a -> f (Vec n b)
- traverse1 :: forall n f a b. (Apply f, SNatI n) => (a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b)
- itraverse :: forall n f a b. (Applicative f, SNatI n) => (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
- itraverse_ :: forall n f a b. (Applicative f, SNatI n) => (Fin n -> a -> f b) -> Vec n a -> f ()
- zipWith :: forall a b c n. SNatI n => (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
- izipWith :: SNatI n => (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
- repeat :: SNatI n => x -> Vec n x
- bind :: SNatI n => Vec n a -> (a -> Vec n b) -> Vec n b
- join :: SNatI n => 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. SNatI n => Vec n a -> Vec n b) -> s -> t
- traverseWithVec :: Applicative f => (forall n. SNatI 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 => 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 => Representable (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 # 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 # | |
n ~ 'S m => Foldable1 (Vec n) Source # | |
Defined in Data.Vec.Lazy fold1 :: Semigroup m => Vec n m -> m # foldMap1 :: Semigroup m => (a -> m) -> Vec n a -> m # foldMap1' :: Semigroup m => (a -> m) -> Vec n a -> m # toNonEmpty :: Vec n a -> NonEmpty a # maximum :: Ord a => Vec n a -> a # minimum :: Ord a => Vec n a -> a # foldrMap1 :: (a -> b) -> (a -> b -> b) -> Vec n a -> b # foldlMap1' :: (a -> b) -> (b -> a -> b) -> Vec n a -> b # foldlMap1 :: (a -> b) -> (b -> a -> b) -> Vec n a -> b # foldrMap1' :: (a -> b) -> (a -> b -> b) -> Vec n a -> b # | |
Eq1 (Vec n) Source # | Since: 0.4 |
Ord1 (Vec n) Source # | Since: 0.4 |
Defined in Data.Vec.Lazy | |
Show1 (Vec n) Source # | Since: 0.4 |
Traversable (Vec n) Source # | |
SNatI n => Applicative (Vec n) Source # | |
Functor (Vec n) Source # | |
SNatI n => Monad (Vec n) Source # | |
SNatI n => Distributive (Vec n) Source # | |
Apply (Vec n) Source # | |
Bind (Vec n) Source # | |
n ~ 'S m => Traversable1 (Vec n) Source # | |
FoldableWithIndex (Fin n) (Vec n) Source # | Since: 0.4 |
Defined in Data.Vec.Lazy | |
FunctorWithIndex (Fin n) (Vec n) Source # | Since: 0.4 |
TraversableWithIndex (Fin n) (Vec n) Source # | Since: 0.4 |
Defined in Data.Vec.Lazy | |
(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 # | |
(SNatI n, Function a) => Function (Vec n a) Source # | |
(Monoid a, SNatI n) => Monoid (Vec n a) Source # | |
Semigroup a => Semigroup (Vec n a) Source # | |
Show a => Show (Vec n a) Source # | |
n ~ 'Z => Boring (Vec n a) Source # | Since: 0.4.1 |
Defined in Data.Vec.Lazy | |
NFData a => NFData (Vec n a) Source # | |
Defined in Data.Vec.Lazy | |
Eq a => Eq (Vec n a) Source # | |
Ord a => Ord (Vec n a) Source # | |
Hashable a => Hashable (Vec n a) Source # | |
Defined in Data.Vec.Lazy | |
type Rep (Vec n) Source # | |
Defined in Data.Vec.Lazy |
Construction
singleton :: a -> Vec ('S 'Z) a Source #
Vec
with exactly one element.
>>>
singleton True
True ::: VNil
Conversions
toList :: forall n a. SNatI n => Vec n a -> [a] Source #
Convert Vec
to list.
>>>
toList $ 'f' ::: 'o' ::: 'o' ::: VNil
"foo"
toNonEmpty :: forall n a. SNatI n => Vec ('S n) a -> NonEmpty a Source #
>>>
toNonEmpty $ 1 ::: 2 ::: 3 ::: VNil
1 :| [2,3]
Since: 0.4
fromListPrefix :: SNatI n => [a] -> Maybe (Vec n a) Source #
Convert list [a]
to
.
Returns Vec
n aNothing
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. SNatI n => Vec n a -> r) -> r Source #
Reify any list [a]
to
.Vec
n a
>>>
reifyList "foo" length
3
Indexing
(!) :: SNatI n => Vec n a -> Fin n -> a Source #
Indexing.
>>>
('a' ::: 'b' ::: 'c' ::: VNil) ! FS FZ
'b'
tabulate :: SNatI n => (Fin n -> a) -> Vec n a Source #
Tabulating, inverse of !
.
>>>
tabulate id :: Vec N.Nat3 (Fin N.Nat3)
0 ::: 1 ::: 2 ::: VNil
snoc :: forall n a. SNatI n => Vec n a -> a -> Vec ('S n) a Source #
Add a single element at the end of a Vec
.
Since: 0.2.1
Concatenation and splitting
(++) :: forall n m a. SNatI 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 :: SNatI 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. (SNatI m, SNatI n) => (a -> Vec m b) -> Vec n a -> Vec (Mult n m) b Source #
chunks :: (SNatI n, SNatI 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)
Reverse
Folds
foldMap1 :: forall s a n. (Semigroup s, SNatI n) => (a -> s) -> Vec ('S n) a -> s Source #
See Foldable1
.
ifoldMap :: forall a n m. (Monoid m, SNatI n) => (Fin n -> a -> m) -> Vec n a -> m Source #
See FoldableWithIndex
.
ifoldMap1 :: forall a n s. (Semigroup s, SNatI n) => (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s Source #
There is no type-class for this :(
ifoldr :: forall a b n. SNatI 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. SNatI n => (a -> b) -> Vec n a -> Vec n b Source #
>>>
map not $ True ::: False ::: VNil
False ::: True ::: VNil
imap :: SNatI 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, SNatI n) => (a -> f b) -> Vec n a -> f (Vec n b) Source #
traverse1 :: forall n f a b. (Apply f, SNatI n) => (a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b) Source #
itraverse :: forall n f a b. (Applicative f, SNatI n) => (Fin n -> a -> f b) -> Vec n a -> f (Vec n b) Source #
itraverse_ :: forall n f a b. (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
zipWith :: forall a b c n. SNatI n => (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c Source #
Zip two Vec
s with a function.
izipWith :: SNatI 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 :: SNatI n => x -> Vec n x Source #
Repeat value
>>>
repeat 'x' :: Vec N.Nat3 Char
'x' ::: 'x' ::: 'x' ::: VNil
Since: 0.2.1
Monadic
join :: SNatI n => Vec n (Vec n a) -> Vec n a Source #
Monadic join.
>>>
join $ ('a' ::: 'b' ::: VNil) ::: ('c' ::: 'd' ::: VNil) ::: VNil
'a' ::: 'd' ::: 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. SNatI n => Vec n a -> Vec n b) -> s -> t Source #
traverseWithVec :: Applicative f => (forall n. SNatI 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). SNatI n => Vec n a -> Vec n b) -> (a, a') -> (b, b') Source # traverseWithVec :: Applicative f => (forall (n :: Nat). SNatI 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). SNatI n => Vec n a -> Vec n b) -> (a, a2, a3) -> (b, b2, b3) Source # traverseWithVec :: Applicative f => (forall (n :: Nat). SNatI 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). SNatI n => Vec n a -> Vec n b) -> (a, a2, a3, a4) -> (b, b2, b3, b4) Source # traverseWithVec :: Applicative f => (forall (n :: Nat). SNatI n => Vec n a -> f (Vec n b)) -> (a, a2, a3, a4) -> f (b, b2, b3, b4) Source # |