vec-0: Nat, Fin and Vec types.

Safe HaskellNone
LanguageHaskell2010

Data.Vec.Lazy.Inline

Contents

Description

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.

Synopsis

Documentation

data Vec n a where Source #

Vector, i.e. length-indexed list.

Constructors

VNil :: Vec Z a 
(:::) :: a -> Vec n a -> Vec (S n) a infixr 5 

Instances

SNatI n => Monad (Vec n) Source # 

Methods

(>>=) :: Vec n a -> (a -> Vec n b) -> Vec n b #

(>>) :: Vec n a -> Vec n b -> Vec n b #

return :: a -> Vec n a #

fail :: String -> Vec n a #

Functor (Vec n) Source # 

Methods

fmap :: (a -> b) -> Vec n a -> Vec n b #

(<$) :: a -> Vec n b -> Vec n a #

SNatI n => Applicative (Vec n) Source # 

Methods

pure :: a -> Vec n a #

(<*>) :: Vec n (a -> b) -> Vec n a -> Vec n b #

(*>) :: Vec n a -> Vec n b -> Vec n b #

(<*) :: Vec n a -> Vec n b -> Vec n a #

Foldable (Vec n) Source # 

Methods

fold :: Monoid m => Vec n m -> m #

foldMap :: Monoid m => (a -> m) -> Vec n a -> m #

foldr :: (a -> b -> b) -> b -> Vec n a -> b #

foldr' :: (a -> b -> b) -> b -> Vec n a -> b #

foldl :: (b -> a -> b) -> b -> Vec n a -> b #

foldl' :: (b -> a -> b) -> b -> Vec n a -> b #

foldr1 :: (a -> a -> a) -> Vec n a -> a #

foldl1 :: (a -> a -> a) -> Vec n a -> a #

toList :: Vec n a -> [a] #

null :: Vec n a -> Bool #

length :: Vec n a -> Int #

elem :: Eq a => a -> Vec n a -> Bool #

maximum :: Ord a => Vec n a -> a #

minimum :: Ord a => Vec n a -> a #

sum :: Num a => Vec n a -> a #

product :: Num a => Vec n a -> a #

Traversable (Vec n) Source # 

Methods

traverse :: Applicative f => (a -> f b) -> Vec n a -> f (Vec n b) #

sequenceA :: Applicative f => Vec n (f a) -> f (Vec n a) #

mapM :: Monad m => (a -> m b) -> Vec n a -> m (Vec n b) #

sequence :: Monad m => Vec n (m a) -> m (Vec n a) #

SNatI n => Distributive (Vec n) Source # 

Methods

distribute :: Functor f => f (Vec n a) -> Vec n (f a) #

collect :: Functor f => (a -> Vec n b) -> f a -> Vec n (f b) #

distributeM :: Monad m => m (Vec n a) -> Vec n (m a) #

collectM :: Monad m => (a -> Vec n b) -> m a -> Vec n (m b) #

SNatI n => Representable (Vec n) Source # 

Associated Types

type Rep (Vec n :: * -> *) :: * #

Methods

tabulate :: (Rep (Vec n) -> a) -> Vec n a #

index :: Vec n a -> Rep (Vec n) -> a #

(~) Nat n (S m) => Traversable1 (Vec n) Source # 

Methods

traverse1 :: Apply f => (a -> f b) -> Vec n a -> f (Vec n b) #

sequence1 :: Apply f => Vec n (f b) -> f (Vec n b) #

Apply (Vec n) Source # 

Methods

(<.>) :: Vec n (a -> b) -> Vec n a -> Vec n b #

(.>) :: Vec n a -> Vec n b -> Vec n b #

(<.) :: Vec n a -> Vec n b -> Vec n a #

Bind (Vec n) Source # 

Methods

(>>-) :: Vec n a -> (a -> Vec n b) -> Vec n b #

join :: Vec n (Vec n a) -> Vec n a #

(~) Nat n (S m) => Foldable1 (Vec n) Source # 

