Data.Sized

This module provides the functionality to make length-parametrized types from existing CFreeMonoid sequential types.

Most of the complexity of operations for Sized f n a are the same as original operations for f. For example, !! is O(1) for Sized Vector n a but O(i) for Sized [] n a.

This module also provides powerful view types and pattern synonyms to inspect the sized sequence. See Views and Patterns for more detail.

Main Data-types

data Sized (f :: Type -> Type) (n :: nat) a

Sized wraps a sequential type f and makes length-parametrized version.

Here, f must be the instance of CFreeMonoid (f a) a for all a@.

Since 0.2.0.0

Instances

(Integral i, FunctorWithIndex i f, HasOrdinal nat, SingI n) => FunctorWithIndex (Ordinal n) (Sized f n)

Since 0.2.0.0

Defined in Data.Sized.Internal

Methods

imap :: (Ordinal n -> a -> b) -> Sized f n a -> Sized f n b

imapped :: IndexedSetter (Ordinal n) (Sized f n a) (Sized f n b) a b

(Integral i, FoldableWithIndex i f, HasOrdinal nat, SingI n) => FoldableWithIndex (Ordinal n) (Sized f n)

Since 0.4.0.0

Defined in Data.Sized.Internal

Methods

ifoldMap :: Monoid m => (Ordinal n -> a -> m) -> Sized f n a -> m

ifolded :: IndexedFold (Ordinal n) (Sized f n a) a

ifoldr :: (Ordinal n -> a -> b -> b) -> b -> Sized f n a -> b

ifoldl :: (Ordinal n -> b -> a -> b) -> b -> Sized f n a -> b

ifoldr' :: (Ordinal n -> a -> b -> b) -> b -> Sized f n a -> b

ifoldl' :: (Ordinal n -> b -> a -> b) -> b -> Sized f n a -> b

(Integral i, TraversableWithIndex i f, HasOrdinal nat, SingI n) => TraversableWithIndex (Ordinal n) (Sized f n)

Since 0.2.0.0

Defined in Data.Sized.Internal

Methods

itraverse :: Applicative f0 => (Ordinal n -> a -> f0 b) -> Sized f n a -> f0 (Sized f n b)

itraversed :: IndexedTraversal (Ordinal n) (Sized f n a) (Sized f n b) a b

Functor f => Functor (Sized f n)

Defined in Data.Sized.Internal

Methods

fmap :: (a -> b) -> Sized f n a -> Sized f n b

(<$) :: a -> Sized f n b -> Sized f n a

(Functor f, CFreeMonoid f, CZip f, HasOrdinal nat, SingI n, forall a. DomC f a) => Applicative (Sized f n)

Applicative instance, generalizing ZipList.

Defined in Data.Sized

Methods

pure :: a -> Sized f n a

(<*>) :: Sized f n (a -> b) -> Sized f n a -> Sized f n b

