-- 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 three flavours: -- --

naive: with explicit recursion. It's simple, -- constraint-less, yet slow.
pull: using Fin n -> a representation, which -- fuses well, but makes some programs hard to write. And
inline: which exploits how GHC dictionary inlining works, -- unrolling recursion if the size of Vec is known -- statically.

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

-- --

linear has V type, which uses Vector from -- vector package as backing store. Vec is a real GADT, -- but tries to provide as many useful instances (upto -- lens).
vector-sized Great package using GHC.TypeLits. -- Current version (0.6.1.0) uses finite-typelits and -- Int indexes.
sized-vector depends on singletons package. -- vec isn't light on dependencies either, but try to provide -- wide GHC support.
fixed-vector
sized also depends on a singletons package. The -- Sized f n a type is generalisation of linear's -- V for any ListLike.
clash-prelude is a kitchen sink package, which has -- CLaSH.Sized.Vector module. Also depends on -- singletons.

@package vec @version 0.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 (F.S F.Z)
--   'b'
--

-- --

--   >>> ('a' L.::: 'b' L.::: 'c' L.::: L.VNil) & L._Pull . ix (F.S F.Z) .~ '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 Data.Semigroup.Semigroup a => Data.Semigroup.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 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 -- | 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) ! F.S F.Z
--   'b'
--

(!) :: Vec n a -> Fin n -> a -- | Index lens. -- --

--   >>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. ix (F.S F.Z)
--   'b'
--

-- --

--   >>> ('a' ::: 'b' ::: 'c' ::: VNil) & ix (F.S F.Z) .~ 'x'
--   'a' ::: 'x' ::: 'c' ::: VNil
--

--   >>> ('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 ~ a', b ~ b') => Data.Vec.Lazy.VecEach (a, a') (b, b') a b instance (a ~ a2, a ~ a3, b ~ b2, b ~ b3) => Data.Vec.Lazy.VecEach (a, a2, a3) (b, b2, b3) a b instance (a ~ a2, a ~ a3, a ~ a4, b ~ b2, b ~ b3, b ~ 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.S m => Data.Semigroup.Foldable.Class.Foldable1 (Data.Vec.Lazy.Vec n) instance Data.Traversable.Traversable (Data.Vec.Lazy.Vec n) instance n ~ 'Data.Nat.S m => 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 Data.Semigroup.Semigroup a => Data.Semigroup.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 -- | 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) ! F.S F.Z
--   'b'
--

(!) :: InlineInduction n => Vec n a -> Fin n -> a -- | Index lens. -- --

--   >>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. ix (F.S F.Z)
--   'b'
--

-- --

--   >>> ('a' ::: 'b' ::: 'c' ::: VNil) & ix (F.S F.Z) .~ '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
--

--   >>> ('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!
--