Methods

fold1 :: Semigroup m => Vec n m -> m #

foldMap1 :: Semigroup m => (a -> m) -> Vec n a -> m #

toNonEmpty :: Vec n a -> NonEmpty a #

FunctorWithIndex (Fin n) (Vec n) Source # 

Methods

imap :: (Fin n -> a -> b) -> Vec n a -> Vec n b #

imapped :: (Indexable (Fin n) p, Settable f) => p a (f b) -> Vec n a -> f (Vec n b) #

FoldableWithIndex (Fin n) (Vec n) Source # 

Methods

ifoldMap :: Monoid m => (Fin n -> a -> m) -> Vec n a -> m #

ifolded :: (Indexable (Fin n) p, Contravariant f, Applicative f) => p a (f a) -> Vec n a -> f (Vec n a) #

ifoldr :: (Fin n -> a -> b -> b) -> b -> Vec n a -> b #

ifoldl :: (Fin n -> b -> a -> b) -> b -> Vec n a -> b #

ifoldr' :: (Fin n -> a -> b -> b) -> b -> Vec n a -> b #

ifoldl' :: (Fin n -> b -> a -> b) -> b -> Vec n a -> b #

TraversableWithIndex (Fin n) (Vec n) Source # 

Methods

itraverse :: Applicative f => (Fin n -> a -> f b) -> Vec n a -> f (Vec n b) #

itraversed :: (Indexable (Fin n) p, Applicative f) => p a (f b) -> Vec n a -> f (Vec n b) #

Eq a => Eq (Vec n a) Source # 

Methods

(==) :: Vec n a -> Vec n a -> Bool #

(/=) :: Vec n a -> Vec n a -> Bool #

Ord a => Ord (Vec n a) Source # 

Methods

compare :: Vec n a -> Vec n a -> Ordering #

(<) :: Vec n a -> Vec n a -> Bool #

(<=) :: Vec n a -> Vec n a -> Bool #

(>) :: Vec n a -> Vec n a -> Bool #

(>=) :: Vec n a -> Vec n a -> Bool #

max :: Vec n a -> Vec n a -> Vec n a #

min :: Vec n a -> Vec n a -> Vec n a #

Show a => Show (Vec n a) Source # 

Methods

showsPrec :: Int -> Vec n a -> ShowS #

show :: Vec n a -> String #

showList :: [Vec n a] -> ShowS #

Semigroup a => Semigroup (Vec n a) Source # 

Methods

(<>) :: Vec n a -> Vec n a -> Vec n a #

sconcat :: NonEmpty (Vec n a) -> Vec n a #

stimes :: Integral b => b -> Vec n a -> Vec n a #

(Monoid a, SNatI n) => Monoid (Vec n a) Source # 

Methods

mempty :: Vec n a #

mappend :: Vec n a -> Vec n a -> Vec n a #

mconcat :: [Vec n a] -> Vec n a #

(~) Nat n Z => Boring (Vec n a) Source # 

Methods

boring :: Vec n a #

NFData a => NFData (Vec n a) Source # 

Methods

rnf :: Vec n a -> () #

Hashable a => Hashable (Vec n a) Source # 

Methods

hashWithSalt :: Int -> Vec n a -> Int #

hash :: Vec n a -> Int #

Ixed (Vec n a) Source #

Vec doesn't have At instance, as we cannot remove value from Vec. See ix in Data.Vec.Lazy module for an Lens (not Traversal).

Methods

ix :: Index (Vec n a) -> Traversal' (Vec n a) (IxValue (Vec n a)) #

Each (Vec n a) (Vec n b) a b Source # 

Methods

each :: Traversal (Vec n a) (Vec n b) a b #

Field1 (Vec (S n) a) (Vec (S n) a) a a Source # 

Methods

_1 :: Lens (Vec (S n) a) (Vec (S n) a) a a #

Field2 (Vec (S (S n)) a) (Vec (S (S n)) a) a a Source # 