liftA2 :: (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c

(*>) :: Sized f n a -> Sized f n b -> Sized f n b

(<*) :: Sized f n a -> Sized f n b -> Sized f n a

Foldable f => Foldable (Sized f n)

Defined in Data.Sized.Internal

Methods

fold :: Monoid m => Sized f n m -> m

foldMap :: Monoid m => (a -> m) -> Sized f n a -> m

foldMap' :: Monoid m => (a -> m) -> Sized f n a -> m

foldr :: (a -> b -> b) -> b -> Sized f n a -> b

foldr' :: (a -> b -> b) -> b -> Sized f n a -> b

foldl :: (b -> a -> b) -> b -> Sized f n a -> b

foldl' :: (b -> a -> b) -> b -> Sized f n a -> b

foldr1 :: (a -> a -> a) -> Sized f n a -> a

foldl1 :: (a -> a -> a) -> Sized f n a -> a

toList :: Sized f n a -> [a]

null :: Sized f n a -> Bool

length :: Sized f n a -> Int

elem :: Eq a => a -> Sized f n a -> Bool

maximum :: Ord a => Sized f n a -> a

minimum :: Ord a => Sized f n a -> a

sum :: Num a => Sized f n a -> a

product :: Num a => Sized f n a -> a

Traversable f => Traversable (Sized f n)

Defined in Data.Sized.Internal

Methods

traverse :: Applicative f0 => (a -> f0 b) -> Sized f n a -> f0 (Sized f n b)

sequenceA :: Applicative f0 => Sized f n (f0 a) -> f0 (Sized f n a)

mapM :: Monad m => (a -> m b) -> Sized f n a -> m (Sized f n b)

sequence :: Monad m => Sized f n (m a) -> m (Sized f n a)

CFoldable f => CFoldable (Sized f n)

Defined in Data.Sized.Internal

Methods

cfoldMap :: (Dom (Sized f n) a, Monoid w) => (a -> w) -> Sized f n a -> w

cfoldMap' :: (Dom (Sized f n) a, Monoid m) => (a -> m) -> Sized f n a -> m

cfold :: (Dom (Sized f n) w, Monoid w) => Sized f n w -> w

cfoldr :: Dom (Sized f n) a => (a -> b -> b) -> b -> Sized f n a -> b

cfoldlM :: (Monad m, Dom (Sized f n) b) => (a -> b -> m a) -> a -> Sized f n b -> m a

cfoldlM' :: (Monad m, Dom (Sized f n) b) => (a -> b -> m a) -> a -> Sized f n b -> m a

cfoldrM :: (Monad m, Dom (Sized f n) a) => (a -> b -> m b) -> b -> Sized f n a -> m b

cfoldrM' :: (Monad m, Dom (Sized f n) a) => (a -> b -> m b) -> b -> Sized f n a -> m b

cfoldl :: Dom (Sized f n) a => (b -> a -> b) -> b -> Sized f n a -> b

cfoldr' :: Dom (Sized f n) a => (a -> b -> b) -> b -> Sized f n a -> b

cfoldl' :: Dom (Sized f n) a => (b -> a -> b) -> b -> Sized f n a -> b

cbasicToList :: Dom (Sized f n) a => Sized f n a -> [a]

cfoldr1 :: Dom (Sized f n) a => (a -> a -> a) -> Sized f n a -> a

cfoldl1 :: Dom (Sized f n) a => (a -> a -> a) -> Sized f n a -> a

cindex :: Dom (Sized f n) a => Sized f n a -> Int -> a

cnull :: Dom (Sized f n) a => Sized f n a -> Bool

clength :: Dom (Sized f n) a => Sized f n a -> Int

cany :: Dom (Sized f n) a => (a -> Bool) -> Sized f n a -> Bool

call :: Dom (Sized f n) a => (a -> Bool) -> Sized f n a -> Bool

celem :: (Eq a, Dom (Sized f n) a) => a -> Sized f n a -> Bool

cnotElem :: (Eq a, Dom (Sized f n) a) => a -> Sized f n a -> Bool

cminimum :: (Ord a, Dom (Sized f n) a) => Sized f n a -> a

cmaximum :: (Ord a, Dom (Sized f n) a) => Sized f n a -> a

csum :: (Num a, Dom (Sized f n) a) => Sized f n a -> a

cproduct :: (Num a, Dom (Sized f n) a) => Sized f n a -> a

cctraverse_ :: (CApplicative g, CPointed g, Dom g (), Dom (Sized f n) a, Dom g b) => (a -> g b) -> Sized f n a -> g ()

ctraverse_ :: (Applicative g, Dom (Sized f n) a) => (a -> g b) -> Sized f n a -> g ()

clast :: Dom (Sized f n) a => Sized f n a -> a

chead :: Dom (Sized f n) a => Sized f n a -> a

cfind :: Dom (Sized f n) a => (a -> Bool) -> Sized f n a -> Maybe a

cfindIndex :: Dom (Sized f n) a => (a -> Bool) -> Sized f n a -> Maybe Int

cfindIndices :: Dom (Sized f n) a => (a -> Bool) -> Sized f n a -> [Int]

celemIndex :: (Dom (Sized f n) a, Eq a) => a -> Sized f n a -> Maybe Int

celemIndices :: (Dom (Sized f n) a, Eq a) => a -> Sized f n a -> [Int]

CTraversable f => CTraversable (Sized f n)

Defined in Data.Sized

Methods

ctraverse :: (Dom (Sized f n) a, Dom (Sized f n) b, Applicative g) => (a -> g b) -> Sized f n a -> g (Sized f n b)

(CZip f, CFreeMonoid f) => CZip (Sized f n)

Defined in Data.Sized

Methods

czipWith :: (Dom (Sized f n) a, Dom (Sized f n) b, Dom (Sized f n) c) => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c

czip :: (Dom (Sized f n) a, Dom (Sized f n) b, Dom (Sized f n) (a, b)) => Sized f n a -> Sized f n b -> Sized f n (a, b)

(PeanoOrder nat, SingI n, CZip f, CFreeMonoid f) => CRepeat (Sized f n)

Defined in Data.Sized

Methods

crepeat :: Dom (Sized f n) a => a -> Sized f n a

(CFreeMonoid f, CZip f) => CApplicative (Sized f n)

Defined in Data.Sized

Methods

pair :: (Dom (Sized f n) a, Dom (Sized f n) b, Dom (Sized f n) (a, b)) => Sized f n a -> Sized f n b -> Sized f n (a, b)

(<.>) :: (Dom (Sized f n) a, Dom (Sized f n) b, Dom (Sized f n) (a -> b)) => Sized f n (a -> b) -> Sized f n a -> Sized f n b

(.>) :: (Dom (Sized f n) a, Dom (Sized f n) b) => Sized f n a -> Sized f n b -> Sized f n b

(<.) :: (Dom (Sized f n) a, Dom (Sized f n) b) => Sized f n a -> Sized f n b -> Sized f n a

(CFreeMonoid f, PeanoOrder nat, SingI n) => CPointed (Sized f n)

Defined in Data.Sized

Methods

cpure :: Dom (Sized f n) a => a -> Sized f n a

(CZip f, CFreeMonoid f) => CSemialign (Sized f n)

N.B. Since calign is just zipping for fixed n, we require more strong CZip constraint here.

Defined in Data.Sized

Methods

calignWith :: (Dom (Sized f n) a, Dom (Sized f n) b, Dom (Sized f n) c) => (These a b -> c) -> Sized f n a -> Sized f n b -> Sized f n c

calign :: (Dom (Sized f n) a, Dom (Sized f n) b, Dom (Sized f n) (These a b)) => Sized f n a -> Sized f n b -> Sized f n (These a b)

Constrained (Sized f n)

Defined in Data.Sized.Internal

Associated Types

type Dom (Sized f n) a

CFunctor f => CFunctor (Sized f n)

Defined in Data.Sized.Internal

Methods

cmap :: (Dom (Sized f n) a, Dom (Sized f n) b) => (a -> b) -> Sized f n a -> Sized f n b

(<$:) :: (Dom (Sized f n) a, Dom (Sized f n) b) => a -> Sized f n b -> Sized f n a

Eq (f a) => Eq (Sized f n a)

Defined in Data.Sized.Internal

Methods

(==) :: Sized f n a -> Sized f n a -> Bool

(/=) :: Sized f n a -> Sized f n a -> Bool

Ord (f a) => Ord (Sized f n a)

Defined in Data.Sized.Internal

Methods

compare :: Sized f n a -> Sized f n a -> Ordering

(<) :: Sized f n a -> Sized f n a -> Bool

(<=) :: Sized f n a -> Sized f n a -> Bool

(>) :: Sized f n a -> Sized f n a -> Bool

(>=) :: Sized f n a -> Sized f n a -> Bool

max :: Sized f n a -> Sized f n a -> Sized f n a

min :: Sized f n a -> Sized f n a -> Sized f n a

Show (f a) => Show (Sized f n a)

Defined in Data.Sized.Internal

Methods

showsPrec :: Int -> Sized f n a -> ShowS

show :: Sized f n a -> String

showList :: [Sized f n a] -> ShowS

NFData (f a) => NFData (Sized f n a)

Defined in Data.Sized.Internal

Methods

rnf :: Sized f n a -> ()

Hashable (f a) => Hashable (Sized f n a)

Defined in Data.Sized.Internal

Methods

hashWithSalt :: Int -> Sized f n a -> Int

hash :: Sized f n a -> Int

(Integral (Index (f a)), Ixed (f a), HasOrdinal nat) => Ixed (Sized f n a)

Defined in Data.Sized.Internal

Methods

ix :: Index (Sized f n a) -> Traversal' (Sized f n a) (IxValue (Sized f n a))

MonoFunctor (f a) => MonoFunctor (Sized f n a)

Since 0.2.0.0

Defined in Data.Sized.Internal

Methods

omap :: (Element (Sized f n a) -> Element (Sized f n a)) -> Sized f n a -> Sized f n a

MonoFoldable (f a) => MonoFoldable (Sized f n a)

Since 0.2.0.0

Defined in Data.Sized.Internal

Methods

ofoldMap :: Monoid m => (Element (Sized f n a) -> m) -> Sized f n a -> m

ofoldr :: (Element (Sized f n a) -> b -> b) -> b -> Sized f n a -> b

ofoldl' :: (a0 -> Element (Sized f n a) -> a0) -> a0 -> Sized f n a -> a0

otoList :: Sized f n a -> [Element (Sized f n a)]

oall :: (Element (Sized f n a) -> Bool) -> Sized f n a -> Bool

oany :: (Element (Sized f n a) -> Bool) -> Sized f n a -> Bool

onull :: Sized f n a -> Bool

olength :: Sized f n a -> Int

olength64 :: Sized f n a -> Int64

ocompareLength :: Integral i => Sized f n a -> i -> Ordering

otraverse_ :: Applicative f0 => (Element (Sized f n a) -> f0 b) -> Sized f n a -> f0 ()

ofor_ :: Applicative f0 => Sized f n a -> (Element (Sized f n a) -> f0 b) -> f0 ()

omapM_ :: Applicative m => (Element (Sized f n a) -> m ()) -> Sized f n a -> m ()

oforM_ :: Applicative m => Sized f n a -> (Element (Sized f n a) -> m ()) -> m ()

ofoldlM :: Monad m => (a0 -> Element (Sized f n a) -> m a0) -> a0 -> Sized f n a -> m a0

ofoldMap1Ex :: Semigroup m => (Element (Sized f n a) -> m) -> Sized f n a -> m

ofoldr1Ex :: (Element (Sized f n a) -> Element (Sized f n a) -> Element (Sized f n a)) -> Sized f n a -> Element (Sized f n a)

ofoldl1Ex' :: (Element (Sized f n a) -> Element (Sized f n a) -> Element (Sized f n a)) -> Sized f n a -> Element (Sized f n a)

headEx :: Sized f n a -> Element (Sized f n a)

lastEx :: Sized f n a -> Element (Sized f n a)

unsafeHead :: Sized f n a -> Element (Sized f n a)

unsafeLast :: Sized f n a -> Element (Sized f n a)

maximumByEx :: (Element (Sized f n a) -> Element (Sized f n a) -> Ordering) -> Sized f n a -> Element (Sized f n a)

minimumByEx :: (Element (Sized f n a) -> Element (Sized f n a) -> Ordering) -> Sized f n a -> Element (Sized f n a)

oelem :: Element (Sized f n a) -> Sized f n a -> Bool

onotElem :: Element (Sized f n a) -> Sized f n a -> Bool

Unbox a => MonoTraversable (Sized Vector n a)

Since 0.6.0.0

Defined in Data.Sized.Internal

Methods

otraverse :: Applicative f => (Element (Sized Vector n a) -> f (Element (Sized Vector n a))) -> Sized Vector n a -> f (Sized Vector n a)

omapM :: Applicative m => (Element (Sized Vector n a) -> m (Element (Sized Vector n a))) -> Sized Vector n a -> m (Sized Vector n a)

Storable a => MonoTraversable (Sized Vector n a)

Since 0.6.0.0

Defined in Data.Sized.Internal

Methods

otraverse :: Applicative f => (Element (Sized Vector n a) -> f (Element (Sized Vector n a))) -> Sized Vector n a -> f (Sized Vector n a)

omapM :: Applicative m => (Element (Sized Vector n a) -> m (Element (Sized Vector n a))) -> Sized Vector n a -> m (Sized Vector n a)

MonoTraversable (f a) => MonoTraversable (Sized f n a)

Since 0.2.0.0

Defined in Data.Sized.Internal

Methods

otraverse :: Applicative f0 => (Element (Sized f n a) -> f0 (Element (Sized f n a))) -> Sized f n a -> f0 (Sized f n a)

omapM :: Applicative m => (Element (Sized f n a) -> m (Element (Sized f n a))) -> Sized f n a -> m (Sized f n a)

type Dom (Sized f n) a

Defined in Data.Sized.Internal

type Dom (Sized f n) a = Dom f a

type Index (Sized f n a)

Since 0.2.0.0

Defined in Data.Sized.Internal

type Index (Sized f n a) = Ordinal n

type IxValue (Sized f n a)

Since 0.3.0.0

Defined in Data.Sized.Internal

type IxValue (Sized f n a) = IxValue (f a)

type Element (Sized f n a)

Defined in Data.Sized.Internal

type Element (Sized f n a) = Element (f a)

data SomeSized' f nat a where

Sized vector with the length is existentially quantified. This type is used mostly when the return type's length cannot be statically determined beforehand.

SomeSized' sn xs :: SomeSized' f a stands for the Sized sequence xs of element type a and length sn.

Since 0.7.0.0

Constructors

SomeSized' :: Sing n -> Sized f (n :: nat) a -> SomeSized' f nat a

Instances

Eq (f a) => Eq (SomeSized' f nat a)

Defined in Data.Sized

Methods

(==) :: SomeSized' f nat a -> SomeSized' f nat a -> Bool

(/=) :: SomeSized' f nat a -> SomeSized' f nat a -> Bool

Show (f a) => Show (SomeSized' f nat a)

Defined in Data.Sized

Methods

showsPrec :: Int -> SomeSized' f nat a -> ShowS

show :: SomeSized' f nat a -> String

showList :: [SomeSized' f nat a] -> ShowS

class Dom f a => DomC f a

Instances

Dom f a => DomC f a

Defined in Data.Sized

Accessors

Length information

length :: forall nat f (n :: nat) a. (IsPeano nat, Dom f a, SingI n) => Sized f n a -> Int

Returns the length of wrapped containers. If you use unsafeFromList or similar unsafe functions, this function may return different value from type-parameterized length.

Since 0.8.0.0 (type changed)

sLength :: forall nat f (n :: nat) a. (HasOrdinal nat, Dom f a, SingI n) => Sized f n a -> Sing n

Sing version of length.

Since 0.8.0.0 (type changed)

null :: forall nat f (n :: nat) a. (CFoldable f, Dom f a) => Sized f n a -> Bool

Test if the sequence is empty or not.

Since 0.7.0.0

Indexing

(!!) :: forall nat f (m :: nat) a. (CFoldable f, Dom f a, (One nat <= m) ~ 'True) => Sized f m a -> Int -> a

(Unsafe) indexing with Ints. If you want to check boundary statically, use %!! or sIndex.

Since 0.7.0.0

(%!!) :: forall nat f (n :: nat) c. (HasOrdinal nat, CFoldable f, Dom f c) => Sized f n c -> Ordinal n -> c

Safe indexing with Ordinals.

Since 0.7.0.0

index :: forall nat f (m :: nat) a. (CFoldable f, Dom f a, (One nat <= m) ~ 'True) => Int -> Sized f m a -> a

Flipped version of !!.

Since 0.7.0.0

sIndex :: forall nat f (n :: nat) c. (HasOrdinal nat, CFoldable f, Dom f c) => Ordinal n -> Sized f n c -> c

Flipped version of %!!.

Since 0.7.0.0

head :: forall nat f (n :: nat) a. (HasOrdinal nat, CFoldable f, Dom f a, (Zero nat < n) ~ 'True) => Sized f n a -> a

Take the first element of non-empty sequence. If you want to make case-analysis for general sequence, see Views and Patterns section.

Since 0.7.0.0

last :: forall nat f (n :: nat) a. (HasOrdinal nat, (Zero nat < n) ~ 'True, CFoldable f, Dom f a) => Sized f n a -> a

Take the last element of non-empty sequence. If you want to make case-analysis for general sequence, see Views and Patterns section.

Since 0.7.0.0

uncons :: forall nat f (n :: nat) a. (PeanoOrder nat, SingI n, CFreeMonoid f, Dom f a, (Zero nat < n) ~ 'True) => Sized f n a -> Uncons f n a

Take the head and tail of non-empty sequence. If you want to make case-analysis for general sequence, see Views and Patterns section.

Since 0.7.0.0

uncons' :: forall nat f (n :: nat) a proxy. (HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a) => proxy n -> Sized f (Succ n) a -> Uncons f (Succ n) a

uncons with explicit specified length n

Since 0.7.0.0

data Uncons f (n :: nat) a where

Constructors

Uncons :: forall nat f (n :: nat) a. SingI n => a -> Sized f n a -> Uncons f (One nat + n) a

unsnoc :: forall nat f (n :: nat) a. (HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a, (Zero nat < n) ~ 'True) => Sized f n a -> Unsnoc f n a

Take the init and last of non-empty sequence. If you want to make case-analysis for general sequence, see Views and Patterns section.

Since 0.7.0.0

unsnoc' :: forall nat f (n :: nat) a proxy. (HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a) => proxy n -> Sized f (Succ n) a -> Unsnoc f (Succ n) a

unsnoc' with explicit specified length n

Since 0.7.0.0

data Unsnoc f n a where

Constructors

Unsnoc :: forall nat f n a. Sized f (n :: nat) a -> a -> Unsnoc f (Succ n) a

Slicing

tail :: forall nat f (n :: nat) a. (HasOrdinal nat, CFreeMonoid f, Dom f a) => Sized f (One nat + n) a -> Sized f n a

Take the tail of non-empty sequence. If you want to make case-analysis for general sequence, see Views and Patterns section.

Since 0.7.0.0

init :: forall nat f (n :: nat) a. (HasOrdinal nat, CFreeMonoid f, Dom f a) => Sized f (n + One nat) a -> Sized f n a

Take the initial segment of non-empty sequence. If you want to make case-analysis for general sequence, see Views and Patterns section.

Since 0.7.0.0

take :: forall nat (n :: nat) f (m :: nat) a. (CFreeMonoid f, Dom f a, (n <= m) ~ 'True, HasOrdinal nat) => Sing n -> Sized f m a -> Sized f n a

take k xs takes first k element of xs where the length of xs should be larger than k.

Since 0.7.0.0

takeAtMost :: forall nat (n :: nat) f m a. (CFreeMonoid f, Dom f a, HasOrdinal nat) => Sing n -> Sized f m a -> Sized f (Min n m) a

takeAtMost k xs takes first at most k elements of xs.

Since 0.7.0.0

drop :: forall nat (n :: nat) f (m :: nat) a. (HasOrdinal nat, CFreeMonoid f, Dom f a, (n <= m) ~ 'True) => Sing n -> Sized f m a -> Sized f (m - n) a

drop k xs drops first k element of xs and returns the rest of sequence, where the length of xs should be larger than k.

Since 0.7.0.0

splitAt :: forall nat (n :: nat) f m a. (CFreeMonoid f, Dom f a, (n <= m) ~ 'True, HasOrdinal nat) => Sing n -> Sized f m a -> (Sized f n a, Sized f (m -. n) a)

splitAt k xs split xs at k, where the length of xs should be less than or equal to k.

Since 0.7.0.0

splitAtMost :: forall nat (n :: nat) f (m :: nat) a. (HasOrdinal nat, CFreeMonoid f, Dom f a) => Sing n -> Sized f m a -> (Sized f (Min n m) a, Sized f (m -. n) a)

splitAtMost k xs split xs at k. If k exceeds the length of xs, then the second result value become empty.

Since 0.7.0.0

Construction

Initialisation

empty :: forall nat f a. (Monoid (f a), HasOrdinal nat, Dom f a) => Sized f (Zero nat) a

Empty sequence.

Since 0.7.0.0 (type changed)

singleton :: forall nat f a. (CPointed f, Dom f a) => a -> Sized f (One nat) a

Sequence with one element.

Since 0.7.0.0

toSomeSized :: forall nat f a. (HasOrdinal nat, Dom f a, CFoldable f) => f a -> SomeSized' f nat a

Consruct the Sized sequence from base type, but the length parameter is dynamically determined and existentially quantified; see also SomeSized'.

Since 0.7.0.0

replicate :: forall nat f (n :: nat) a. (HasOrdinal nat, CFreeMonoid f, Dom f a) => Sing n -> a -> Sized f n a

Replicates the same value.

Since 0.7.0.0

replicate' :: forall nat f (n :: nat) a. (HasOrdinal nat, SingI (n :: nat), CFreeMonoid f, Dom f a) => a -> Sized f n a

replicate with the length inferred.

Since 0.7.0.0

generate :: forall (nat :: Type) f (n :: nat) (a :: Type). (CFreeMonoid f, Dom f a, HasOrdinal nat) => Sing n -> (Ordinal n -> a) -> Sized f n a

Construct a sequence of the given length by applying the function to each index.

Since 0.7.0.0

generate' :: forall (nat :: Type) f (n :: nat) (a :: Type). (SingI n, CFreeMonoid f, Dom f a, HasOrdinal nat) => (Ordinal n -> a) -> Sized f n a

generate with length inferred.

Since 0.8.0.0

Concatenation

cons :: forall nat f (n :: nat) a. (CFreeMonoid f, Dom f a) => a -> Sized f n a -> Sized f (One nat + n) a

Append an element to the head of sequence.

Since 0.8.0.0

(<|) :: forall nat f (n :: nat) a. (CFreeMonoid f, Dom f a) => a -> Sized f n a -> Sized f (One nat + n) a infixr 5

Infix version of cons.

Since 0.8.0.0

snoc :: forall nat f (n :: nat) a. (CFreeMonoid f, Dom f a) => Sized f n a -> a -> Sized f (n + One nat) a

Append an element to the tail of sequence.

Since 0.7.0.0

(|>) :: forall nat f (n :: nat) a. (CFreeMonoid f, Dom f a) => Sized f n a -> a -> Sized f (n + One nat) a infixl 5

Infix version of snoc.

Since 0.7.0.0

append :: forall nat f (n :: nat) (m :: nat) a. (CFreeMonoid f, Dom f a) => Sized f n a -> Sized f m a -> Sized f (n + m) a

Append two lists.

Since 0.7.0.0

(++) :: forall nat f (n :: nat) (m :: nat) a. (CFreeMonoid f, Dom f a) => Sized f n a -> Sized f m a -> Sized f (n + m) a infixr 5

Infix version of append.

Since 0.7.0.0

concat :: forall nat f' (m :: nat) f (n :: nat) a. (CFreeMonoid f, CFunctor f', CFoldable f', Dom f a, Dom f' (f a), Dom f' (Sized f n a)) => Sized f' m (Sized f n a) -> Sized f (m * n) a

Concatenates multiple sequences into one.

Since 0.7.0.0

Zips

zip :: forall nat f (n :: nat) a (m :: nat) b. (Dom f a, CZip f, Dom f b, Dom f (a, b)) => Sized f n a -> Sized f m b -> Sized f (Min n m) (a, b)

Zipping two sequences. Length is adjusted to shorter one.

Since 0.7.0.0

zipSame :: forall nat f (n :: nat) a b. (Dom f a, CZip f, Dom f b, Dom f (a, b)) => Sized f n a -> Sized f n b -> Sized f n (a, b)

zip for the sequences of the same length.

Since 0.7.0.0

zipWith :: forall nat f (n :: nat) a (m :: nat) b c. (Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c) => (a -> b -> c) -> Sized f n a -> Sized f m b -> Sized f (Min n m) c

Zipping two sequences with funtion. Length is adjusted to shorter one.

Since 0.7.0.0

zipWithSame :: forall nat f (n :: nat) a b c. (Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c) => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c

zipWith for the sequences of the same length.

Since 0.7.0.0

unzip :: forall nat f (n :: nat) a b. (CUnzip f, Dom f a, Dom f b, Dom f (a, b)) => Sized f n (a, b) -> (Sized f n a, Sized f n b)

Unzipping the sequence of tuples.

Since 0.7.0.0

unzipWith :: forall nat f (n :: nat) a b c. (CUnzip f, Dom f a, Dom f b, Dom f c) => (a -> (b, c)) -> Sized f n a -> (Sized f n b, Sized f n c)

Unzipping the sequence of tuples.

Since 0.7.0.0

Transformation

map :: forall nat f (n :: nat) a b. (CFreeMonoid f, Dom f a, Dom f b) => (a -> b) -> Sized f n a -> Sized f n b

Map function.

Since 0.7.0.0

reverse :: forall nat f (n :: nat) a. (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f n a

Reverse function.

Since 0.7.0.0

intersperse :: forall nat f (n :: nat) a. (CFreeMonoid f, Dom f a) => a -> Sized f n a -> Sized f ((FromInteger 2 * n) -. One nat) a

Intersperces.

Since 0.7.0.0

nub :: forall nat f (n :: nat) a. (HasOrdinal nat, Dom f a, Eq a, CFreeMonoid f) => Sized f n a -> SomeSized' f nat a

Remove all duplicates.

Since 0.7.0.0

sort :: forall nat f (n :: nat) a. (CFreeMonoid f, Dom f a, Ord a) => Sized f n a -> Sized f n a

Sorting sequence by ascending order.

Since 0.7.0.0

sortBy :: forall nat f (n :: nat) a. (CFreeMonoid f, Dom f a) => (a -> a -> Ordering) -> Sized f n a -> Sized f n a

Generalized version of sort.

Since 0.7.0.0

insert :: forall nat f (n :: nat) a. (CFreeMonoid f, Dom f a, Ord a) => a -> Sized f n a -> Sized f (Succ n) a

Insert new element into the presorted sequence.

Since 0.7.0.0

insertBy :: forall nat f (n :: nat) a. (CFreeMonoid f, Dom f a) => (a -> a -> Ordering) -> a -> Sized f n a -> Sized f (Succ n) a

Generalized version of insert.

Since 0.7.0.0

Conversion

List

toList :: forall nat f (n :: nat) a. (CFoldable f, Dom f a) => Sized f n a -> [a]

Convert to list.

Since 0.7.0.0

fromList :: forall nat f (n :: nat) a. (HasOrdinal nat, CFreeMonoid f, Dom f a) => Sing n -> [a] -> Maybe (Sized f n a)

If the given list is shorter than n, then returns Nothing Otherwise returns Sized f n a consisting of initial n element of given list.

Since 0.7.0.0 (type changed)

fromList' :: forall nat f (n :: nat) a. (PeanoOrder nat, Dom f a, CFreeMonoid f, SingI n) => [a] -> Maybe (Sized f n a)

fromList with the result length inferred.

Since 0.7.0.0

unsafeFromList :: forall (nat :: Type) f (n :: nat) a. (CFreeMonoid f, Dom f a) => Sing n -> [a] -> Sized f n a

Unsafe version of fromList. If the length of the given list does not equal to n, then something unusual happens.

Since 0.7.0.0

unsafeFromList' :: forall nat f (n :: nat) a. (SingI n, CFreeMonoid f, Dom f a) => [a] -> Sized f n a

unsafeFromList with the result length inferred.

Since 0.7.0.0

fromListWithDefault :: forall nat f (n :: nat) a. (HasOrdinal nat, Dom f a, CFreeMonoid f) => Sing n -> a -> [a] -> Sized f n a

Construct a Sized f n a by padding default value if the given list is short.

Since 0.5.0.0 (type changed)

fromListWithDefault' :: forall nat f (n :: nat) a. (PeanoOrder nat, SingI n, CFreeMonoid f, Dom f a) => a -> [a] -> Sized f n a

fromListWithDefault with the result length inferred.

Since 0.7.0.0

Base container

unsized :: forall nat f (n :: nat) a. Sized f n a -> f a

Forget the length and obtain the wrapped base container.

Since 0.7.0.0

toSized :: forall nat f (n :: nat) a. (HasOrdinal nat, CFreeMonoid f, Dom f a) => Sing (n :: nat) -> f a -> Maybe (Sized f n a)

If the length of the input is shorter than n, then returns Nothing. Otherwise returns Sized f n a consisting of initial n element of the input.

Since 0.7.0.0

toSized' :: forall nat f (n :: nat) a. (PeanoOrder nat, Dom f a, CFreeMonoid f, SingI n) => f a -> Maybe (Sized f n a)

toSized with the result length inferred.

Since 0.7.0.0

unsafeToSized :: forall nat f (n :: nat) a. Sing n -> f a -> Sized f n a

Unsafe version of toSized. If the length of the given list does not equal to n, then something unusual happens.

Since 0.7.0.0

unsafeToSized' :: forall nat f (n :: nat) a. (SingI n, Dom f a) => f a -> Sized f n a

unsafeToSized with the result length inferred.

Since 0.7.0.0

toSizedWithDefault :: forall nat f (n :: nat) a. (HasOrdinal nat, CFreeMonoid f, Dom f a) => Sing (n :: nat) -> a -> f a -> Sized f n a

Construct a Sized f n a by padding default value if the given list is short.

Since 0.7.0.0

toSizedWithDefault' :: forall nat f (n :: nat) a. (PeanoOrder nat, SingI n, CFreeMonoid f, Dom f a) => a -> f a -> Sized f n a

toSizedWithDefault with the result length inferred.

Since 0.7.0.0

Querying

Partitioning

data Partitioned f n a where

The type Partitioned f n a represents partitioned sequence of length n. Value Partitioned lenL ls lenR rs stands for:

• Entire sequence is divided into ls and rs, and their length are lenL and lenR resp.

• lenL + lenR = n

Since 0.7.0.0

Constructors

Partitioned :: Dom f a => Sing n -> Sized f n a -> Sing m -> Sized f m a -> Partitioned f (n + m) a

takeWhile :: forall nat f (n :: nat) a. (HasOrdinal nat, Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> SomeSized' f nat a

Take the initial segment as long as elements satisfys the predicate.

Since 0.7.0.0

dropWhile :: forall nat f (n :: nat) a. (HasOrdinal nat, CFreeMonoid f, Dom f a) => (a -> Bool) -> Sized f n a -> SomeSized' f nat a

Drop the initial segment as long as elements satisfys the predicate.

Since 0.7.0.0

span :: forall nat f (n :: nat) a. (HasOrdinal nat, CFreeMonoid f, Dom f a) => (a -> Bool) -> Sized f n a -> Partitioned f n a

Split the sequence into the longest prefix of elements that satisfy the predicate and the rest.

Since 0.7.0.0

break :: forall nat f (n :: nat) a. (HasOrdinal nat, CFreeMonoid f, Dom f a) => (a -> Bool) -> Sized f n a -> Partitioned f n a

Split the sequence into the longest prefix of elements that do not satisfy the predicate and the rest.

Since 0.7.0.0

partition :: forall nat f (n :: nat) a. (HasOrdinal nat, CFreeMonoid f, Dom f a) => (a -> Bool) -> Sized f n a -> Partitioned f n a

Split the sequence in two parts, the first one containing those elements that satisfy the predicate and the second one those that don't.

Since 0.7.0.0

Searching

elem :: forall nat f (n :: nat) a. (CFoldable f, Dom f a, Eq a) => a -> Sized f n a -> Bool

Membership test; see also notElem.

Since 0.7.0.0

notElem :: forall nat f (n :: nat) a. (CFoldable f, Dom f a, Eq a) => a -> Sized f n a -> Bool

Negation of elem.

Since 0.7.0.0

find :: forall nat f (n :: nat) a. (CFoldable f, Dom f a) => (a -> Bool) -> Sized f n a -> Maybe a

Find the element satisfying the predicate.

Since 0.7.0.0

findIndex :: forall nat f (n :: nat) a. (CFoldable f, Dom f a) => (a -> Bool) -> Sized f n a -> Maybe Int

findIndex p xs find the element satisfying p and returns its index if exists.

Since 0.7.0.0

sFindIndex :: forall nat f (n :: nat) a. (SingI (n :: nat), CFoldable f, Dom f a, HasOrdinal nat) => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n)

Ordinal version of findIndex.

Since 0.7.0.0

findIndices :: forall nat f (n :: nat) a. (CFoldable f, Dom f a) => (a -> Bool) -> Sized f n a -> [Int]

findIndices p xs find all elements satisfying p and returns their indices.

Since 0.7.0.0

sFindIndices :: forall nat f (n :: nat) a. (HasOrdinal nat, CFoldable f, Dom f a, SingI (n :: nat)) => (a -> Bool) -> Sized f n a -> [Ordinal n]

Ordinal version of findIndices.

Since 0.7.0.0

elemIndex :: forall nat f (n :: nat) a. (CFoldable f, Eq a, Dom f a) => a -> Sized f n a -> Maybe Int

Returns the index of the given element in the list, if exists.

Since 0.7.0.0

sElemIndex :: forall nat f (n :: nat) a. (SingI n, CFoldable f, Dom f a, Eq a, HasOrdinal nat) => a -> Sized f n a -> Maybe (Ordinal n)

Ordinal version of elemIndex. Since 0.7.0.0, we no longer do boundary check inside the definition.

Since 0.7.0.0

sUnsafeElemIndex :: forall nat f (n :: nat) a. (SingI n, CFoldable f, Dom f a, Eq a, HasOrdinal nat) => a -> Sized f n a -> Maybe (Ordinal n)

Deprecated: No difference with sElemIndex; use sElemIndex instead.

Since 0.5.0.0 (type changed)

Ordinal version of elemIndex. Since 0.7.0.0, we no longer do boundary check inside the definition.

Since 0.7.0.0

elemIndices :: forall nat f (n :: nat) a. (CFoldable f, Dom f a, Eq a) => a -> Sized f n a -> [Int]

Returns all indices of the given element in the list.

Since 0.7.0.0

sElemIndices :: forall nat f (n :: nat) a. (CFoldable f, HasOrdinal nat, SingI (n :: nat), Dom f a, Eq a) => a -> Sized f n a -> [Ordinal n]

Ordinal version of elemIndices

Since 0.7.0.0

Views and Patterns

With GHC's ViewPatterns and PatternSynonym extensions, we can pattern-match on arbitrary Sized f n a if f is list-like functor. Curretnly, there are two direction view and patterns: Cons and Snoc. Assuming underlying sequence type f has O(1) implementation for cnull, chead (resp. clast) and ctail (resp. cinit), We can view and pattern-match on cons (resp. snoc) of Sized f n a in O(1).

Views

With ViewPatterns extension, we can pattern-match on Sized value as follows:

slen :: (SingI n, 'Dom f a' f) => Sized f n a -> Sing n
slen (viewCons -> NilCV)    = SZ
slen (viewCons -> _ :- as) = SS (slen as)
slen _                          = error "impossible"

The constraint (SingI n, 'Dom f a' f) is needed for view function. In the above, we have extra wildcard pattern (_) at the last. Code compiles if we removed it, but current GHC warns for incomplete pattern, although we know first two patterns exhausts all the case.

Equivalently, we can use snoc-style pattern-matching:

slen :: (SingI n, 'Dom f a' f) => Sized f n a -> Sing n
slen (viewSnoc -> NilSV)     = SZ
slen (viewSnoc -> as -:: _) = SS (slen as)

Patterns

So we can pattern match on both end of sequence via views, but it is rather clumsy to nest it. For example:

nextToHead :: ('Dom f a' f, SingI n) => Sized f (S (S n)) a -> a
nextToHead (viewCons -> _ :- (viewCons -> a :- _)) = a

In such a case, with PatternSynonyms extension we can write as follows:

nextToHead :: ('Dom f a' f, SingI n) => Sized f (S (S n)) a -> a
nextToHead (_ :< a :< _) = a

Of course, we can also rewrite above slen example using PatternSynonyms:

slen :: (SingI n, 'Dom f a' f) => Sized f n a -> Sing n
slen Nil      = SZ
slen (_ :< as) = SS (slen as)

So, we can use :< and Nil (resp. :> and Nil) to pattern-match directly on cons-side (resp. snoc-side) as we usually do for lists. Nil, :<, and :> are neither functions nor data constructors, but pattern synonyms so we cannot use them in expression contexts. For more detail on pattern synonyms, see GHC Users Guide and HaskellWiki.

Definitions

viewCons :: forall nat f (n :: nat) a. (HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a) => Sized f n a -> ConsView f n a

Case analysis for the cons-side of sequence.

Since 0.5.0.0 (type changed)

data ConsView f n a where

View of the left end of sequence (cons-side).

Since 0.7.0.0

Constructors

NilCV :: ConsView f (Zero nat) a

(:-) :: (SingI n, SingI (One nat + n)) => a -> Sized f n a -> ConsView f (One nat + n) a infixr 5

viewSnoc :: forall nat f (n :: nat) a. (HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a) => Sized f n a -> SnocView f n a

Case analysis for the snoc-side of sequence.

Since 0.5.0.0 (type changed)

data SnocView f n a where

View of the left end of sequence (snoc-side).

Since 0.7.0.0

Constructors

NilSV :: SnocView f (Zero nat) a

(:-::) :: SingI (n :: nat) => Sized f n a -> a -> SnocView f (n + One nat) a infixl 5

pattern Nil :: forall nat f (n :: nat) a. (SingI n, CFreeMonoid f, Dom f a, HasOrdinal nat) => n ~ Zero nat => Sized f n a

Pattern synonym for a nil sequence.

pattern (:<) :: forall nat (f :: Type -> Type) a (n :: nat). (Dom f a, PeanoOrder nat, SingI n, CFreeMonoid f) => forall (n1 :: nat). (n ~ (One nat + n1), SingI n1) => a -> Sized f n1 a -> Sized f n a infixr 5

Pattern synonym for cons-side uncons.

pattern (:>) :: forall nat (f :: Type -> Type) a (n :: nat). (Dom f a, PeanoOrder nat, SingI n, CFreeMonoid f) => forall (n1 :: nat). (n ~ (n1 + One nat), SingI n1) => Sized f n1 a -> a -> Sized f n a infixl 5

Pattern synonym for snoc-side unsnoc.

Orphan instances

(Functor f, CFreeMonoid f, CZip f, HasOrdinal nat, SingI n, forall a. DomC f a) => Applicative (Sized f n)

Applicative instance, generalizing ZipList.

Methods

pure :: a -> Sized f n a

(<*>) :: Sized f n (a -> b) -> Sized f n a -> Sized f n b

liftA2 :: (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c

(*>) :: Sized f n a -> Sized f n b -> Sized f n b

(<*) :: Sized f n a -> Sized f n b -> Sized f n a

CTraversable f => CTraversable (Sized f n)

Methods

ctraverse :: (Dom (Sized f n) a, Dom (Sized f n) b, Applicative g) => (a -> g b) -> Sized f n a -> g (Sized f n b)

(CZip f, CFreeMonoid f) => CZip (Sized f n)

Methods

czipWith :: (Dom (Sized f n) a, Dom (Sized f n) b, Dom (Sized f n) c) => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c

czip :: (Dom (Sized f n) a, Dom (Sized f n) b, Dom (Sized f n) (a, b)) => Sized f n a -> Sized f n b -> Sized f n (a, b)

(PeanoOrder nat, SingI n, CZip f, CFreeMonoid f) => CRepeat (Sized f n)

Methods

crepeat :: Dom (Sized f n) a => a -> Sized f n a

(CFreeMonoid f, CZip f) => CApplicative (Sized f n)

Methods

pair :: (Dom (Sized f n) a, Dom (Sized f n) b, Dom (Sized f n) (a, b)) => Sized f n a -> Sized f n b -> Sized f n (a, b)

(<.>) :: (Dom (Sized f n) a, Dom (Sized f n) b, Dom (Sized f n) (a -> b)) => Sized f n (a -> b) -> Sized f n a -> Sized f n b

(.>) :: (Dom (Sized f n) a, Dom (Sized f n) b) => Sized f n a -> Sized f n b -> Sized f n b

(<.) :: (Dom (Sized f n) a, Dom (Sized f n) b) => Sized f n a -> Sized f n b -> Sized f n a

(CFreeMonoid f, PeanoOrder nat, SingI n) => CPointed (Sized f n)

Methods

cpure :: Dom (Sized f n) a => a -> Sized f n a

(CZip f, CFreeMonoid f) => CSemialign (Sized f n)

N.B. Since calign is just zipping for fixed n, we require more strong CZip constraint here.

Methods

calignWith :: (Dom (Sized f n) a, Dom (Sized f n) b, Dom (Sized f n) c) => (These a b -> c) -> Sized f n a -> Sized f n b -> Sized f n c

calign :: (Dom (Sized f n) a, Dom (Sized f n) b, Dom (Sized f n) (These a b)) => Sized f n a -> Sized f n b -> Sized f n (These a b)