Data.Sized

This module provides the functionality to make length-parametrized types from existing ListLike and Functor 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 n a

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

Here, f must be the instance of Functor and ListLike (f a) a for all a. This constraint is expressed by ListLikeF. Folding and traversing function such as all and foldl' is available via Foldable or Traversable class, if f is the instance of them.

Since 0.2.0.0

Instances

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

Since 0.2.0.0

Methods

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

imapped :: (Indexable (Ordinal nat1 n) p, Settable f) => p a (f b) -> Sized nat1 f n a -> f (Sized nat1 f n b)

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

Since 0.2.0.0

Methods

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

ifolded :: (Indexable (Ordinal nat1 n) p, Contravariant f, Applicative f) => p a (f a) -> Sized nat1 f n a -> f (Sized nat1 f n a)

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

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

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

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

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

Since 0.2.0.0

Methods

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

itraversed :: (Indexable (Ordinal nat1 n) p, Applicative f) => p a (f b) -> Sized nat1 f n a -> f (Sized nat1 f n b)

Functor f => Functor (Sized nat f n)

Methods

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

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

Foldable f => Foldable (Sized nat f n)

Methods

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

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

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

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

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

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

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

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

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

null :: Sized nat f n a -> Bool

length :: Sized nat f n a -> Int

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

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

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

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

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

Traversable f => Traversable (Sized nat f n)

Methods

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

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

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

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

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

Methods

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

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

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

Methods

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

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

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

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

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

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

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

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

Methods

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

show :: Sized nat f n a -> String

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

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

Methods

rnf :: Sized nat f n a -> ()

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

Methods

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

hash :: Sized nat f n a -> Int

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

Methods

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

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

Methods

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

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

Methods

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

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

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

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

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

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

onull :: Sized nat f n a -> Bool

olength :: Sized nat f n a -> Int

olength64 :: Sized nat f n a -> Int64

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Unbox a => MonoTraversable (Sized nat Vector n a)

Since 0.2.0.0

Methods

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

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

Storable a => MonoTraversable (Sized nat Vector n a)

Since 0.2.0.0

Methods

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

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

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

Since 0.2.0.0

Methods

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

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

type Index (Sized nat f n a)

type Index (Sized nat f n a) = Ordinal nat n

type IxValue (Sized nat f n a)

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

type Element (Sized nat f n a)

type Element (Sized nat 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.1.0.0

Constructors

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

Instances

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

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)

Methods

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

show :: SomeSized f nat a -> String

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

instLL :: forall f a. ListLikeF f :- ListLike (f a) a

instFunctor :: ListLikeF f :- Functor f

type ListLikeF f = (Functor f, Forall (LLF f))

Functor f such that there is instance ListLike (f a) a for any a.

Since 0.1.0.0

withListLikeF :: forall pxy f a b. ListLikeF f => pxy (f a) -> ((Functor f, ListLike (f a) a) => b) -> b

withListLikeF' :: ListLikeF f => f a -> ((Functor f, ListLike (f a) a) => b) -> b

Accessors

Length information

length :: ListLike (f a) a => 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.1.0.0

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

Sing version of length.

Since 0.2.0.0

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

Test if the sequence is empty or not.

Since 0.1.0.0

Indexing

(!!) :: ListLike (f a) a => Sized f (Succ m) a -> Int -> a

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

Since 0.1.0.0

(%!!) :: (HasOrdinal nat, ListLike (f c) c) => Sized f n c -> Ordinal (n :: nat) -> c

Safe indexing with Ordinals.

Since 0.1.0.0

index :: ListLike (f a) a => Int -> Sized f (Succ m) a -> a

Flipped version of !!.

Since 0.1.0.0

sIndex :: (HasOrdinal nat, ListLike (f c) c) => Ordinal (n :: nat) -> Sized f n c -> c

Flipped version of %!!.

Since 0.1.0.0

head :: (HasOrdinal nat, ListLike (f a) b, (Zero nat :< n) ~ True) => Sized f n a -> b

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

last :: (HasOrdinal nat, (Zero nat :< n) ~ True, ListLike (f a) b) => Sized f n a -> b

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