Methods

_2 :: Lens (Vec (S (S n)) a) (Vec (S (S n)) a) a a #

Field3 (Vec (S (S (S n))) a) (Vec (S (S (S n))) a) a a Source # 

Methods

_3 :: Lens (Vec (S (S (S n))) a) (Vec (S (S (S n))) a) a a #

Field4 (Vec (S (S (S (S n)))) a) (Vec (S (S (S (S n)))) a) a a Source # 

Methods

_4 :: Lens (Vec (S (S (S (S n)))) a) (Vec (S (S (S (S n)))) a) a a #

Field5 (Vec (S (S (S (S (S n))))) a) (Vec (S (S (S (S (S n))))) a) a a Source # 

Methods

_5 :: Lens (Vec (S (S (S (S (S n))))) a) (Vec (S (S (S (S (S n))))) a) a a #

Field6 (Vec (S (S (S (S (S (S n)))))) a) (Vec (S (S (S (S (S (S n)))))) a) a a Source # 

Methods

_6 :: Lens (Vec (S (S (S (S (S (S n)))))) a) (Vec (S (S (S (S (S (S n)))))) a) a a #

Field7 (Vec (S (S (S (S (S (S (S n))))))) a) (Vec (S (S (S (S (S (S (S n))))))) a) a a Source # 

Methods

_7 :: Lens (Vec (S (S (S (S (S (S (S n))))))) a) (Vec (S (S (S (S (S (S (S n))))))) a) a a #

Field8 (Vec (S (S (S (S (S (S (S (S n)))))))) a) (Vec (S (S (S (S (S (S (S (S n)))))))) a) a a Source # 

Methods

_8 :: Lens (Vec (S (S (S (S (S (S (S (S n)))))))) a) (Vec (S (S (S (S (S (S (S (S n)))))))) a) a a #

Field9 (Vec (S (S (S (S (S (S (S (S (S n))))))))) a) (Vec (S (S (S (S (S (S (S (S (S n))))))))) a) a a Source # 

Methods

_9 :: Lens (Vec (S (S (S (S (S (S (S (S (S n))))))))) a) (Vec (S (S (S (S (S (S (S (S (S n))))))))) a) a a #

type Rep (Vec n) Source # 
type Rep (Vec n) = Fin n
type Index (Vec n a) Source # 
type Index (Vec n a) = Fin n
type IxValue (Vec n a) Source # 
type IxValue (Vec n a) = a

Construction

empty :: Vec Z a Source #

Empty Vec.

singleton :: a -> Vec (S Z) a Source #

Vec with exactly one element.

>>> singleton True
True ::: VNil

Conversions

toPull :: forall n a. InlineInduction n => Vec n a -> Vec n a Source #

Convert to pull Vec.

fromPull :: forall n a. InlineInduction n => Vec n a -> Vec n a Source #

Convert from pull Vec.

_Pull :: InlineInduction n => Iso (Vec n a) (Vec n b) (Vec n a) (Vec n b) Source #

An Iso from toPull and fromPull.

toList :: forall n a. InlineInduction n => Vec n a -> [a] Source #

Convert Vec to list.

>>> toList $ 'f' ::: 'o' ::: 'o' ::: VNil
"foo"

fromList :: InlineInduction n => [a] -> Maybe (Vec n a) Source #

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

_Vec :: InlineInduction n => Prism' [a] (Vec n a) Source #

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]

fromListPrefix :: InlineInduction n => [a] -> Maybe (Vec n a) Source #

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

reifyList :: [a] -> (forall n. InlineInduction n => Vec n a -> r) -> r Source #

Reify any list [a] to Vec n a.

>>> reifyList "foo" length
3

Indexing

(!) :: InlineInduction n => Vec n a -> Fin n -> a Source #

Indexing.

>>> ('a' ::: 'b' ::: 'c' ::: VNil) ! F.S F.Z
'b'

ix :: InlineInduction n => Fin n -> Lens' (Vec n a) a Source #

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

