Safe Haskell | None |
---|---|
Language | Haskell2010 |
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.
- data Sized f n a
- data SomeSized f nat a where
- instLL :: forall f a. ListLikeF f :- ListLike (f a) a
- instFunctor :: ListLikeF f :- Functor f
- type ListLikeF f = (Functor f, Forall (LLF f))
- 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
- length :: ListLike (f a) a => Sized f n a -> Int
- sLength :: forall f n a. (HasOrdinal nat, ListLike (f a) a) => Sized f n a -> Sing n
- null :: ListLike (f a) a => Sized f n a -> Bool
- (!!) :: ListLike (f a) a => Sized f (Succ m) a -> Int -> a
- (%!!) :: (HasOrdinal nat, ListLike (f c) c) => Sized f n c -> Ordinal (n :: nat) -> c
- index :: ListLike (f a) a => Int -> Sized f (Succ m) a -> a
- sIndex :: (HasOrdinal nat, ListLike (f c) c) => Ordinal (n :: nat) -> Sized f n c -> c
- head :: (HasOrdinal nat, ListLike (f a) b, (Zero nat :< n) ~ True) => Sized f n a -> b
- last :: (HasOrdinal nat, (Zero nat :< n) ~ True, ListLike (f a) b) => Sized f n a -> b
- uncons :: ListLike (f a) b => Sized f (Succ n) a -> (b, Sized f n a)
- 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)
- unsnoc' :: ListLike (f a) b => proxy n -> Sized f (Succ n) a -> (Sized f n a, b)
- tail :: (HasOrdinal nat, ListLike (f a) a) => Sized f (Succ n) a -> Sized f (n :: nat) a
- init :: ListLike (f a) a => Sized f (Succ n) a -> Sized f n a
- take :: (ListLike (f a) a, (n :<= m) ~ True, HasOrdinal nat) => Sing (n :: nat) -> Sized f m a -> Sized f n a
- takeAtMost :: (ListLike (f a) a, HasOrdinal nat) => Sing (n :: nat) -> Sized f m a -> Sized f (Min n m) a
- drop :: (HasOrdinal nat, ListLike (f a) a, (n :<= m) ~ True) => Sing (n :: nat) -> Sized f m a -> Sized f (m :- n) a
- 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)
- 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)
- empty :: forall f a. (HasOrdinal nat, ListLike (f a) a) => Sized f (Zero nat :: nat) a
- singleton :: forall f a. ListLike (f a) a => a -> Sized f 1 a
- toSomeSized :: forall nat f a. (HasOrdinal nat, ListLike (f a) a) => f a -> SomeSized f nat a
- replicate :: forall f n a. (HasOrdinal nat, ListLike (f a) a) => Sing n -> a -> Sized f n a
- replicate' :: (HasOrdinal nat, SingI (n :: nat), ListLike (f a) a) => a -> Sized f n a
- generate :: forall nat n a f. (ListLike (f a) a, HasOrdinal nat) => Sing n -> (Ordinal n -> a) -> Sized f n a
- cons :: ListLike (f a) b => b -> Sized f n a -> Sized f (Succ n) a
- (<|) :: ListLike (f a) b => b -> Sized f n a -> Sized f (Succ n) a
- snoc :: ListLike (f a) b => Sized f n a -> b -> Sized f (Succ n) a
- (|>) :: ListLike (f a) b => Sized f n a -> b -> Sized f (Succ n) a
- append :: ListLike (f a) a => Sized f n a -> Sized f m a -> Sized f (n :+ m) a
- (++) :: ListLike (f a) a => Sized f n a -> Sized f m a -> Sized f (n :+ m) a
- 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
- 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)
- 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)
- 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
- 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
- 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)
- map :: (ListLike (f a) a, ListLike (f b) b) => (a -> b) -> Sized f n a -> Sized f n b
- 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
- intersperse :: ListLike (f a) a => a -> Sized f n a -> Sized f ((FromInteger 2 :* n) :-. 1) a
- nub :: (HasOrdinal nat, ListLike (f a) a, Eq a) => Sized f n a -> SomeSized f nat a
- sort :: (ListLike (f a) a, Ord a) => Sized f n a -> Sized f n a
- sortBy :: ListLike (f a) a => (a -> a -> Ordering) -> Sized f n a -> Sized f n a
- insert :: (ListLike (f a) a, Ord a) => a -> Sized f n a -> Sized f (Succ n) a
- insertBy :: ListLike (f a) a => (a -> a -> Ordering) -> a -> Sized f n a -> Sized f (Succ n) a
- toList :: ListLike (f a) a => Sized f n a -> [a]
- fromList :: forall f n a. (HasOrdinal nat, ListLike (f a) a) => Sing (n :: nat) -> [a] -> Maybe (Sized f n a)
- fromList' :: (ListLike (f a) a, SingI (n :: Nat)) => [a] -> Maybe (Sized f n a)
- unsafeFromList :: forall nat f n a. ListLike (f a) a => Sing n -> [a] -> Sized f n a
- unsafeFromList' :: (SingI (n :: Nat), ListLike (f a) a) => [a] -> Sized f n a
- fromListWithDefault :: forall f n a. (HasOrdinal nat, ListLike (f a) a) => Sing n -> a -> [a] -> Sized f n a
- fromListWithDefault' :: (SingI (n :: Nat), ListLike (f a) a) => a -> [a] -> Sized f n a
- unsized :: Sized f n a -> f a
- toSized :: (HasOrdinal nat, ListLike (f a) a) => Sing (n :: nat) -> f a -> Maybe (Sized f n a)
- toSized' :: (ListLike (f a) a, SingI (n :: Nat)) => f a -> Maybe (Sized f n a)
- unsafeToSized :: Sing n -> f a -> Sized f n a
- unsafeToSized' :: (SingI (n :: Nat), ListLike (f a) a) => f a -> Sized f n a
- toSizedWithDefault :: (HasOrdinal nat, ListLike (f a) a) => Sing (n :: nat) -> a -> f a -> Sized f n a
- toSizedWithDefault' :: (SingI (n :: Nat), ListLike (f a) a) => a -> f a -> Sized f n a
- data Partitioned f n a where
- 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
- dropWhile :: (HasOrdinal nat, ListLike (f a) a) => (a -> Bool) -> Sized f n a -> SomeSized f nat a
- span :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> Partitioned f n a
- break :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> Partitioned f n a
- partition :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> Partitioned f n a
- elem :: (ListLike (f a) a, Eq a) => a -> Sized f n a -> Bool
- notElem :: (ListLike (f a) a, Eq a) => a -> Sized f n a -> Bool
- find :: Foldable f => (a -> Bool) -> Sized f n a -> Maybe a
- findF :: Foldable f => (a -> Bool) -> Sized f n a -> Maybe a
- findIndex :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> Maybe Int
- findIndexIF :: FoldableWithIndex i f => (a -> Bool) -> Sized f n a -> Maybe i
- sFindIndex :: (SingI (n :: nat), ListLike (f a) a, HasOrdinal nat) => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n)
- sFindIndexIF :: (FoldableWithIndex i f, Integral i, HasOrdinal nat, SingI n) => (a -> Bool) -> Sized f (n :: nat) a -> Maybe (Ordinal n)
- findIndices :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> [Int]
- findIndicesIF :: FoldableWithIndex i f => (a -> Bool) -> Sized f n a -> [i]
- sFindIndices :: (HasOrdinal nat, SingI (n :: nat), ListLike (f a) a) => (a -> Bool) -> Sized f n a -> [Ordinal n]
- 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
- sElemIndex :: forall n f a. (SingI n, ListLike (f a) a, Eq a, HasOrdinal nat) => a -> Sized f n a -> Maybe (Ordinal n)
- 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]
- sElemIndices :: (HasOrdinal nat, SingI (n :: nat), ListLike (f a) a, Eq a) => a -> Sized f n a -> [Ordinal n]
- viewCons :: forall f a n. (HasOrdinal nat, ListLike (f a) a) => Sized f n a -> ConsView f n a
- data ConsView f n a where
- viewSnoc :: forall f n a. (HasOrdinal nat, ListLike (f a) a) => Sized f n a -> SnocView f n a
- data SnocView f n a where
- 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
- 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
- pattern NilR :: forall nat f n a. (ListLike (f a) a, HasOrdinal nat) => (~) nat n (Zero nat) => Sized nat f n a
Main Data-types
Sized
wraps a sequential type f
and makes length-parametrized version.
Here, f
must be the instance of Functor
and
for all ListLike
(f a) aa
.
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
type ListLikeF f = (Functor f, Forall (LLF f)) Source #
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 Source #
Accessors
Length information
length :: ListLike (f a) a => Sized f n a -> Int Source #
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 Source #
Sing
version of length
.
Since 0.2.0.0
null :: ListLike (f a) a => Sized f n a -> Bool Source #
Test if the sequence is empty or not.
Since 0.1.0.0
Indexing
(%!!) :: (HasOrdinal nat, ListLike (f c) c) => Sized f n c -> Ordinal (n :: nat) -> c Source #
Safe indexing with Ordinal
s.
Since 0.1.0.0
index :: ListLike (f a) a => Int -> Sized f (Succ m) a -> a Source #
Flipped version of !!
.
Since 0.1.0.0
sIndex :: (HasOrdinal nat, ListLike (f c) c) => Ordinal (n :: nat) -> Sized f n c -> c Source #
Flipped version of %!!
.
Since 0.1.0.0
head :: (HasOrdinal nat, ListLike (f a) b, (Zero nat :< n) ~ True) => Sized f n a -> b Source #
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 Source #
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) Source #
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
unsnoc :: ListLike (f a) b => Sized f (Succ n) a -> (Sized f n a, b) Source #
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
Slicing
tail :: (HasOrdinal nat, ListLike (f a) a) => Sized f (Succ n) a -> Sized f (n :: nat) a Source #
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 Source #
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 Source #
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 Source #
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 Source #
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) Source #
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) Source #
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 Source #
Empty sequence.
Since 0.1.0.0
singleton :: forall f a. ListLike (f a) a => a -> Sized f 1 a Source #
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 Source #
replicate :: forall f n a. (HasOrdinal nat, ListLike (f a) a) => Sing n -> a -> Sized f n a Source #
Replicates the same value.
Since 0.1.0.0
replicate' :: (HasOrdinal nat, SingI (n :: nat), ListLike (f a) a) => a -> Sized f n a Source #
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 Source #
Concatenation
cons :: ListLike (f a) b => b -> Sized f n a -> Sized f (Succ n) a Source #
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 Source #
Infix version of cons
.
Since 0.1.0.0
snoc :: ListLike (f a) b => Sized f n a -> b -> Sized f (Succ n) a Source #
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 Source #
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 Source #
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 Source #
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 Source #
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) Source #
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) Source #
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 Source #
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 Source #
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) Source #
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 Source #
Map function.
Since 0.1.0.0
intersperse :: ListLike (f a) a => a -> Sized f n a -> Sized f ((FromInteger 2 :* n) :-. 1) a Source #
Intersperces.
Since 0.1.0.0
nub :: (HasOrdinal nat, ListLike (f a) a, Eq a) => Sized f n a -> SomeSized f nat a Source #
Remove all duplicates.
Since 0.1.0.0
sort :: (ListLike (f a) a, Ord a) => Sized f n a -> Sized f n a Source #
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 Source #
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 Source #
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 Source #
Generalized version of insert
.
Since 0.1.0.0
Conversion
List
fromList :: forall f n a. (HasOrdinal nat, ListLike (f a) a) => Sing (n :: nat) -> [a] -> Maybe (Sized f n a) Source #
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) Source #
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 Source #
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 Source #
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 Source #
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 Source #
fromListWithDefault
with the result length inferred.
Since 0.1.0.0
Base container
unsized :: Sized f n a -> f a Source #
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) Source #
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) Source #
toSized
with the result length inferred.
Since 0.1.0.0
unsafeToSized :: Sing n -> f a -> Sized f n a Source #
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 Source #
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 Source #
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 Source #
toSizedWithDefault
with the result length inferred.
Since 0.1.0.0
Querying
Partitioning
data Partitioned f n a where Source #
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
andrs
, and their length arelenL
andlenR
resp. lenL + lenR = n
Since 0.1.0.0
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 Source #
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 Source #
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 Source #
Invariant:
instance must be implemented
to satisfy the following property:
ListLike
(f a) alength (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 Source #
Invariant:
instance must be implemented
to satisfy the following property:
ListLike
(f a) alength (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 Source #
Invariant:
instance must be implemented
to satisfy the following property:
ListLike
(f a) alength (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 Source #
Membership test; see also notElem
.
Since 0.1.0.0
notElem :: (ListLike (f a) a, Eq a) => a -> Sized f n a -> Bool Source #
Negation of elem
.
Since 0.1.0.0
find :: Foldable f => (a -> Bool) -> Sized f n a -> Maybe a Source #
Find the element satisfying the predicate.
Since 0.1.0.0
findIndex :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> Maybe Int Source #
find the element satisfying findIndex
p xsp
and returns its index if exists.
Since 0.1.0.0
findIndexIF :: FoldableWithIndex i f => (a -> Bool) -> Sized f n a -> Maybe i Source #
implemented in terms of findIndex
FoldableWithIndex
sFindIndex :: (SingI (n :: nat), ListLike (f a) a, HasOrdinal nat) => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n) Source #
sFindIndexIF :: (FoldableWithIndex i f, Integral i, HasOrdinal nat, SingI n) => (a -> Bool) -> Sized f (n :: nat) a -> Maybe (Ordinal n) Source #
implemented in terms of sFindIndex
FoldableWithIndex
findIndices :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> [Int] Source #
find all elements satisfying findIndices
p xsp
and returns their indices.
Since 0.1.0.0
findIndicesIF :: FoldableWithIndex i f => (a -> Bool) -> Sized f n a -> [i] Source #
implemented in terms of findIndices
FoldableWithIndex
sFindIndices :: (HasOrdinal nat, SingI (n :: nat), ListLike (f a) a) => (a -> Bool) -> Sized f n a -> [Ordinal n] Source #
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] Source #
elemIndex :: (Eq a, ListLike (f a) a) => a -> Sized f n a -> Maybe Int Source #
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) Source #
Ordinal version of elemIndex
It statically checks boundary invariants.
If you don't internal structure on
,
then Sized
is much faster and
also safe for most cases.sUnsafeElemIndex
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) Source #
elemIndices :: (ListLike (f a) a, Eq a) => a -> Sized f n a -> [Int] Source #
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] Source #
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 (
is needed for view function.
In the above, we have extra wildcard pattern (SingI
n, 'ListLike (f a) a' f)_
) 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 slenNilL
=SZ
slen (_:<
as) =SS
(slen as) slen _ = error "impossible"
So, we can use
and :<
(resp. NilL
and :>
) to
pattern-match directly on cons-side (resp. snoc-side) as we usually do for lists.
NilR
, :<
, NilL
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.NilR
Definitions
viewCons :: forall f a n. (HasOrdinal nat, ListLike (f a) a) => Sized f n a -> ConsView f n a Source #
Case analysis for the cons-side of sequence.
Since 0.1.0.0
viewSnoc :: forall f n a. (HasOrdinal nat, ListLike (f a) a) => Sized f n a -> SnocView f n a Source #
Case analysis for the snoc-side of sequence.
Since 0.1.0.0
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 Source #
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 Source #
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 Source #
pattern NilR :: forall nat f n a. (ListLike (f a) a, HasOrdinal nat) => (~) nat n (Zero nat) => Sized nat f n a Source #
Orphan instances
(Functor f, HasOrdinal nat1, SingI nat1 n, ListLikeF f) => Applicative (Sized nat1 f n) Source # | Applicative instance, generalizing |