-- 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:
--
--
-- - 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
-- - data-family: which allows lazy pattern matching
-- - 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.
--
-- 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
--
--
-- - 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.3
-- | 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)
-- | 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
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. InlineInduction n => Vec n a -> 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
-- | Reverse Vec.
reverse :: forall n a. InlineInduction 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 (Data.Type.Nat.SNatI m, (n :: Data.Nat.Nat) Data.Type.Equality.~ ('Data.Nat.S m :: Data.Nat.Nat)) => Data.Semigroup.Foldable.Class.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)
-- | 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
-- | 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)
-- | 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
-- | 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 elements after the head of a Vec.
tail :: 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
-- | 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
-- | 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. 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 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.Foldable.Class.Foldable1 (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 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
-- 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
-- | 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)
-- | 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
-- | Tabulating, inverse of !.
--
--
-- >>> tabulate id :: Vec N.Nat3 (Fin N.Nat3)
-- 0 ::: 1 ::: 2 ::: VNil
--
tabulate :: InlineInduction 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. InlineInduction n => Vec n a -> 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)
-- | Reverse Vec.
--
--
-- >>> reverse ('a' ::: 'b' ::: 'c' ::: VNil)
-- 'c' ::: 'b' ::: 'a' ::: VNil
--
reverse :: forall n a. InlineInduction n => Vec n a -> Vec n 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
-- | Repeat value
--
--
-- >>> repeat 'x' :: Vec N.Nat3 Char
-- 'x' ::: 'x' ::: 'x' ::: VNil
--
repeat :: InlineInduction n => x -> Vec n x
-- | 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.
--
-- 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. 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
-- | 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)
-- | 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
-- | Tabulating, inverse of !.
--
--
-- >>> tabulate id :: Vec N.Nat3 (Fin N.Nat3)
-- 0 ::: 1 ::: 2 ::: VNil
--
tabulate :: InlineInduction 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. InlineInduction n => Vec n a -> 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
-- | Reverse Vec.
--
--
-- >>> reverse ('a' ::: 'b' ::: 'c' ::: VNil)
-- 'c' ::: 'b' ::: 'a' ::: VNil
--
reverse :: forall n a. InlineInduction 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. 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
-- | Repeat value
--
--
-- >>> repeat 'x' :: Vec N.Nat3 Char
-- 'x' ::: 'x' ::: 'x' ::: VNil
--
repeat :: InlineInduction n => x -> Vec n x
-- | 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.
--
-- 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 :: 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 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 => Data.Traversable.Traversable (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.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)
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.
--
--
-- >>> gtabulate (\() -> 'x') :: Identity Char
-- Identity 'x'
--
--
--
-- >>> gtabulate absurd :: Proxy Integer
-- Proxy
--
--
--
-- >>> gtabulate absurd :: Proxy Integer
-- Proxy
--
gtabulate :: (Generic i, GTo i, Generic1 f, GTo f, GEnumSize i ~ GPigeonholeSize f, InlineInduction (GPigeonholeSize f)) => (i -> a) -> f a
-- | A lens. i -> Lens' (t a) a
--
--
-- >>> Lens.view (gix ()) (Identity 'x')
-- 'x'
--
--
--
-- >>> Lens.over (gix ()) toUpper (Identity 'x')
-- Identity 'X'
--
gix :: (Generic i, GFrom i, Generic1 t, GTo t, GFrom t, GEnumSize i ~ GPigeonholeSize t, InlineInduction (GPigeonholeSize t), Functor f) => i -> (a -> f a) -> t a -> f (t 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 *)