_Cons :: Iso (Vec (S n) a) (Vec (S n) b) (a, Vec n a) (b, Vec n b) Source #

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.

_head :: Lens' (Vec (S n) a) a Source #

Head lens. Note: lens _head is a Traversal'.

>>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. _head
'a'
>>> ('a' ::: 'b' ::: 'c' ::: VNil) & _head .~ 'x'
'x' ::: 'b' ::: 'c' ::: VNil

_tail :: Lens' (Vec (S n) a) (Vec n a) Source #

Head lens. Note: lens _head is a Traversal'.

cons :: a -> Vec n a -> Vec (S n) a Source #

Cons an element in front of a Vec.

head :: Vec (S n) a -> a Source #

The first element of a Vec.

tail :: Vec (S n) a -> Vec n a Source #

The elements after the head of a Vec.

Concatenation and splitting

(++) :: forall n m a. InlineInduction n => Vec n a -> Vec m a -> Vec (Plus n m) a infixr 5 Source #

Append two Vec.

>>> ('a' ::: 'b' ::: VNil) ++ ('c' ::: 'd' ::: VNil)
'a' ::: 'b' ::: 'c' ::: 'd' ::: VNil

split :: InlineInduction n => Vec (Plus n m) a -> (Vec n a, Vec m a) Source #

Split vector into two parts. Inverse of ++.

>>> split ('a' ::: 'b' ::: 'c' ::: VNil) :: (Vec N.Nat1 Char, Vec N.Nat2 Char)
('a' ::: VNil,'b' ::: 'c' ::: VNil)
>>> uncurry (++) (split ('a' ::: 'b' ::: 'c' ::: VNil) :: (Vec N.Nat1 Char, Vec N.Nat2 Char))
'a' ::: 'b' ::: 'c' ::: VNil

concatMap :: forall a b n m. (InlineInduction m, InlineInduction n) => (a -> Vec m b) -> Vec n a -> Vec (Mult n m) b Source #

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

chunks :: (InlineInduction n, InlineInduction m) => Vec (Mult n m) a -> Vec n (Vec m a) Source #

Inverse of concat.

>>> chunks <$> fromListPrefix [1..] :: Maybe (Vec N.Nat2 (Vec N.Nat3 Int))
Just ((1 ::: 2 ::: 3 ::: VNil) ::: (4 ::: 5 ::: 6 ::: VNil) ::: VNil)
>>> let idVec x = x :: Vec N.Nat2 (Vec N.Nat3 Int)
>>> concat . idVec . chunks <$> fromListPrefix [1..]
Just (1 ::: 2 ::: 3 ::: 4 ::: 5 ::: 6 ::: VNil)

Folds

foldMap :: (Monoid m, InlineInduction n) => (a -> m) -> Vec n a -> m Source #

foldMap1 :: forall s a n. (Semigroup s, InlineInduction n) => (a -> s) -> Vec (S n) a -> s Source #

ifoldMap :: forall a n m. (Monoid m, InlineInduction n) => (Fin n -> a -> m) -> Vec n a -> m Source #

ifoldMap1 :: forall a n s. (Semigroup s, InlineInduction n) => (Fin (S n) -> a -> s) -> Vec (S n) a -> s Source #

There is no type-class for this :(

foldr :: forall a b n. InlineInduction n => (a -> b -> b) -> b -> Vec n a -> b Source #

Right fold.

ifoldr :: forall a b n. InlineInduction n => (Fin n -> a -> b -> b) -> b -> Vec n a -> b Source #

Right fold with an index.

Special folds

length :: forall n a. InlineInduction n => Vec n a -> Int Source #

Yield the length of a Vec. O(n)

null :: Vec n a -> Bool Source #

Test whether a Vec is empty. O(1)

sum :: (Num a, InlineInduction n) => Vec n a -> a Source #

Non-strict sum.

product :: (Num a, InlineInduction n) => Vec n a -> a Source #

Non-strict product.

Mapping

map :: forall a b n. InlineInduction n => (a -> b) -> Vec n a -> Vec n b Source #

>>> map not $ True ::: False ::: VNil
False ::: True ::: VNil

imap :: InlineInduction n => (Fin n -> a -> b) -> Vec n a -> Vec n b Source #

>>> imap (,) $ 'a' ::: 'b' ::: 'c' ::: VNil
(0,'a') ::: (1,'b') ::: (2,'c') ::: VNil

traverse :: forall n f a b. (Applicative f, InlineInduction n) => (a -> f b) -> Vec n a -> f (Vec n b) Source #

Apply an action to every element of a 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) Source #

