-- 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. -- -- 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.1.1.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 unpurpose don'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 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) -- | Prism from list. _Vec :: SNatI n => Prism' [a] (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. InlineInduction n => Vec n a -> r) -> r -- | Indexing. (!) :: Vec n a -> Fin n -> a -- | Index lens. -- -- 
--   >>> ('a' L.::: 'b' L.::: 'c' L.::: L.VNil) ^. L._Pull . ix (FS FZ)
--   'b'
--
-- -- 
--   >>> ('a' L.::: 'b' L.::: 'c' L.::: L.VNil) & L._Pull . ix (FS FZ) .~ 'x'
--   'a' ::: 'x' ::: 'c' ::: VNil
--
ix :: Fin n -> Lens' (Vec n a) a -- | Match on non-empty Vec. -- -- Note: lens _Cons is a Prism. In fact, -- Vec n a cannot have an instance of Cons as -- types don't match. _Cons :: Iso (Vec ( 'S n) a) (Vec ( 'S n) b) (a, Vec n a) (b, Vec n b) -- | Head lens. Note: lens _head is a -- Traversal'. -- -- 
--   >>> ('a' L.::: 'b' L.::: 'c' L.::: L.VNil) ^. L._Pull . _head
--   'a'
--
-- -- 
--   >>> ('a' L.::: 'b' L.::: 'c' L.::: L.VNil) & L._Pull . _head .~ 'x'
--   'x' ::: 'b' ::: 'c' ::: VNil
--
_head :: Lens' (Vec ( 'S n) a) a -- | Head lens. Note: lens _head is a -- Traversal'. _tail :: Lens' (Vec ( 'S n) a) (Vec n a) -- | The first element of a Vec. head :: Vec ( 'S n) a -> a -- | The elements after the head of a Vec. tail :: Vec ( 'S 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 -- | 
--   >>> over L._Pull (map not) (True L.::: False L.::: L.VNil)
--   False ::: True ::: VNil
--
map :: (a -> b) -> Vec n a -> Vec n b -- | 
--   >>> over L._Pull (imap (,)) ('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 -- | 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 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 Control.Lens.Indexed.FunctorWithIndex (Data.Fin.Fin n) (Data.Vec.Pull.Vec n) instance Data.Type.Nat.SNatI n => Control.Lens.Indexed.FoldableWithIndex (Data.Fin.Fin n) (Data.Vec.Pull.Vec n) -- | 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 InlineInduction (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 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. withDict :: Vec n a -> (InlineInduction 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 -- | An Iso from toPull and fromPull. _Pull :: SNatI n => Iso (Vec n a) (Vec n b) (Vec n a) (Vec n b) -- | Convert Vec to list. -- -- 
--   >>> toList $ 'f' ::: 'o' ::: 'o' ::: VNil
--   "foo"
--
toList :: Vec n a -> [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) -- | Prism from list. -- -- 
--   >>> "foo" ^? _Vec :: Maybe (Vec N.Nat3 Char)
--   Just ('f' ::: 'o' ::: 'o' ::: VNil)
--
-- -- 
--   >>> "foo" ^? _Vec :: Maybe (Vec N.Nat2 Char)
--   Nothing
--
-- -- 
--   >>> _Vec # (True ::: False ::: VNil)
--   [True,False]
--
_Vec :: SNatI n => Prism' [a] (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. InlineInduction n => Vec n a -> r) -> r -- | Indexing. -- -- 
--   >>> ('a' ::: 'b' ::: 'c' ::: VNil) ! FS FZ
--   'b'
--
(!) :: Vec n a -> Fin n -> a -- | Index lens. -- -- 
--   >>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. ix (FS FZ)
--   'b'
--
-- -- 
--   >>> ('a' ::: 'b' ::: 'c' ::: VNil) & ix (FS FZ) .~ 'x'
--   'a' ::: 'x' ::: 'c' ::: VNil
--
ix :: Fin n -> Lens' (Vec n a) a -- | Match on non-empty Vec. -- -- Note: lens _Cons is a Prism. In fact, -- Vec n a cannot have an instance of Cons as -- types don't match. _Cons :: Iso (Vec ( 'S n) a) (Vec ( 'S n) b) (a, Vec n a) (b, Vec n b) -- | Head lens. Note: lens _head is a -- Traversal'. -- -- 
--   >>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. _head
--   'a'
--
-- -- 
--   >>> ('a' ::: 'b' ::: 'c' ::: VNil) & _head .~ 'x'
--   'x' ::: 'b' ::: 'c' ::: VNil
--
_head :: Lens' (Vec ( 'S n) a) a -- | Head lens. Note: lens _head is a -- Traversal'. _tail :: Lens' (Vec ( 'S n) a) (Vec n a) -- | Cons an element in front of a Vec. cons :: a -> Vec n a -> Vec ( 'S n) a -- | The first element of a Vec. head :: Vec ( 'S n) a -> a -- | The elements after the head of a Vec. tail :: Vec ( 'S n) a -> Vec n a -- | 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) -- | 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 -- | 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. class Each s t a b => VecEach s t a b | s -> a, t -> b, s b -> t, t a -> s mapWithVec :: VecEach s t a b => (forall n. InlineInduction n => Vec n a -> Vec n b) -> s -> t traverseWithVec :: (VecEach s t a b, Applicative f) => (forall n. InlineInduction 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 :: *) Data.Type.Equality.~ (a' :: *), (b :: *) Data.Type.Equality.~ (b' :: *)) => Data.Vec.Lazy.VecEach (a, a') (b, b') a b instance ((a :: *) Data.Type.Equality.~ (a2 :: *), (a :: *) Data.Type.Equality.~ (a3 :: *), (b :: *) Data.Type.Equality.~ (b2 :: *), (b :: *) Data.Type.Equality.~ (b3 :: *)) => Data.Vec.Lazy.VecEach (a, a2, a3) (b, b2, b3) a b instance ((a :: *) Data.Type.Equality.~ (a2 :: *), (a :: *) Data.Type.Equality.~ (a3 :: *), (a :: *) Data.Type.Equality.~ (a4 :: *), (b :: *) Data.Type.Equality.~ (b2 :: *), (b :: *) Data.Type.Equality.~ (b3 :: *), (b :: *) Data.Type.Equality.~ (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 ((n :: Data.Nat.Nat) Data.Type.Equality.~ ('Data.Nat.S m :: Data.Nat.Nat)) => Data.Semigroup.Foldable.Class.Foldable1 (Data.Vec.Lazy.Vec n) instance Data.Traversable.Traversable (Data.Vec.Lazy.Vec n) instance ((n :: Data.Nat.Nat) Data.Type.Equality.~ ('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 Control.Lens.Indexed.FunctorWithIndex (Data.Fin.Fin n) (Data.Vec.Lazy.Vec n) instance Control.Lens.Indexed.FoldableWithIndex (Data.Fin.Fin n) (Data.Vec.Lazy.Vec n) instance Control.Lens.Indexed.TraversableWithIndex (Data.Fin.Fin n) (Data.Vec.Lazy.Vec n) instance Control.Lens.Each.Each (Data.Vec.Lazy.Vec n a) (Data.Vec.Lazy.Vec n b) a b instance Control.Lens.At.Ixed (Data.Vec.Lazy.Vec n a) instance Control.Lens.Tuple.Field1 (Data.Vec.Lazy.Vec ('Data.Nat.S n) a) (Data.Vec.Lazy.Vec ('Data.Nat.S n) a) a a instance Control.Lens.Tuple.Field2 (Data.Vec.Lazy.Vec ('Data.Nat.S ('Data.Nat.S n)) a) (Data.Vec.Lazy.Vec ('Data.Nat.S ('Data.Nat.S n)) a) a a instance Control.Lens.Tuple.Field3 (Data.Vec.Lazy.Vec ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S n))) a) (Data.Vec.Lazy.Vec ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S n))) a) a a instance Control.Lens.Tuple.Field4 (Data.Vec.Lazy.Vec ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S n)))) a) (Data.Vec.Lazy.Vec ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S n)))) a) a a instance Control.Lens.Tuple.Field5 (Data.Vec.Lazy.Vec ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S n))))) a) (Data.Vec.Lazy.Vec ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S n))))) a) a a instance Control.Lens.Tuple.Field6 (Data.Vec.Lazy.Vec ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S n)))))) a) (Data.Vec.Lazy.Vec ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S n)))))) a) a a instance Control.Lens.Tuple.Field7 (Data.Vec.Lazy.Vec ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S n))))))) a) (Data.Vec.Lazy.Vec ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S n))))))) a) a a instance Control.Lens.Tuple.Field8 (Data.Vec.Lazy.Vec ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S n)))))))) a) (Data.Vec.Lazy.Vec ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S n)))))))) a) a a instance Control.Lens.Tuple.Field9 (Data.Vec.Lazy.Vec ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S n))))))))) a) (Data.Vec.Lazy.Vec ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S n))))))))) a) a a -- | A variant of Data.Vec.Lazy with functions written using -- InlineInduction. 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. InlineInduction n => Vec n a -> Vec n a -- | Convert from pull Vec. fromPull :: forall n a. InlineInduction n => Vec n a -> Vec n a -- | An Iso from toPull and fromPull. _Pull :: InlineInduction n => Iso (Vec n a) (Vec n b) (Vec n a) (Vec n b) -- | Convert Vec to list. -- -- 
--   >>> toList $ 'f' ::: 'o' ::: 'o' ::: VNil
--   "foo"
--
toList :: forall n a. InlineInduction n => Vec n a -> [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 :: InlineInduction n => [a] -> Maybe (Vec n a) -- | Prism from list. -- -- 
--   >>> "foo" ^? _Vec :: Maybe (Vec N.Nat3 Char)
--   Just ('f' ::: 'o' ::: 'o' ::: VNil)
--
-- -- 
--   >>> "foo" ^? _Vec :: Maybe (Vec N.Nat2 Char)
--   Nothing
--
-- -- 
--   >>> _Vec # (True ::: False ::: VNil)
--   [True,False]
--
_Vec :: InlineInduction n => Prism' [a] (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 :: InlineInduction n => [a] -> Maybe (Vec n a) -- | Reify any list [a] to Vec n a. -- -- 
--   >>> reifyList "foo" length
--   3
--
reifyList :: [a] -> (forall n. InlineInduction n => Vec n a -> r) -> r -- | Indexing. -- -- 
--   >>> ('a' ::: 'b' ::: 'c' ::: VNil) ! FS FZ
--   'b'
--
(!) :: InlineInduction n => Vec n a -> Fin n -> a -- | Index lens. -- -- 
--   >>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. ix (FS FZ)
--   'b'
--
-- -- 
--   >>> ('a' ::: 'b' ::: 'c' ::: VNil) & ix (FS FZ) .~ 'x'
--   'a' ::: 'x' ::: 'c' ::: VNil
--
ix :: InlineInduction n => Fin n -> Lens' (Vec n a) a -- | Match on non-empty Vec. -- -- Note: lens _Cons is a Prism. In fact, -- Vec n a cannot have an instance of Cons as -- types don't match. _Cons :: Iso (Vec ( 'S n) a) (Vec ( 'S n) b) (a, Vec n a) (b, Vec n b) -- | Head lens. Note: lens _head is a -- Traversal'. -- -- 
--   >>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. _head
--   'a'
--
-- -- 
--   >>> ('a' ::: 'b' ::: 'c' ::: VNil) & _head .~ 'x'
--   'x' ::: 'b' ::: 'c' ::: VNil
--
_head :: Lens' (Vec ( 'S n) a) a -- | Head lens. Note: lens _head is a -- Traversal'. _tail :: Lens' (Vec ( 'S n) a) (Vec n a) -- | Cons an element in front of a Vec. cons :: a -> Vec n a -> Vec ( 'S n) a -- | The first element of a Vec. head :: Vec ( 'S n) a -> a -- | The elements after the head of a Vec. tail :: 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. InlineInduction 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 :: InlineInduction 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. (InlineInduction m, InlineInduction n) => (a -> Vec m b) -> Vec n a -> Vec (Mult n m) b -- | 
--   concatMap id
--
concat :: (InlineInduction m, InlineInduction 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 :: (InlineInduction n, InlineInduction m) => Vec (Mult n m) a -> Vec n (Vec m a) -- | See Foldable. foldMap :: (Monoid m, InlineInduction n) => (a -> m) -> Vec n a -> m -- | See Foldable1. foldMap1 :: forall s a n. (Semigroup s, InlineInduction n) => (a -> s) -> Vec ( 'S n) a -> s -- | See FoldableWithIndex. ifoldMap :: forall a n m. (Monoid m, InlineInduction n) => (Fin n -> a -> m) -> Vec n a -> m -- | There is no type-class for this :( ifoldMap1 :: forall a n s. (Semigroup s, InlineInduction n) => (Fin ( 'S n) -> a -> s) -> Vec ( 'S n) a -> s -- | Right fold. foldr :: forall a b n. InlineInduction n => (a -> b -> b) -> b -> Vec n a -> b -- | Right fold with an index. ifoldr :: forall a b n. InlineInduction n => (Fin n -> a -> b -> b) -> b -> Vec n a -> b -- | Yield the length of a Vec. O(n) length :: forall n a. InlineInduction n => Vec n a -> Int -- | Test whether a Vec is empty. O(1) null :: Vec n a -> Bool -- | Non-strict sum. sum :: (Num a, InlineInduction n) => Vec n a -> a -- | Non-strict product. product :: (Num a, InlineInduction n) => Vec n a -> a -- | 
--   >>> map not $ True ::: False ::: VNil
--   False ::: True ::: VNil
--
map :: forall a b n. InlineInduction n => (a -> b) -> Vec n a -> Vec n b -- | 
--   >>> imap (,) $ 'a' ::: 'b' ::: 'c' ::: VNil
--   (0,'a') ::: (1,'b') ::: (2,'c') ::: VNil
--
imap :: InlineInduction 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, InlineInduction 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, InlineInduction 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, InlineInduction 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, InlineInduction n) => (Fin n -> a -> f b) -> Vec n a -> f () -- | Zip two Vecs with a function. zipWith :: forall a b c n. InlineInduction 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 :: InlineInduction n => (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c -- | Monadic bind. bind :: InlineInduction 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 :: InlineInduction 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 :: InlineInduction 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. class Each s t a b => VecEach s t a b | s -> a, t -> b, s b -> t, t a -> s mapWithVec :: VecEach s t a b => (forall n. InlineInduction n => Vec n a -> Vec n b) -> s -> t traverseWithVec :: (VecEach s t a b, Applicative f) => (forall n. InlineInduction n => Vec n a -> f (Vec n b)) -> s -> f t -- | 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. InlineInduction n => Vec n a -> Vec n a -- | Convert from pull Vec. fromPull :: forall n a. InlineInduction n => Vec n a -> Vec n a -- | An Iso from toPull and fromPull. _Pull :: InlineInduction n => Iso (Vec n a) (Vec n b) (Vec n a) (Vec n b) -- | Convert Vec to list. -- -- 
--   >>> toList $ 'f' ::: 'o' ::: 'o' ::: VNil
--   "foo"
--
toList :: forall n a. InlineInduction n => Vec n a -> [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 :: InlineInduction n => [a] -> Maybe (Vec n a) -- | Prism from list. -- -- 
--   >>> "foo" ^? _Vec :: Maybe (Vec N.Nat3 Char)
--   Just ('f' ::: 'o' ::: 'o' ::: VNil)
--
-- -- 
--   >>> "foo" ^? _Vec :: Maybe (Vec N.Nat2 Char)
--   Nothing
--
-- -- 
--   >>> _Vec # (True ::: False ::: VNil)
--   [True,False]
--
_Vec :: InlineInduction n => Prism' [a] (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 :: InlineInduction n => [a] -> Maybe (Vec n a) -- | Reify any list [a] to Vec n a. -- -- 
--   >>> reifyList "foo" length
--   3
--
reifyList :: [a] -> (forall n. InlineInduction n => Vec n a -> r) -> r -- | Indexing. -- -- 
--   >>> ('a' ::: 'b' ::: 'c' ::: VNil) ! FS FZ
--   'b'
--
(!) :: InlineInduction n => Vec n a -> Fin n -> a -- | Index lens. -- -- 
--   >>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. ix (FS FZ)
--   'b'
--
-- -- 
--   >>> ('a' ::: 'b' ::: 'c' ::: VNil) & ix (FS FZ) .~ 'x'
--   'a' ::: 'x' ::: 'c' ::: VNil
--
ix :: Fin n -> Lens' (Vec n a) a -- | Match on non-empty Vec. -- -- Note: lens _Cons is a Prism. In fact, -- Vec n a cannot have an instance of Cons as -- types don't match. _Cons :: Iso (Vec ( 'S n) a) (Vec ( 'S n) b) (a, Vec n a) (b, Vec n b) -- | Head lens. Note: lens _head is a -- Traversal'. -- -- 
--   >>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. _head
--   'a'
--
-- -- 
--   >>> ('a' ::: 'b' ::: 'c' ::: VNil) & _head .~ 'x'
--   'x' ::: 'b' ::: 'c' ::: VNil
--
_head :: Lens' (Vec ( 'S n) a) a -- | Head lens. Note: lens _head is a -- Traversal'. _tail :: Lens' (Vec ( 'S n) a) (Vec n a) -- | Cons an element in front of a Vec. cons :: a -> Vec n a -> Vec ( 'S n) a -- | The first element of a Vec. head :: Vec ( 'S n) a -> a -- | The elements after the head of a Vec. tail :: 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. InlineInduction 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 :: InlineInduction 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. (InlineInduction m, InlineInduction n) => (a -> Vec m b) -> Vec n a -> Vec (Mult n m) b -- | 
--   concatMap id
--
concat :: (InlineInduction m, InlineInduction 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 :: (InlineInduction n, InlineInduction m) => Vec (Mult n m) a -> Vec n (Vec m a) -- | See Foldable. foldMap :: (Monoid m, InlineInduction n) => (a -> m) -> Vec n a -> m -- | See Foldable1. foldMap1 :: forall s a n. (Semigroup s, InlineInduction n) => (a -> s) -> Vec ( 'S n) a -> s -- | See FoldableWithIndex. ifoldMap :: forall a n m. (Monoid m, InlineInduction n) => (Fin n -> a -> m) -> Vec n a -> m -- | There is no type-class for this :( ifoldMap1 :: forall a n s. (Semigroup s, InlineInduction n) => (Fin ( 'S n) -> a -> s) -> Vec ( 'S n) a -> s -- | Right fold. foldr :: forall a b n. InlineInduction n => (a -> b -> b) -> b -> Vec n a -> b -- | Right fold with an index. ifoldr :: forall a b n. InlineInduction n => (Fin n -> a -> b -> b) -> b -> Vec n a -> b -- | Yield the length of a Vec. O(n) length :: forall n a. InlineInduction 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, InlineInduction n) => Vec n a -> a -- | Non-strict product. product :: (Num a, InlineInduction n) => Vec n a -> a -- | 
--   >>> map not $ True ::: False ::: VNil
--   False ::: True ::: VNil
--
map :: forall a b n. InlineInduction n => (a -> b) -> Vec n a -> Vec n b -- | 
--   >>> imap (,) $ 'a' ::: 'b' ::: 'c' ::: VNil
--   (0,'a') ::: (1,'b') ::: (2,'c') ::: VNil
--
imap :: InlineInduction 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, InlineInduction 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, InlineInduction 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, InlineInduction 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, InlineInduction n) => (Fin n -> a -> f b) -> Vec n a -> f () -- | Zip two Vecs with a function. zipWith :: forall a b c n. InlineInduction 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 :: InlineInduction n => (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c -- | Monadic bind. bind :: InlineInduction 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 :: InlineInduction 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 :: InlineInduction n => Vec n (Fin n) -- | Ensure spine. -- -- 
--   >>> view (ix F.fin1) $ set (ix F.fin1) 'x' (error "err" :: Vec N.Nat2 Char)
--   *** Exception: err
--   ...
--
-- -- 
--   >>> view (ix F.fin1) $ set (ix F.fin1) 'x' $ ensureSpine (error "err" :: Vec N.Nat2 Char)
--   'x'
--
ensureSpine :: InlineInduction n => Vec n a -> Vec n a instance (Data.Hashable.Class.Hashable a, Data.Type.Nat.InlineInduction n) => Data.Hashable.Class.Hashable (Data.Vec.DataFamily.SpineStrict.Vec n a) instance (Control.DeepSeq.NFData a, Data.Type.Nat.InlineInduction n) => Control.DeepSeq.NFData (Data.Vec.DataFamily.SpineStrict.Vec n a) instance (GHC.Show.Show a, Data.Type.Nat.InlineInduction n) => GHC.Show.Show (Data.Vec.DataFamily.SpineStrict.Vec n a) instance (GHC.Classes.Ord a, Data.Type.Nat.InlineInduction n) => GHC.Classes.Ord (Data.Vec.DataFamily.SpineStrict.Vec n a) instance (GHC.Classes.Eq a, Data.Type.Nat.InlineInduction n) => GHC.Classes.Eq (Data.Vec.DataFamily.SpineStrict.Vec n a) instance Data.Type.Nat.InlineInduction n => GHC.Base.Functor (Data.Vec.DataFamily.SpineStrict.Vec n) instance Data.Type.Nat.InlineInduction n => Data.Foldable.Foldable (Data.Vec.DataFamily.SpineStrict.Vec n) instance (Data.Type.Nat.InlineInduction m, (n :: Data.Nat.Nat) Data.Type.Equality.~ ('Data.Nat.S m :: Data.Nat.Nat)) => Data.Semigroup.Foldable.Class.Foldable1 (Data.Vec.DataFamily.SpineStrict.Vec n) instance Data.Type.Nat.InlineInduction n => Data.Traversable.Traversable (Data.Vec.DataFamily.SpineStrict.Vec n) instance (Data.Type.Nat.InlineInduction m, (n :: Data.Nat.Nat) Data.Type.Equality.~ ('Data.Nat.S m :: Data.Nat.Nat)) => Data.Semigroup.Traversable.Class.Traversable1 (Data.Vec.DataFamily.SpineStrict.Vec n) instance Data.Type.Nat.InlineInduction n => GHC.Base.Applicative (Data.Vec.DataFamily.SpineStrict.Vec n) instance Data.Type.Nat.InlineInduction n => GHC.Base.Monad (Data.Vec.DataFamily.SpineStrict.Vec n) instance Data.Type.Nat.InlineInduction n => Data.Distributive.Distributive (Data.Vec.DataFamily.SpineStrict.Vec n) instance Data.Type.Nat.InlineInduction n => Data.Functor.Rep.Representable (Data.Vec.DataFamily.SpineStrict.Vec n) instance (GHC.Base.Semigroup a, Data.Type.Nat.InlineInduction n) => GHC.Base.Semigroup (Data.Vec.DataFamily.SpineStrict.Vec n a) instance (GHC.Base.Monoid a, Data.Type.Nat.InlineInduction n) => GHC.Base.Monoid (Data.Vec.DataFamily.SpineStrict.Vec n a) instance Data.Type.Nat.InlineInduction n => Data.Functor.Bind.Class.Apply (Data.Vec.DataFamily.SpineStrict.Vec n) instance Data.Type.Nat.InlineInduction n => Data.Functor.Bind.Class.Bind (Data.Vec.DataFamily.SpineStrict.Vec n) instance Data.Type.Nat.InlineInduction n => Control.Lens.Indexed.FunctorWithIndex (Data.Fin.Fin n) (Data.Vec.DataFamily.SpineStrict.Vec n) instance Data.Type.Nat.InlineInduction n => Control.Lens.Indexed.FoldableWithIndex (Data.Fin.Fin n) (Data.Vec.DataFamily.SpineStrict.Vec n) instance Data.Type.Nat.InlineInduction n => Control.Lens.Indexed.TraversableWithIndex (Data.Fin.Fin n) (Data.Vec.DataFamily.SpineStrict.Vec n) instance Data.Type.Nat.InlineInduction n => Control.Lens.Each.Each (Data.Vec.DataFamily.SpineStrict.Vec n a) (Data.Vec.DataFamily.SpineStrict.Vec n b) a b instance Control.Lens.At.Ixed (Data.Vec.DataFamily.SpineStrict.Vec n a) instance Control.Lens.Tuple.Field1 (Data.Vec.DataFamily.SpineStrict.Vec ('Data.Nat.S n) a) (Data.Vec.DataFamily.SpineStrict.Vec ('Data.Nat.S n) a) a a instance Control.Lens.Tuple.Field2 (Data.Vec.DataFamily.SpineStrict.Vec ('Data.Nat.S ('Data.Nat.S n)) a) (Data.Vec.DataFamily.SpineStrict.Vec ('Data.Nat.S ('Data.Nat.S n)) a) a a instance Control.Lens.Tuple.Field3 (Data.Vec.DataFamily.SpineStrict.Vec ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S n))) a) (Data.Vec.DataFamily.SpineStrict.Vec ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S n))) a) a a instance Control.Lens.Tuple.Field4 (Data.Vec.DataFamily.SpineStrict.Vec ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S n)))) a) (Data.Vec.DataFamily.SpineStrict.Vec ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S n)))) a) a a instance Control.Lens.Tuple.Field5 (Data.Vec.DataFamily.SpineStrict.Vec ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S n))))) a) (Data.Vec.DataFamily.SpineStrict.Vec ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S n))))) a) a a instance Control.Lens.Tuple.Field6 (Data.Vec.DataFamily.SpineStrict.Vec ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S n)))))) a) (Data.Vec.DataFamily.SpineStrict.Vec ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S n)))))) a) a a instance Control.Lens.Tuple.Field7 (Data.Vec.DataFamily.SpineStrict.Vec ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S n))))))) a) (Data.Vec.DataFamily.SpineStrict.Vec ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S n))))))) a) a a instance Control.Lens.Tuple.Field8 (Data.Vec.DataFamily.SpineStrict.Vec ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S n)))))))) a) (Data.Vec.DataFamily.SpineStrict.Vec ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S n)))))))) a) a a instance Control.Lens.Tuple.Field9 (Data.Vec.DataFamily.SpineStrict.Vec ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S n))))))))) a) (Data.Vec.DataFamily.SpineStrict.Vec ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S ('Data.Nat.S n))))))))) a) a a module Data.Vec.DataFamily.SpineStrict.Pigeonhole -- | Generic pigeonholes. -- -- Examples: -- -- 
--   >>> from (Identity 'a')
--   'a' ::: VNil
--
-- -- 
--   >>> data Values a = Values a a a deriving (Generic1)
--   
--   >>> instance Pigeonhole Values
--   
--   >>> from (Values 1 2 3)
--   1 ::: 2 ::: 3 ::: VNil
--
class Pigeonhole f where { -- | The size of a pigeonhole type family PigeonholeSize f :: Nat; type PigeonholeSize f = GPigeonholeSize f; } -- | Converts a value to vector from :: Pigeonhole f => f x -> Vec (PigeonholeSize f) x -- | Converts a value to vector from :: (Pigeonhole f, Generic1 f, GFrom f, PigeonholeSize f ~ GPigeonholeSize f) => f x -> Vec (PigeonholeSize f) x -- | Converts back from vector. to :: Pigeonhole f => Vec (PigeonholeSize f) x -> f x -- | Converts back from vector. to :: (Pigeonhole f, Generic1 f, GTo f, PigeonholeSize f ~ GPigeonholeSize f) => Vec (PigeonholeSize f) x -> f x -- | Index. -- -- 
--   >>> gindex (Identity 'y') (Proxy :: Proxy Int)
--   'y'
--
-- -- 
--   >>> data Key = Key1 | Key2 | Key3 deriving (Generic)
--   
--   >>> data Values a = Values a a a deriving (Generic1)
--
-- -- 
--   >>> gindex (Values 'a' 'b' 'c') Key2
--   'b'
--
gindex :: (Generic i, GFrom i, Generic1 f, GFrom f, GEnumSize i ~ GPigeonholeSize f, InlineInduction (GPigeonholeSize f)) => f a -> i -> a -- | Tabulate. -- -- 
--   >>> tabulate (\() -> 'x') :: Identity Char
--   Identity 'x'
--
-- -- 
--   >>> tabulate absurd :: Proxy Integer
--   Proxy
--
-- -- 
--   >>> tabulate absurd :: Proxy Integer
--   Proxy
--
gtabulate :: (Generic i, GTo i, Generic1 f, GTo f, GEnumSize i ~ GPigeonholeSize f, InlineInduction (GPigeonholeSize f)) => (i -> a) -> f a -- | Generic traverse. -- -- Don't use, rather use DeriveTraversable gtraverse :: (Generic1 t, GFrom t, GTo t, InlineInduction (GPigeonholeSize t), Applicative f) => (a -> f b) -> t a -> f (t b) -- | Traverse with index. -- -- 
--   >>> data Key = Key1 | Key2 | Key3 deriving (Show, Generic)
--   
--   >>> data Values a = Values a a a deriving (Generic1)
--
-- -- 
--   >>> gitraverse (\i a -> Const [(i :: Key, a)]) (Values 'a' 'b' 'c')
--   Const [(Key1,'a'),(Key2,'b'),(Key3,'c')]
--
gitraverse :: (Generic i, GTo i, Generic1 t, GFrom t, GTo t, GEnumSize i ~ GPigeonholeSize t, InlineInduction (GPigeonholeSize t), Applicative f) => (i -> a -> f b) -> t a -> f (t b) -- | Generic version of from. gfrom :: (Generic1 c, GFrom c) => c a -> Vec (GPigeonholeSize c) a -- | Constraint for the class that computes gfrom. type GFrom c = GFromRep1 (Rep1 c) -- | Generic version of to. gto :: forall c a. (Generic1 c, GTo c) => Vec (GPigeonholeSize c) a -> c a -- | Constraint for the class that computes gto. type GTo c = GToRep1 (Rep1 c) -- | Compute the size from the type. type GPigeonholeSize c = PigeonholeSizeRep (Rep1 c) Nat0 instance Data.Vec.DataFamily.SpineStrict.Pigeonhole.Pigeonhole Data.Functor.Identity.Identity instance Data.Vec.DataFamily.SpineStrict.Pigeonhole.Pigeonhole (Data.Proxy.Proxy *) instance (Data.Vec.DataFamily.SpineStrict.Pigeonhole.Pigeonhole f, Data.Vec.DataFamily.SpineStrict.Pigeonhole.Pigeonhole g, Data.Type.Nat.InlineInduction (Data.Vec.DataFamily.SpineStrict.Pigeonhole.PigeonholeSize f)) => Data.Vec.DataFamily.SpineStrict.Pigeonhole.Pigeonhole (Data.Functor.Product.Product * f g) instance Data.Vec.DataFamily.SpineStrict.Pigeonhole.GToRep1 a => Data.Vec.DataFamily.SpineStrict.Pigeonhole.GToRep1 (GHC.Generics.M1 * d c a) instance (Data.Vec.DataFamily.SpineStrict.Pigeonhole.GToRep1 a, Data.Vec.DataFamily.SpineStrict.Pigeonhole.GToRep1 b) => Data.Vec.DataFamily.SpineStrict.Pigeonhole.GToRep1 ((GHC.Generics.:*:) * a b) instance Data.Vec.DataFamily.SpineStrict.Pigeonhole.GToRep1 GHC.Generics.Par1 instance Data.Vec.DataFamily.SpineStrict.Pigeonhole.GToRep1 (GHC.Generics.U1 *) instance (Data.Vec.DataFamily.SpineStrict.Pigeonhole.GFromRep1 a, Data.Vec.DataFamily.SpineStrict.Pigeonhole.GFromRep1 b) => Data.Vec.DataFamily.SpineStrict.Pigeonhole.GFromRep1 ((GHC.Generics.:*:) * a b) instance Data.Vec.DataFamily.SpineStrict.Pigeonhole.GFromRep1 a => Data.Vec.DataFamily.SpineStrict.Pigeonhole.GFromRep1 (GHC.Generics.M1 * d c a) instance Data.Vec.DataFamily.SpineStrict.Pigeonhole.GFromRep1 GHC.Generics.Par1 instance Data.Vec.DataFamily.SpineStrict.Pigeonhole.GFromRep1 (GHC.Generics.U1 *)