-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Vec: length-indexed (sized) list -- -- This package provides length-indexed (sized) lists, also known as -- vectors. -- -- 
--   data Vec n a where
--       VNil  :: Vec 'Nat.Z a
--       (:::) :: a -> Vec n a -> Vec ('Nat.S n) a
--
-- -- The functions are implemented in four flavours: -- -- -- -- As best approach depends on the application, vec doesn't do -- any magic transformation. Benchmark your code. -- -- This package uses fin, i.e. not GHC.TypeLits, for -- indexes. -- -- For lens or optics support see vec-lens and -- vec-optics packages respectively. -- -- See Hasochism: the pleasure and pain of dependently typed haskell -- programming by Sam Lindley and Conor McBride for answers to -- how and why. Read APLicative Programming with -- Naperian Functors by Jeremy Gibbons for (not so) different ones. -- --

Similar packages

-- -- @package vec @version 0.5.1 -- | Pull/representable Vec n a = Fin n -> a. -- -- The module tries to have same API as Data.Vec.Lazy, missing -- bits: withDict, toPull, fromPull, -- traverse (and variants), (++), concat and -- split. module Data.Vec.Pull -- | Easily fuseable Vec. -- -- It on purpose doesn't have bad (fusion-wise) instances, like -- Traversable. Generally, there aren't functions which would be -- bad consumers or bad producers. newtype Vec n a Vec :: (Fin n -> a) -> Vec n a [unVec] :: Vec n a -> Fin n -> a -- | Empty Vec. empty :: Vec 'Z a -- | Vec with exactly one element. -- -- 
--   >>> L.fromPull $ singleton True
--   True ::: VNil
--
singleton :: a -> Vec ('S 'Z) a -- | Convert Vec to list. toList :: SNatI n => Vec n a -> [a] -- | Convert Vec to NonEmpty. toNonEmpty :: SNatI n => Vec ('S n) a -> NonEmpty a -- | Convert list [a] to Vec n a. Returns -- Nothing if lengths don't match exactly. -- -- 
--   >>> L.fromPull <$> fromList "foo" :: Maybe (L.Vec N.Nat3 Char)
--   Just ('f' ::: 'o' ::: 'o' ::: VNil)
--
-- -- 
--   >>> L.fromPull <$> fromList "quux" :: Maybe (L.Vec N.Nat3 Char)
--   Nothing
--
-- -- 
--   >>> L.fromPull <$> fromList "xy" :: Maybe (L.Vec N.Nat3 Char)
--   Nothing
--
fromList :: SNatI n => [a] -> Maybe (Vec n a) -- | Convert list [a] to Vec n a. Returns -- Nothing if input list is too short. -- -- 
--   >>> L.fromPull <$> fromListPrefix "foo" :: Maybe (L.Vec N.Nat3 Char)
--   Just ('f' ::: 'o' ::: 'o' ::: VNil)
--
-- -- 
--   >>> L.fromPull <$> fromListPrefix "quux" :: Maybe (L.Vec N.Nat3 Char)
--   Just ('q' ::: 'u' ::: 'u' ::: VNil)
--
-- -- 
--   >>> L.fromPull <$> fromListPrefix "xy" :: Maybe (L.Vec N.Nat3 Char)
--   Nothing
--
fromListPrefix :: SNatI n => [a] -> Maybe (Vec n a) -- | Reify any list [a] to Vec n a. -- -- 
--   >>> reifyList "foo" length
--   3
--
reifyList :: [a] -> (forall n. SNatI n => Vec n a -> r) -> r -- | Indexing. (!) :: Vec n a -> Fin n -> a tabulate :: (Fin n -> a) -> Vec n a -- | Cons an element in front of a Vec. cons :: a -> Vec n a -> Vec ('S n) a -- | Add a single element at the end of a Vec. snoc :: forall a n. SNatI n => Vec n a -> a -> Vec ('S n) a -- | The first element of a Vec. head :: Vec ('S n) a -> a -- | The last element of a Vec. last :: forall n a. SNatI n => Vec ('S n) a -> a -- | The elements after the head of a Vec. tail :: Vec ('S n) a -> Vec n a -- | The elements before the last of a Vec. init :: forall n a. SNatI n => Vec ('S n) a -> Vec n a -- | Reverse Vec. reverse :: forall n a. SNatI n => Vec n a -> Vec n a -- | See Foldable. foldMap :: (Monoid m, SNatI n) => (a -> m) -> Vec n a -> m -- | See Foldable1. foldMap1 :: (Semigroup s, SNatI n) => (a -> s) -> Vec ('S n) a -> s -- | See FoldableWithIndex. ifoldMap :: (Monoid m, SNatI n) => (Fin n -> a -> m) -> Vec n a -> m -- | There is no type-class for this :( ifoldMap1 :: (Semigroup s, SNatI n) => (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s -- | Right fold. foldr :: SNatI n => (a -> b -> b) -> b -> Vec n a -> b -- | Right fold with an index. ifoldr :: SNatI n => (Fin n -> a -> b -> b) -> b -> Vec n a -> b -- | Strict left fold. foldl' :: SNatI n => (b -> a -> b) -> b -> Vec n a -> b -- | Yield the length of a Vec. length :: forall n a. SNatI n => Vec n a -> Int -- | Test whether a Vec is empty. null :: forall n a. SNatI n => Vec n a -> Bool -- | Strict sum. sum :: (Num a, SNatI n) => Vec n a -> a -- | Strict product. product :: (Num a, SNatI n) => Vec n a -> a -- | 
--   >>> L.fromPull $ map not $ L.toPull $ True L.::: False L.::: L.VNil
--   False ::: True ::: VNil
--
map :: (a -> b) -> Vec n a -> Vec n b -- | 
--   >>> L.fromPull $ imap (,) $ L.toPull $ 'a' L.::: 'b' L.::: 'c' L.::: L.VNil
--   (0,'a') ::: (1,'b') ::: (2,'c') ::: VNil
--
imap :: (Fin n -> a -> b) -> Vec n a -> Vec n b -- | Zip two Vecs with a function. zipWith :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c -- | Zip two Vecs. with a function that also takes the elements' -- indices. izipWith :: (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c -- | Repeat value repeat :: x -> Vec n x -- | Monadic bind. bind :: Vec n a -> (a -> Vec n b) -> Vec n b -- | Monadic join. join :: Vec n (Vec n a) -> Vec n a -- | Get all Fin n in a Vec n. -- -- 
--   >>> L.fromPull (universe :: Vec N.Nat3 (Fin N.Nat3))
--   0 ::: 1 ::: 2 ::: VNil
--
universe :: SNatI n => Vec n (Fin n) instance (GHC.Classes.Eq a, Data.Type.Nat.SNatI n) => GHC.Classes.Eq (Data.Vec.Pull.Vec n a) instance GHC.Base.Functor (Data.Vec.Pull.Vec n) instance Data.Type.Nat.SNatI n => Data.Foldable.Foldable (Data.Vec.Pull.Vec n) instance WithIndex.FunctorWithIndex (Data.Fin.Fin n) (Data.Vec.Pull.Vec n) instance Data.Type.Nat.SNatI n => WithIndex.FoldableWithIndex (Data.Fin.Fin n) (Data.Vec.Pull.Vec n) instance (Data.Type.Nat.SNatI m, (n :: Data.Nat.Nat) GHC.Types.~ ('Data.Nat.S m :: Data.Nat.Nat)) => Data.Foldable1.Foldable1 (Data.Vec.Pull.Vec n) instance GHC.Base.Applicative (Data.Vec.Pull.Vec n) instance GHC.Base.Monad (Data.Vec.Pull.Vec n) instance Data.Distributive.Distributive (Data.Vec.Pull.Vec n) instance Data.Functor.Rep.Representable (Data.Vec.Pull.Vec n) instance GHC.Base.Semigroup a => GHC.Base.Semigroup (Data.Vec.Pull.Vec n a) instance GHC.Base.Monoid a => GHC.Base.Monoid (Data.Vec.Pull.Vec n a) instance Data.Functor.Bind.Class.Apply (Data.Vec.Pull.Vec n) instance Data.Functor.Bind.Class.Bind (Data.Vec.Pull.Vec n) instance ((n :: Data.Nat.Nat) GHC.Types.~ ('Data.Nat.Z :: Data.Nat.Nat)) => Data.Boring.Boring (Data.Vec.Pull.Vec n a) -- | 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
--
module Data.Vec.DataFamily.SpineStrict -- | Vector, i.e. length-indexed list. data family Vec (n :: Nat) a infixr 5 ::: -- | Empty Vec. empty :: Vec 'Z a -- | Vec with exactly one element. -- -- 
--   >>> singleton True
--   True ::: VNil
--
singleton :: a -> Vec ('S 'Z) a -- | Convert to pull Vec. toPull :: forall n a. SNatI n => Vec n a -> Vec n a -- | Convert from pull Vec. fromPull :: forall n a. SNatI n => Vec n a -> Vec n a -- | Convert Vec to list. -- -- 
--   >>> toList $ 'f' ::: 'o' ::: 'o' ::: VNil
--   "foo"
--
toList :: forall n a. SNatI n => Vec n a -> [a] -- | 
--   >>> toNonEmpty $ 1 ::: 2 ::: 3 ::: VNil
--   1 :| [2,3]
--
toNonEmpty :: forall n a. SNatI n => Vec ('S n) a -> NonEmpty a -- | Convert list [a] to Vec n a. Returns -- Nothing if lengths don't match exactly. -- -- 
--   >>> fromList "foo" :: Maybe (Vec N.Nat3 Char)
--   Just ('f' ::: 'o' ::: 'o' ::: VNil)
--
-- -- 
--   >>> fromList "quux" :: Maybe (Vec N.Nat3 Char)
--   Nothing
--
-- -- 
--   >>> fromList "xy" :: Maybe (Vec N.Nat3 Char)
--   Nothing
--
fromList :: SNatI n => [a] -> Maybe (Vec n a) -- | Convert list [a] to Vec n a. Returns -- Nothing 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
--
fromListPrefix :: SNatI n => [a] -> Maybe (Vec n a) -- | Reify any list [a] to Vec n a. -- -- 
--   >>> reifyList "foo" length
--   3
--
reifyList :: [a] -> (forall n. SNatI n => Vec n a -> r) -> r -- | Indexing. -- -- 
--   >>> ('a' ::: 'b' ::: 'c' ::: VNil) ! FS FZ
--   'b'
--
(!) :: SNatI n => Vec n a -> Fin n -> a -- | Tabulating, inverse of !. -- -- 
--   >>> tabulate id :: Vec N.Nat3 (Fin N.Nat3)
--   0 ::: 1 ::: 2 ::: VNil
--
tabulate :: SNatI n => (Fin n -> a) -> Vec n a -- | Cons an element in front of a Vec. cons :: a -> Vec n a -> Vec ('S n) a -- | Add a single element at the end of a Vec. snoc :: forall n a. SNatI n => Vec n a -> a -> Vec ('S n) a -- | The first element of a Vec. head :: Vec ('S n) a -> a -- | The last element of a Vec. last :: forall n a. SNatI n => Vec ('S n) a -> a -- | The elements after the head of a Vec. tail :: Vec ('S n) a -> Vec n a -- | The elements before the last of a Vec. init :: forall n a. SNatI n => Vec ('S n) a -> Vec n a -- | Reverse Vec. -- -- 
--   >>> reverse ('a' ::: 'b' ::: 'c' ::: VNil)
--   'c' ::: 'b' ::: 'a' ::: VNil
--
reverse :: forall n a. SNatI n => Vec n a -> Vec n a -- | Append two Vec. -- -- 
--   >>> ('a' ::: 'b' ::: VNil) ++ ('c' ::: 'd' ::: VNil)
--   'a' ::: 'b' ::: 'c' ::: 'd' ::: VNil
--
(++) :: forall n m a. SNatI n => Vec n a -> Vec m a -> Vec (Plus n m) a infixr 5 ++ -- | 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
--
split :: SNatI n => Vec (Plus n m) a -> (Vec n a, Vec m a) -- | Map over all the elements of a Vec and concatenate the -- resulting Vecs. -- -- 
--   >>> concatMap (\x -> x ::: x ::: VNil) ('a' ::: 'b' ::: VNil)
--   'a' ::: 'a' ::: 'b' ::: 'b' ::: VNil
--
concatMap :: forall a b n m. (SNatI m, SNatI n) => (a -> Vec m b) -> Vec n a -> Vec (Mult n m) b -- | 
--   concatMap id
--
concat :: (SNatI m, SNatI n) => Vec n (Vec m a) -> Vec (Mult n m) a -- | 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)
--
chunks :: (SNatI n, SNatI m) => Vec (Mult n m) a -> Vec n (Vec m a) -- | See Foldable. foldMap :: (Monoid m, SNatI n) => (a -> m) -> Vec n a -> m -- | See Foldable1. foldMap1 :: forall s a n. (Semigroup s, SNatI n) => (a -> s) -> Vec ('S n) a -> s -- | See FoldableWithIndex. ifoldMap :: forall a n m. (Monoid m, SNatI n) => (Fin n -> a -> m) -> Vec n a -> m -- | There is no type-class for this :( ifoldMap1 :: forall a n s. (Semigroup s, SNatI n) => (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s -- | Right fold. foldr :: forall a b n. SNatI n => (a -> b -> b) -> b -> Vec n a -> b -- | Right fold with an index. ifoldr :: forall a b n. SNatI n => (Fin n -> a -> b -> b) -> b -> Vec n a -> b -- | Yield the length of a Vec. O(n) length :: forall n a. SNatI n => Vec n a -> Int -- | Test whether a Vec is empty. O(1) null :: forall n a. SNatI n => Vec n a -> Bool -- | Non-strict sum. sum :: (Num a, SNatI n) => Vec n a -> a -- | Non-strict product. product :: (Num a, SNatI n) => Vec n a -> a -- | 
--   >>> map not $ True ::: False ::: VNil
--   False ::: True ::: VNil
--
map :: forall a b n. SNatI n => (a -> b) -> Vec n a -> Vec n b -- | 
--   >>> imap (,) $ 'a' ::: 'b' ::: 'c' ::: VNil
--   (0,'a') ::: (1,'b') ::: (2,'c') ::: VNil
--
imap :: SNatI n => (Fin n -> a -> b) -> Vec n a -> Vec n b -- | Apply an action to every element of a Vec, yielding a -- Vec of results. traverse :: forall n f a b. (Applicative f, SNatI n) => (a -> f b) -> Vec n a -> f (Vec n b) -- | Apply an action to non-empty Vec, yielding a Vec of -- results. traverse1 :: forall n f a b. (Apply f, SNatI n) => (a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b) -- | Apply an action to every element of a Vec and its index, -- yielding a Vec of results. itraverse :: forall n f a b. (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, -- ignoring the results. itraverse_ :: forall n f a b. (Applicative f, SNatI n) => (Fin n -> a -> f b) -> Vec n a -> f () -- | Zip two Vecs with a function. zipWith :: forall a b c n. SNatI 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. izipWith :: SNatI n => (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c -- | Repeat value -- -- 
--   >>> repeat 'x' :: Vec N.Nat3 Char
--   'x' ::: 'x' ::: 'x' ::: VNil
--
repeat :: SNatI n => x -> Vec n x -- | Monadic bind. bind :: SNatI n => Vec n a -> (a -> Vec n b) -> Vec n b -- | Monadic join. -- -- 
--   >>> join $ ('a' ::: 'b' ::: VNil) ::: ('c' ::: 'd' ::: VNil) ::: VNil
--   'a' ::: 'd' ::: VNil
--
join :: SNatI n => Vec n (Vec n a) -> Vec n a -- | Get all Fin n in a Vec n. -- -- 
--   >>> universe :: Vec N.Nat3 (Fin N.Nat3)
--   0 ::: 1 ::: 2 ::: VNil
--
universe :: SNatI n => Vec n (Fin n) -- | 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: -- -- 
--   >>> head $ setHead 'x' v
--   *** Exception: err
--   ...
--
-- -- But with the spine, it won't: -- -- 
--   >>> head $ setHead 'x' $ ensureSpine v
--   'x'
--
ensureSpine :: SNatI n => Vec n a -> Vec n a instance (Data.Hashable.Class.Hashable a, Data.Type.Nat.SNatI n) => Data.Hashable.Class.Hashable (Data.Vec.DataFamily.SpineStrict.Vec n a) instance (Control.DeepSeq.NFData a, Data.Type.Nat.SNatI n) => Control.DeepSeq.NFData (Data.Vec.DataFamily.SpineStrict.Vec n a) instance (GHC.Show.Show a, Data.Type.Nat.SNatI n) => GHC.Show.Show (Data.Vec.DataFamily.SpineStrict.Vec n a) instance Data.Type.Nat.SNatI n => Data.Functor.Classes.Show1 (Data.Vec.DataFamily.SpineStrict.Vec n) instance (GHC.Classes.Ord a, Data.Type.Nat.SNatI n) => GHC.Classes.Ord (Data.Vec.DataFamily.SpineStrict.Vec n a) instance Data.Type.Nat.SNatI n => Data.Functor.Classes.Ord1 (Data.Vec.DataFamily.SpineStrict.Vec n) instance (GHC.Classes.Eq a, Data.Type.Nat.SNatI n) => GHC.Classes.Eq (Data.Vec.DataFamily.SpineStrict.Vec n a) instance Data.Type.Nat.SNatI n => Data.Functor.Classes.Eq1 (Data.Vec.DataFamily.SpineStrict.Vec n) instance Data.Type.Nat.SNatI n => GHC.Base.Functor (Data.Vec.DataFamily.SpineStrict.Vec n) instance Data.Type.Nat.SNatI n => Data.Foldable.Foldable (Data.Vec.DataFamily.SpineStrict.Vec n) instance (Data.Type.Nat.SNatI m, (n :: Data.Nat.Nat) GHC.Types.~ ('Data.Nat.S m :: Data.Nat.Nat)) => Data.Foldable1.Foldable1 (Data.Vec.DataFamily.SpineStrict.Vec n) instance (Data.Type.Nat.SNatI m, (n :: Data.Nat.Nat) GHC.Types.~ ('Data.Nat.S m :: Data.Nat.Nat)) => Data.Semigroup.Traversable.Class.Traversable1 (Data.Vec.DataFamily.SpineStrict.Vec n) instance Data.Type.Nat.SNatI n => Data.Traversable.Traversable (Data.Vec.DataFamily.SpineStrict.Vec n) instance Data.Type.Nat.SNatI n => WithIndex.FunctorWithIndex (Data.Fin.Fin n) (Data.Vec.DataFamily.SpineStrict.Vec n) instance Data.Type.Nat.SNatI n => WithIndex.FoldableWithIndex (Data.Fin.Fin n) (Data.Vec.DataFamily.SpineStrict.Vec n) instance Data.Type.Nat.SNatI n => WithIndex.TraversableWithIndex (Data.Fin.Fin n) (Data.Vec.DataFamily.SpineStrict.Vec n) instance Data.Type.Nat.SNatI n => GHC.Base.Applicative (Data.Vec.DataFamily.SpineStrict.Vec n) instance Data.Type.Nat.SNatI n => GHC.Base.Monad (Data.Vec.DataFamily.SpineStrict.Vec n) instance Data.Type.Nat.SNatI n => Data.Distributive.Distributive (Data.Vec.DataFamily.SpineStrict.Vec n) instance Data.Type.Nat.SNatI n => Data.Functor.Rep.Representable (Data.Vec.DataFamily.SpineStrict.Vec n) instance (GHC.Base.Semigroup a, Data.Type.Nat.SNatI n) => GHC.Base.Semigroup (Data.Vec.DataFamily.SpineStrict.Vec n a) instance (GHC.Base.Monoid a, Data.Type.Nat.SNatI n) => GHC.Base.Monoid (Data.Vec.DataFamily.SpineStrict.Vec n a) instance Data.Type.Nat.SNatI n => Data.Functor.Bind.Class.Apply (Data.Vec.DataFamily.SpineStrict.Vec n) instance Data.Type.Nat.SNatI n => Data.Functor.Bind.Class.Bind (Data.Vec.DataFamily.SpineStrict.Vec n) instance Data.Type.Nat.SNatI n => Test.QuickCheck.Arbitrary.Arbitrary1 (Data.Vec.DataFamily.SpineStrict.Vec n) instance (Data.Type.Nat.SNatI n, Test.QuickCheck.Arbitrary.Arbitrary a) => Test.QuickCheck.Arbitrary.Arbitrary (Data.Vec.DataFamily.SpineStrict.Vec n a) instance (Data.Type.Nat.SNatI n, Test.QuickCheck.Arbitrary.CoArbitrary a) => Test.QuickCheck.Arbitrary.CoArbitrary (Data.Vec.DataFamily.SpineStrict.Vec n a) instance (Data.Type.Nat.SNatI n, Test.QuickCheck.Function.Function a) => Test.QuickCheck.Function.Function (Data.Vec.DataFamily.SpineStrict.Vec n a) -- | Lazy (in elements and spine) length-indexed list: Vec. module Data.Vec.Lazy -- | Vector, i.e. length-indexed list. data Vec (n :: Nat) a [VNil] :: Vec 'Z a [:::] :: a -> Vec n a -> Vec ('S n) a infixr 5 ::: -- | Empty Vec. empty :: Vec 'Z a -- | Vec with exactly one element. -- -- 
--   >>> singleton True
--   True ::: VNil
--
singleton :: a -> Vec ('S 'Z) a -- | O(n). Recover SNatI (and SNatI) dictionary from a -- Vec value. -- -- Example: reflect is constrained with SNatI n, -- but if we have a Vec n a, we can recover that -- dictionary: -- -- 
--   >>> let f :: forall n a. Vec n a -> N.Nat; f v = withDict v (N.reflect (Proxy :: Proxy n)) in f (True ::: VNil)
--   1
--
-- -- Note: using SNatI 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. withDict :: Vec n a -> (SNatI n => r) -> r -- | Convert to pull Vec. toPull :: Vec n a -> Vec n a -- | Convert from pull Vec. fromPull :: forall n a. SNatI n => Vec n a -> Vec n a -- | Convert Vec to list. -- -- 
--   >>> toList $ 'f' ::: 'o' ::: 'o' ::: VNil
--   "foo"
--
toList :: Vec n a -> [a] -- | 
--   >>> toNonEmpty $ 1 ::: 2 ::: 3 ::: VNil
--   1 :| [2,3]
--
toNonEmpty :: Vec ('S n) a -> NonEmpty a -- | Convert list [a] to Vec n a. Returns -- Nothing if lengths don't match exactly. -- -- 
--   >>> fromList "foo" :: Maybe (Vec N.Nat3 Char)
--   Just ('f' ::: 'o' ::: 'o' ::: VNil)
--
-- -- 
--   >>> fromList "quux" :: Maybe (Vec N.Nat3 Char)
--   Nothing
--
-- -- 
--   >>> fromList "xy" :: Maybe (Vec N.Nat3 Char)
--   Nothing
--
fromList :: SNatI n => [a] -> Maybe (Vec n a) -- | Convert list [a] to Vec n a. Returns -- Nothing 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
--
fromListPrefix :: SNatI n => [a] -> Maybe (Vec n a) -- | Reify any list [a] to Vec n a. -- -- 
--   >>> reifyList "foo" length
--   3
--
reifyList :: [a] -> (forall n. SNatI n => Vec n a -> r) -> r -- | Indexing. -- -- 
--   >>> ('a' ::: 'b' ::: 'c' ::: VNil) ! FS FZ
--   'b'
--
(!) :: Vec n a -> Fin n -> a -- | Tabulating, inverse of !. -- -- 
--   >>> tabulate id :: Vec N.Nat3 (Fin N.Nat3)
--   0 ::: 1 ::: 2 ::: VNil
--
tabulate :: SNatI n => (Fin n -> a) -> Vec n a -- | Cons an element in front of a Vec. cons :: a -> Vec n a -> Vec ('S n) a -- | Add a single element at the end of a Vec. snoc :: Vec n a -> a -> Vec ('S n) a -- | The first element of a Vec. head :: Vec ('S n) a -> a -- | The last element of a Vec. last :: Vec ('S n) a -> a -- | The elements after the head of a Vec. tail :: Vec ('S n) a -> Vec n a -- | The elements before the last of a Vec. init :: Vec ('S n) a -> Vec n a -- | Reverse Vec. -- -- 
--   >>> reverse ('a' ::: 'b' ::: 'c' ::: VNil)
--   'c' ::: 'b' ::: 'a' ::: VNil
--
reverse :: Vec n a -> Vec n a -- | Dependent right fold. -- -- This could been called an indexed fold, but that name is already used. dfoldr :: forall n a f. (forall m. a -> f m -> f ('S m)) -> f 'Z -> Vec n a -> f n -- | Dependent left fold. dfoldl :: forall n a f. (forall m. f m -> a -> f ('S m)) -> f 'Z -> Vec n a -> f n -- | Dependent strict left fold. dfoldl' :: forall n a f. (forall m. f m -> a -> f ('S m)) -> f 'Z -> Vec n a -> f n -- | Append two Vec. -- -- 
--   >>> ('a' ::: 'b' ::: VNil) ++ ('c' ::: 'd' ::: VNil)
--   'a' ::: 'b' ::: 'c' ::: 'd' ::: VNil
--
(++) :: Vec n a -> Vec m a -> Vec (Plus n m) a infixr 5 ++ -- | 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
--
split :: SNatI n => Vec (Plus n m) a -> (Vec n a, Vec m a) -- | Map over all the elements of a Vec and concatenate the -- resulting Vecs. -- -- 
--   >>> concatMap (\x -> x ::: x ::: VNil) ('a' ::: 'b' ::: VNil)
--   'a' ::: 'a' ::: 'b' ::: 'b' ::: VNil
--
concatMap :: (a -> Vec m b) -> Vec n a -> Vec (Mult n m) b -- | 
--   concatMap id
--
concat :: Vec n (Vec m a) -> Vec (Mult n m) a -- | 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)
--
chunks :: (SNatI n, SNatI m) => Vec (Mult n m) a -> Vec n (Vec m a) -- | 
--   >>> let xs = 'a' ::: 'b' ::: 'c' ::: 'd' ::: 'e' ::: VNil
--   
--   >>> take xs :: Vec N.Nat3 Char
--   'a' ::: 'b' ::: 'c' ::: VNil
--
take :: forall n m a. LE n m => Vec m a -> Vec n a -- | 
--   >>> let xs = 'a' ::: 'b' ::: 'c' ::: 'd' ::: 'e' ::: VNil
--   
--   >>> drop xs :: Vec N.Nat3 Char
--   'c' ::: 'd' ::: 'e' ::: VNil
--
drop :: forall n m a. (LE n m, SNatI m) => Vec m a -> Vec n a -- | See Foldable. foldMap :: Monoid m => (a -> m) -> Vec n a -> m -- | See Foldable1. foldMap1 :: Semigroup s => (a -> s) -> Vec ('S n) a -> s -- | See FoldableWithIndex. ifoldMap :: Monoid m => (Fin n -> a -> m) -> Vec n a -> m -- | There is no type-class for this :( ifoldMap1 :: Semigroup s => (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s -- | Right fold. foldr :: forall a b n. (a -> b -> b) -> b -> Vec n a -> b -- | Right fold with an index. ifoldr :: forall a b n. (Fin n -> a -> b -> b) -> b -> Vec n a -> b -- | Strict left fold. foldl' :: forall a b n. (b -> a -> b) -> b -> Vec n a -> b -- | Yield the length of a Vec. O(n) length :: Vec n a -> Int -- | Test whether a Vec is empty. O(1) null :: Vec n a -> Bool -- | Non-strict sum. sum :: Num a => Vec n a -> a -- | Non-strict product. product :: Num a => Vec n a -> a -- | 
--   >>> map not $ True ::: False ::: VNil
--   False ::: True ::: VNil
--
map :: (a -> b) -> Vec n a -> Vec n b -- | 
--   >>> imap (,) $ 'a' ::: 'b' ::: 'c' ::: VNil
--   (0,'a') ::: (1,'b') ::: (2,'c') ::: VNil
--
imap :: (Fin n -> a -> b) -> Vec n a -> Vec n b -- | Apply an action to every element of a Vec, yielding a -- Vec of results. traverse :: forall n f a b. Applicative f => (a -> f b) -> Vec n a -> f (Vec n b) -- | Apply an action to non-empty Vec, yielding a Vec of -- results. traverse1 :: forall n f a b. Apply f => (a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b) -- | Apply an action to every element of a Vec and its index, -- yielding a Vec of results. itraverse :: Applicative f => (Fin n -> a -> f b) -> Vec n a -> f (Vec n b) -- | Apply an action to every element of a Vec and its index, -- ignoring the results. itraverse_ :: Applicative f => (Fin n -> a -> f b) -> Vec n a -> f () -- | Zip two Vecs with a function. zipWith :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c -- | Zip two Vecs. with a function that also takes the elements' -- indices. izipWith :: (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c -- | Repeat a value. -- -- 
--   >>> repeat 'x' :: Vec N.Nat3 Char
--   'x' ::: 'x' ::: 'x' ::: VNil
--
repeat :: SNatI n => x -> Vec n x -- | Monadic bind. bind :: Vec n a -> (a -> Vec n b) -> Vec n b -- | Monadic join. -- -- 
--   >>> join $ ('a' ::: 'b' ::: VNil) ::: ('c' ::: 'd' ::: VNil) ::: VNil
--   'a' ::: 'd' ::: VNil
--
join :: Vec n (Vec n a) -> Vec n a -- | Get all Fin n in a Vec n. -- -- 
--   >>> universe :: Vec N.Nat3 (Fin N.Nat3)
--   0 ::: 1 ::: 2 ::: VNil
--
universe :: SNatI n => Vec n (Fin n) -- | 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. class VecEach s t a b | s -> a, t -> b, s b -> t, t a -> s mapWithVec :: VecEach s t a b => (forall n. SNatI n => Vec n a -> Vec n b) -> s -> t traverseWithVec :: (VecEach s t a b, Applicative f) => (forall n. SNatI n => Vec n a -> f (Vec n b)) -> s -> f t instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.Vec.Lazy.Vec n a) instance GHC.Classes.Ord a => GHC.Classes.Ord (Data.Vec.Lazy.Vec n a) instance ((a :: *) GHC.Types.~ (a' :: *), (b :: *) GHC.Types.~ (b' :: *)) => Data.Vec.Lazy.VecEach (a, a') (b, b') a b instance ((a :: *) GHC.Types.~ (a2 :: *), (a :: *) GHC.Types.~ (a3 :: *), (b :: *) GHC.Types.~ (b2 :: *), (b :: *) GHC.Types.~ (b3 :: *)) => Data.Vec.Lazy.VecEach (a, a2, a3) (b, b2, b3) a b instance ((a :: *) GHC.Types.~ (a2 :: *), (a :: *) GHC.Types.~ (a3 :: *), (a :: *) GHC.Types.~ (a4 :: *), (b :: *) GHC.Types.~ (b2 :: *), (b :: *) GHC.Types.~ (b3 :: *), (b :: *) GHC.Types.~ (b4 :: *)) => Data.Vec.Lazy.VecEach (a, a2, a3, a4) (b, b2, b3, b4) a b instance GHC.Show.Show a => GHC.Show.Show (Data.Vec.Lazy.Vec n a) instance GHC.Base.Functor (Data.Vec.Lazy.Vec n) instance Data.Foldable.Foldable (Data.Vec.Lazy.Vec n) instance Data.Traversable.Traversable (Data.Vec.Lazy.Vec n) instance WithIndex.FunctorWithIndex (Data.Fin.Fin n) (Data.Vec.Lazy.Vec n) instance WithIndex.FoldableWithIndex (Data.Fin.Fin n) (Data.Vec.Lazy.Vec n) instance WithIndex.TraversableWithIndex (Data.Fin.Fin n) (Data.Vec.Lazy.Vec n) instance ((n :: Data.Nat.Nat) GHC.Types.~ ('Data.Nat.S m :: Data.Nat.Nat)) => Data.Foldable1.Foldable1 (Data.Vec.Lazy.Vec n) instance ((n :: Data.Nat.Nat) GHC.Types.~ ('Data.Nat.S m :: Data.Nat.Nat)) => Data.Semigroup.Traversable.Class.Traversable1 (Data.Vec.Lazy.Vec n) instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Data.Vec.Lazy.Vec n a) instance Data.Hashable.Class.Hashable a => Data.Hashable.Class.Hashable (Data.Vec.Lazy.Vec n a) instance Data.Type.Nat.SNatI n => GHC.Base.Applicative (Data.Vec.Lazy.Vec n) instance Data.Type.Nat.SNatI n => GHC.Base.Monad (Data.Vec.Lazy.Vec n) instance Data.Type.Nat.SNatI n => Data.Distributive.Distributive (Data.Vec.Lazy.Vec n) instance Data.Type.Nat.SNatI n => Data.Functor.Rep.Representable (Data.Vec.Lazy.Vec n) instance GHC.Base.Semigroup a => GHC.Base.Semigroup (Data.Vec.Lazy.Vec n a) instance (GHC.Base.Monoid a, Data.Type.Nat.SNatI n) => GHC.Base.Monoid (Data.Vec.Lazy.Vec n a) instance Data.Functor.Bind.Class.Apply (Data.Vec.Lazy.Vec n) instance Data.Functor.Bind.Class.Bind (Data.Vec.Lazy.Vec n) instance ((n :: Data.Nat.Nat) GHC.Types.~ ('Data.Nat.Z :: Data.Nat.Nat)) => Data.Boring.Boring (Data.Vec.Lazy.Vec n a) instance Data.Functor.Classes.Eq1 (Data.Vec.Lazy.Vec n) instance Data.Functor.Classes.Ord1 (Data.Vec.Lazy.Vec n) instance Data.Functor.Classes.Show1 (Data.Vec.Lazy.Vec n) instance Data.Type.Nat.SNatI n => Test.QuickCheck.Arbitrary.Arbitrary1 (Data.Vec.Lazy.Vec n) instance (Data.Type.Nat.SNatI n, Test.QuickCheck.Arbitrary.Arbitrary a) => Test.QuickCheck.Arbitrary.Arbitrary (Data.Vec.Lazy.Vec n a) instance (Data.Type.Nat.SNatI n, Test.QuickCheck.Arbitrary.CoArbitrary a) => Test.QuickCheck.Arbitrary.CoArbitrary (Data.Vec.Lazy.Vec n a) instance (Data.Type.Nat.SNatI n, Test.QuickCheck.Function.Function a) => Test.QuickCheck.Function.Function (Data.Vec.Lazy.Vec n a) -- | 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. module Data.Vec.Lazy.Inline -- | Vector, i.e. length-indexed list. data Vec (n :: Nat) a [VNil] :: Vec 'Z a [:::] :: a -> Vec n a -> Vec ('S n) a infixr 5 ::: -- | Empty Vec. empty :: Vec 'Z a -- | Vec with exactly one element. -- -- 
--   >>> singleton True
--   True ::: VNil
--
singleton :: a -> Vec ('S 'Z) a -- | Convert to pull Vec. toPull :: forall n a. SNatI n => Vec n a -> Vec n a -- | Convert from pull Vec. fromPull :: forall n a. SNatI n => Vec n a -> Vec n a -- | Convert Vec to list. -- -- 
--   >>> toList $ 'f' ::: 'o' ::: 'o' ::: VNil
--   "foo"
--
toList :: forall n a. SNatI n => Vec n a -> [a] -- | 
--   >>> toNonEmpty $ 1 ::: 2 ::: 3 ::: VNil
--   1 :| [2,3]
--
toNonEmpty :: forall n a. SNatI n => Vec ('S n) a -> NonEmpty a -- | Convert list [a] to Vec n a. Returns -- Nothing if lengths don't match exactly. -- -- 
--   >>> fromList "foo" :: Maybe (Vec N.Nat3 Char)
--   Just ('f' ::: 'o' ::: 'o' ::: VNil)
--
-- -- 
--   >>> fromList "quux" :: Maybe (Vec N.Nat3 Char)
--   Nothing
--
-- -- 
--   >>> fromList "xy" :: Maybe (Vec N.Nat3 Char)
--   Nothing
--
fromList :: SNatI n => [a] -> Maybe (Vec n a) -- | Convert list [a] to Vec n a. Returns -- Nothing 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
--
fromListPrefix :: SNatI n => [a] -> Maybe (Vec n a) -- | Reify any list [a] to Vec n a. -- -- 
--   >>> reifyList "foo" length
--   3
--
reifyList :: [a] -> (forall n. SNatI n => Vec n a -> r) -> r -- | Indexing. -- -- 
--   >>> ('a' ::: 'b' ::: 'c' ::: VNil) ! FS FZ
--   'b'
--
(!) :: SNatI n => Vec n a -> Fin n -> a -- | Tabulating, inverse of !. -- -- 
--   >>> tabulate id :: Vec N.Nat3 (Fin N.Nat3)
--   0 ::: 1 ::: 2 ::: VNil
--
tabulate :: SNatI n => (Fin n -> a) -> Vec n a -- | Cons an element in front of a Vec. cons :: a -> Vec n a -> Vec ('S n) a -- | Add a single element at the end of a Vec. snoc :: forall n a. SNatI n => Vec n a -> a -> Vec ('S n) a -- | The first element of a Vec. head :: Vec ('S n) a -> a -- | The last element of a Vec. last :: forall n a. SNatI n => Vec ('S n) a -> a -- | The elements after the head of a Vec. tail :: Vec ('S n) a -> Vec n a -- | The elements before the last of a Vec. init :: forall n a. SNatI n => Vec ('S n) a -> Vec n a -- | Append two Vec. -- -- 
--   >>> ('a' ::: 'b' ::: VNil) ++ ('c' ::: 'd' ::: VNil)
--   'a' ::: 'b' ::: 'c' ::: 'd' ::: VNil
--
(++) :: forall n m a. SNatI n => Vec n a -> Vec m a -> Vec (Plus n m) a infixr 5 ++ -- | 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
--
split :: SNatI n => Vec (Plus n m) a -> (Vec n a, Vec m a) -- | Map over all the elements of a Vec and concatenate the -- resulting Vecs. -- -- 
--   >>> concatMap (\x -> x ::: x ::: VNil) ('a' ::: 'b' ::: VNil)
--   'a' ::: 'a' ::: 'b' ::: 'b' ::: VNil
--
concatMap :: forall a b n m. (SNatI m, SNatI n) => (a -> Vec m b) -> Vec n a -> Vec (Mult n m) b -- | 
--   concatMap id
--
concat :: (SNatI m, SNatI n) => Vec n (Vec m a) -> Vec (Mult n m) a -- | 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)
--
chunks :: (SNatI n, SNatI m) => Vec (Mult n m) a -> Vec n (Vec m a) -- | Reverse Vec. -- -- 
--   >>> reverse ('a' ::: 'b' ::: 'c' ::: VNil)
--   'c' ::: 'b' ::: 'a' ::: VNil
--
reverse :: forall n a. SNatI n => Vec n a -> Vec n a -- | See Foldable. foldMap :: (Monoid m, SNatI n) => (a -> m) -> Vec n a -> m -- | See Foldable1. foldMap1 :: forall s a n. (Semigroup s, SNatI n) => (a -> s) -> Vec ('S n) a -> s -- | See FoldableWithIndex. ifoldMap :: forall a n m. (Monoid m, SNatI n) => (Fin n -> a -> m) -> Vec n a -> m -- | There is no type-class for this :( ifoldMap1 :: forall a n s. (Semigroup s, SNatI n) => (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s -- | Right fold. foldr :: forall a b n. SNatI n => (a -> b -> b) -> b -> Vec n a -> b -- | Right fold with an index. ifoldr :: forall a b n. SNatI n => (Fin n -> a -> b -> b) -> b -> Vec n a -> b -- | Yield the length of a Vec. O(n) length :: forall n a. SNatI n => Vec n a -> Int -- | Test whether a Vec is empty. O(1) null :: Vec n a -> Bool -- | Non-strict sum. sum :: (Num a, SNatI n) => Vec n a -> a -- | Non-strict product. product :: (Num a, SNatI n) => Vec n a -> a -- | 
--   >>> map not $ True ::: False ::: VNil
--   False ::: True ::: VNil
--
map :: forall a b n. SNatI n => (a -> b) -> Vec n a -> Vec n b -- | 
--   >>> imap (,) $ 'a' ::: 'b' ::: 'c' ::: VNil
--   (0,'a') ::: (1,'b') ::: (2,'c') ::: VNil
--
imap :: SNatI n => (Fin n -> a -> b) -> Vec n a -> Vec n b -- | Apply an action to every element of a Vec, yielding a -- Vec of results. traverse :: forall n f a b. (Applicative f, SNatI n) => (a -> f b) -> Vec n a -> f (Vec n b) -- | Apply an action to non-empty Vec, yielding a Vec of -- results. traverse1 :: forall n f a b. (Apply f, SNatI n) => (a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b) -- | Apply an action to every element of a Vec and its index, -- yielding a Vec of results. itraverse :: forall n f a b. (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, -- ignoring the results. itraverse_ :: forall n f a b. (Applicative f, SNatI n) => (Fin n -> a -> f b) -> Vec n a -> f () -- | Zip two Vecs with a function. zipWith :: forall a b c n. SNatI 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. izipWith :: SNatI n => (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c -- | Repeat value -- -- 
--   >>> repeat 'x' :: Vec N.Nat3 Char
--   'x' ::: 'x' ::: 'x' ::: VNil
--
repeat :: SNatI n => x -> Vec n x -- | Monadic bind. bind :: SNatI n => Vec n a -> (a -> Vec n b) -> Vec n b -- | Monadic join. -- -- 
--   >>> join $ ('a' ::: 'b' ::: VNil) ::: ('c' ::: 'd' ::: VNil) ::: VNil
--   'a' ::: 'd' ::: VNil
--
join :: SNatI n => Vec n (Vec n a) -> Vec n a -- | Get all Fin n in a Vec n. -- -- 
--   >>> universe :: Vec N.Nat3 (Fin N.Nat3)
--   0 ::: 1 ::: 2 ::: VNil
--
universe :: SNatI n => Vec n (Fin n) -- | 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. class VecEach s t a b | s -> a, t -> b, s b -> t, t a -> s mapWithVec :: VecEach s t a b => (forall n. SNatI n => Vec n a -> Vec n b) -> s -> t traverseWithVec :: (VecEach s t a b, Applicative f) => (forall n. SNatI n => Vec n a -> f (Vec n b)) -> s -> f t