Apply an action to non-empty Vec, 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) Source #

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 () Source #

Apply an action to every element of a Vec and its index, ignoring the results.

Zipping

zipWith :: forall a b c n. InlineInduction n => (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c Source #

Zip two Vecs with a function.

izipWith :: InlineInduction n => (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c Source #

Zip two Vecs. with a function that also takes the elements' indices.

Monadic

bind :: InlineInduction n => Vec n a -> (a -> Vec n b) -> Vec n b Source #

Monadic bind.

join :: InlineInduction n => Vec n (Vec n a) -> Vec n a Source #

Monadic join.

>>> join $ ('a' ::: 'b' ::: VNil) ::: ('c' ::: 'd' ::: VNil) ::: VNil
'a' ::: 'd' ::: VNil

Universe

universe :: InlineInduction n => Vec n (Fin n) Source #

Get all Fin n in a Vec n.

>>> universe :: Vec N.Nat3 (Fin N.Nat3)
0 ::: 1 ::: 2 ::: VNil

VecEach

class Each s t a b => VecEach s t a b | s -> a, t -> b, s b -> t, t a -> s where Source #

Write functions on Vec. Use them with tuples.

VecEach can be used to avoid "this function won't change the length of the list" in DSLs.

bad: Instead of

[x, y] <- badDslMagic ["foo", "bar"]  -- list!

good: we can write

(x, y) <- betterDslMagic ("foo", "bar") -- homogenic tuple!

where betterDslMagic can be defined using traverseWithVec.

Minimal complete definition

mapWithVec, traverseWithVec

Methods

mapWithVec :: (forall n. InlineInduction n => Vec n a -> Vec n b) -> s -> t Source #

traverseWithVec :: Applicative f => (forall n. InlineInduction n => Vec n a -> f (Vec n b)) -> s -> f t Source #

Instances

((~) * a a', (~) * b b') => VecEach (a, a') (b, b') a b Source # 

Methods

mapWithVec :: (forall n. InlineInduction n => Vec n a -> Vec n b) -> (a, a') -> (b, b') Source #

traverseWithVec :: Applicative f => (forall n. InlineInduction n => Vec n a -> f (Vec n b)) -> (a, a') -> f (b, b') Source #

((~) * a a2, (~) * a a3, (~) * b b2, (~) * b b3) => VecEach (a, a2, a3) (b, b2, b3) a b Source # 

Methods

mapWithVec :: (forall n. InlineInduction n => Vec n a -> Vec n b) -> (a, a2, a3) -> (b, b2, b3) Source #

traverseWithVec :: Applicative f => (forall n. InlineInduction n => Vec n a -> f (Vec n b)) -> (a, a2, a3) -> f (b, b2, b3) Source #

((~) * a a2, (~) * a a3, (~) * a a4, (~) * b b2, (~) * b b3, (~) * b b4) => VecEach (a, a2, a3, a4) (b, b2, b3, b4) a b Source # 

Methods

mapWithVec :: (forall n. InlineInduction n => Vec n a -> Vec n b) -> (a, a2, a3, a4) -> (b, b2, b3, b4) Source #

traverseWithVec :: Applicative f => (forall n. InlineInduction n => Vec n a -> f (Vec n b)) -> (a, a2, a3, a4) -> f (b, b2, b3, b4) Source #