uncons :: ListLike (f a) b => Sized f (Succ n) a -> (b, Sized 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.1.0.0

uncons' :: ListLike (f a) b => proxy n -> Sized f (Succ n) a -> (b, Sized f n a)

unsnoc :: ListLike (f a) b => Sized f (Succ n) a -> (Sized f n a, b)

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

unsnoc' :: ListLike (f a) b => proxy n -> Sized f (Succ n) a -> (Sized f n a, b)

Slicing

tail :: (HasOrdinal nat, ListLike (f a) a) => Sized f (Succ n) a -> Sized f (n :: nat) 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.1.0.0

init :: ListLike (f a) a => Sized f (Succ n) 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.1.0.0

take :: (ListLike (f a) a, (n :<= m) ~ True, HasOrdinal nat) => Sing (n :: nat) -> 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. It is really sad, that this function takes at least O(k) regardless of base container.

Since 0.1.0.0

takeAtMost :: (ListLike (f a) a, HasOrdinal nat) => Sing (n :: nat) -> Sized f m a -> Sized f (Min n m) a

take k xs takes first k element of xs at most. It is really sad, that this function takes at least O(k) regardless of base container.

Since 0.1.0.0

drop :: (HasOrdinal nat, ListLike (f a) a, (n :<= m) ~ True) => Sing (n :: nat) -> 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. It is really sad, that this function takes at least O(k) regardless of base container.

Since 0.1.0.0

splitAt :: (ListLike (f a) a, (n :<= m) ~ True, HasOrdinal nat) => Sing (n :: nat) -> 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. It is really sad, that this function takes at least O(k) regardless of base container.

Since 0.1.0.0

splitAtMost :: (HasOrdinal nat, ListLike (f a) a) => Sing (n :: nat) -> 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. It is really sad, that this function takes at least O(k) regardless of base container.

Since 0.1.0.0

Construction

Initialisation

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

Empty sequence.

Since 0.1.0.0

singleton :: forall f a. ListLike (f a) a => a -> Sized f 1 a

Sequence with one element.

Since 0.1.0.0

toSomeSized :: forall nat f a. (HasOrdinal nat, ListLike (f a) a) => 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.1.0.0

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

Replicates the same value.

Since 0.1.0.0

replicate' :: (HasOrdinal nat, SingI (n :: nat), ListLike (f a) a) => a -> Sized f n a

replicate with the length inferred.

Since 0.1.0.0

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

Concatenation

cons :: ListLike (f a) b => b -> Sized f n a -> Sized f (Succ n) a

Append an element to the head of sequence.

Since 0.1.0.0

(<|) :: ListLike (f a) b => b -> Sized f n a -> Sized f (Succ n) a infixr 5

Infix version of cons.

Since 0.1.0.0

snoc :: ListLike (f a) b => Sized f n a -> b -> Sized f (Succ n) a

Append an element to the tail of sequence.

Since 0.1.0.0

(|>) :: ListLike (f a) b => Sized f n a -> b -> Sized f (Succ n) a infixl 5

Infix version of snoc.

Since 0.1.0.0

append :: ListLike (f a) a => Sized f n a -> Sized f m a -> Sized f (n :+ m) a

Append two lists.

Since 0.1.0.0

(++) :: ListLike (f a) a => Sized f n a -> Sized f m a -> Sized f (n :+ m) a infixr 5

Infix version of append.

Since 0.1.0.0

concat :: forall f f' m n a. (Functor f', Foldable f', ListLike (f a) a) => Sized f' m (Sized f n a) -> Sized f (m :* n) a

Concatenates multiple sequences into one.

Since 0.1.0.0

Zips

zip :: (ListLike (f a) a, ListLike (f b) b, ListLike (f (a, b)) (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.1.0.0

zipSame :: (ListLike (f a) a, ListLike (f b) b, ListLike (f (a, b)) (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.1.0.0

zipWith :: (ListLike (f a) a, ListLike (f b) b, ListLike (f c) 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.1.0.0

zipWithSame :: (ListLike (f a) a, ListLike (f b) b, ListLike (f c) 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.1.0.0

unzip :: (ListLike (f a) a, ListLike (f b) b, ListLike (f (a, b)) (a, b)) => Sized f n (a, b) -> (Sized f n a, Sized f n b)

Unzipping the sequence of tuples.

Since 0.1.0.0

Transformation

map :: (ListLike (f a) a, ListLike (f b) b) => (a -> b) -> Sized f n a -> Sized f n b

Map function.

Since 0.1.0.0

fmap :: forall f n a b. Functor f => (a -> b) -> Sized f n a -> Sized f n b

reverse :: ListLike (f a) a => Sized f n a -> Sized f n a

Reverse function.

Since 0.1.0.0

intersperse :: ListLike (f a) a => a -> Sized f n a -> Sized f ((FromInteger 2 :* n) :-. 1) a

Intersperces.

Since 0.1.0.0

nub :: (HasOrdinal nat, ListLike (f a) a, Eq a) => Sized f n a -> SomeSized f nat a

Remove all duplicates.

Since 0.1.0.0

sort :: (ListLike (f a) a, Ord a) => Sized f n a -> Sized f n a

Sorting sequence by ascending order.

Since 0.1.0.0

sortBy :: ListLike (f a) a => (a -> a -> Ordering) -> Sized f n a -> Sized f n a

Generalized version of sort.

Since 0.1.0.0

insert :: (ListLike (f a) a, Ord a) => a -> Sized f n a -> Sized f (Succ n) a

Insert new element into the presorted sequence.

Since 0.1.0.0

insertBy :: ListLike (f a) a => (a -> a -> Ordering) -> a -> Sized f n a -> Sized f (Succ n) a

Generalized version of insert.

Since 0.1.0.0

Conversion

List

toList :: ListLike (f a) a => Sized f n a -> [a]

Convert to list.

Since 0.1.0.0

fromList :: forall f n a. (HasOrdinal nat, ListLike (f a) a) => Sing (n :: nat) -> [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.1.0.0

fromList' :: (ListLike (f a) a, SingI (n :: Nat)) => [a] -> Maybe (Sized f n a)

fromList with the result length inferred.

Since 0.1.0.0

unsafeFromList :: forall nat f n a. ListLike (f a) 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.1.0.0

unsafeFromList' :: (SingI (n :: Nat), ListLike (f a) a) => [a] -> Sized f n a

unsafeFromList with the result length inferred.

Since 0.1.0.0

fromListWithDefault :: forall f n a. (HasOrdinal nat, ListLike (f a) a) => 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.1.0.0

fromListWithDefault' :: (SingI (n :: Nat), ListLike (f a) a) => a -> [a] -> Sized f n a

fromListWithDefault with the result length inferred.

Since 0.1.0.0

Base container

unsized :: Sized f n a -> f a

Forget the length and obtain the wrapped base container.

Since 0.1.0.0

toSized :: (HasOrdinal nat, ListLike (f a) 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.1.0.0

toSized' :: (ListLike (f a) a, SingI (n :: Nat)) => f a -> Maybe (Sized f n a)

toSized with the result length inferred.

Since 0.1.0.0

unsafeToSized :: 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.1.0.0

unsafeToSized' :: (SingI (n :: Nat), ListLike (f a) a) => f a -> Sized f n a

unsafeToSized with the result length inferred.

Since 0.1.0.0

toSizedWithDefault :: (HasOrdinal nat, ListLike (f a) 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.1.0.0

toSizedWithDefault' :: (SingI (n :: Nat), ListLike (f a) a) => a -> f a -> Sized f n a

toSizedWithDefault with the result length inferred.

Since 0.1.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.1.0.0

Constructors

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

takeWhile :: (HasOrdinal nat, ListLike (f a) a) => (a -> Bool) -> Sized f n a -> SomeSized f nat a

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

Since 0.1.0.0

dropWhile :: (HasOrdinal nat, ListLike (f a) a) => (a -> Bool) -> Sized f n a -> SomeSized f nat a

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

Since 0.1.0.0

span :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> Partitioned f n a

Invariant: ListLike (f a) a instance must be implemented to satisfy the following property: length (fst (span p xs)) + length (snd (span p xs)) == length xs Otherwise, this function introduces severe contradiction.

Since 0.1.0.0

break :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> Partitioned f n a

Invariant: ListLike (f a) a instance must be implemented to satisfy the following property: length (fst (break p xs)) + length (snd (break p xs)) == length xs Otherwise, this function introduces severe contradiction.

Since 0.1.0.0

partition :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> Partitioned f n a

Invariant: ListLike (f a) a instance must be implemented to satisfy the following property: length (fst (partition p xs)) + length (snd (partition p xs)) == length xs Otherwise, this function introduces severe contradiction.

Since 0.1.0.0

Searching

elem :: (ListLike (f a) a, Eq a) => a -> Sized f n a -> Bool

Membership test; see also notElem.

Since 0.1.0.0

notElem :: (ListLike (f a) a, Eq a) => a -> Sized f n a -> Bool

Negation of elem.

Since 0.1.0.0

find :: Foldable f => (a -> Bool) -> Sized f n a -> Maybe a

Find the element satisfying the predicate.

Since 0.1.0.0

findF :: Foldable f => (a -> Bool) -> Sized f n a -> Maybe a

Foldable version of find.

findIndex :: ListLike (f a) 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.1.0.0

findIndexIF :: FoldableWithIndex i f => (a -> Bool) -> Sized f n a -> Maybe i

findIndex implemented in terms of FoldableWithIndex

sFindIndex :: (SingI (n :: nat), ListLike (f a) a, HasOrdinal nat) => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n)

Ordinal version of findIndex.

Since 0.1.0.0

sFindIndexIF :: (FoldableWithIndex i f, Integral i, HasOrdinal nat, SingI n) => (a -> Bool) -> Sized f (n :: nat) a -> Maybe (Ordinal n)

sFindIndex implemented in terms of FoldableWithIndex

findIndices :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> [Int]

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

Since 0.1.0.0

findIndicesIF :: FoldableWithIndex i f => (a -> Bool) -> Sized f n a -> [i]

findIndices implemented in terms of FoldableWithIndex

sFindIndices :: (HasOrdinal nat, SingI (n :: nat), ListLike (f a) a) => (a -> Bool) -> Sized f n a -> [Ordinal n]

Ordinal version of findIndices.

Since 0.1.0.0

sFindIndicesIF :: (FoldableWithIndex i f, Integral i, HasOrdinal nat, SingI n) => (a -> Bool) -> Sized f (n :: nat) a -> [Ordinal n]

elemIndex :: (Eq a, ListLike (f a) a) => a -> Sized f n a -> Maybe Int

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

Since 0.1.0.0

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

Ordinal version of elemIndex It statically checks boundary invariants. If you don't internal structure on Sized, then sUnsafeElemIndex is much faster and also safe for most cases.

Since 0.1.0.0

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

elemIndices :: (ListLike (f a) a, Eq a) => a -> Sized f n a -> [Int]

Returns all indices of the given element in the list.

Since 0.1.0.0

sElemIndices :: (HasOrdinal nat, SingI (n :: nat), ListLike (f a) a, Eq a) => a -> Sized f n a -> [Ordinal n]

Ordinal version of elemIndices

Since 0.1.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 null, head (resp. last) and tail (resp. init), 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, 'ListLike (f a) 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, 'ListLike (f a) 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, 'ListLike (f a) 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 :: ('ListLike (f a) 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 :: ('ListLike (f a) 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, 'ListLike (f a) a' f) => Sized f n a -> Sing n
slen NilL      = SZ
slen (_ :< as) = SS (slen as)
slen _           = error "impossible"

So, we can use :< and NilL (resp. :> and NilR) to pattern-match directly on cons-side (resp. snoc-side) as we usually do for lists. :<, NilL, :> and NilR 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 f a n. (HasOrdinal nat, ListLike (f a) a) => Sized f n a -> ConsView f n a

Case analysis for the cons-side of sequence.

Since 0.1.0.0

data ConsView f n a where

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

Since 0.1.0.0

Constructors

NilCV :: ConsView f (Zero nat) a

(::-) :: SingI n => a -> Sized f n a -> ConsView f (Succ n) a infixr 5

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

Case analysis for the snoc-side of sequence.

Since 0.1.0.0

data SnocView f n a where

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

Since 0.1.0.0

Constructors

NilSV :: SnocView f (Zero nat) a

(:-::) :: SingI n => Sized f n a -> a -> SnocView f (Succ n) a infixl 5

pattern (:<) :: forall nat f n a. (ListLike (f a) a, HasOrdinal nat) => forall n1. ((~) nat n (Succ nat n1), SingI nat n1) => a -> Sized nat f n1 a -> Sized nat f n a infixr 5

Pattern synonym for cons-side uncons.

pattern NilL :: forall nat f n a. (ListLike (f a) a, HasOrdinal nat) => (~) nat n (Zero nat) => Sized nat f n a

pattern (:>) :: forall nat f n a. (ListLike (f a) a, HasOrdinal nat) => forall n1. ((~) nat n (Succ nat n1), SingI nat n1) => Sized nat f n1 a -> a -> Sized nat f n a infixl 5

pattern NilR :: forall nat f n a. (ListLike (f a) a, HasOrdinal nat) => (~) nat n (Zero nat) => Sized nat f n a

Orphan instances

(Functor f, HasOrdinal nat1, SingI nat1 n, ListLikeF f) => Applicative (Sized nat1 f n)

Applicative instance, generalizing ZipList.

Methods

pure :: a -> Sized nat1 f n a

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

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

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