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
- type ListLikeF f = (Functor f, Forall (LLF f))
- data SomeSized f a where
- length :: ListLikeF f => Sized f n a -> Int
- sLength :: SingI n => Sized f n a -> SNat n
- null :: ListLikeF f => Sized f n a -> Bool
- (!!) :: ListLikeF f => Sized f (S m) a -> Int -> a
- (%!!) :: ListLikeF f => Sized f n a -> Ordinal n -> a
- index :: ListLikeF f => Int -> Sized f (S m) c -> c
- sIndex :: ListLikeF f => Ordinal n -> Sized f n c -> c
- head :: ListLikeF f => Sized f (S n) a -> a
- last :: ListLikeF f => Sized f (S n) a -> a
- uncons :: ListLikeF f => Sized f (S n) a -> (a, Sized f n a)
- unsnoc :: ListLikeF f => Sized f (S n) a -> (Sized f n a, a)
- tail :: ListLikeF f => Sized f (S n) a -> Sized f n a
- init :: ListLikeF f => Sized f (S n) a -> Sized f n a
- take :: (ListLikeF f, (n :<<= m) ~ True) => SNat n -> Sized f m a -> Sized f n a
- takeAtMost :: ListLikeF f => SNat n -> Sized f m a -> Sized f (Min n m) a
- drop :: (ListLikeF f, (n :<<= m) ~ True) => SNat n -> Sized f m a -> Sized f (m :-: n) a
- splitAt :: (ListLikeF f, (n :<<= m) ~ True) => SNat n -> Sized f m a -> (Sized f n a, Sized f (m :-: n) a)
- splitAtMost :: ListLikeF f => SNat n -> Sized f m a -> (Sized f (Min n m) a, Sized f (m :-: n) a)
- empty :: forall f a. ListLikeF f => Sized f Z a
- singleton :: forall f a. ListLikeF f => a -> Sized f One a
- toSomeSized :: forall f a. ListLikeF f => f a -> SomeSized f a
- replicate :: forall f n a. ListLikeF f => SNat n -> a -> Sized f n a
- replicate' :: (SingI (n :: Nat), ListLikeF f) => a -> Sized f n a
- cons :: ListLikeF f => a -> Sized f n a -> Sized f (S n) a
- (<|) :: ListLikeF f => a -> Sized f n a -> Sized f (S n) a
- snoc :: ListLikeF f => Sized f n a -> a -> Sized f (S n) a
- (|>) :: ListLikeF f => Sized f n a -> a -> Sized f (S n) a
- append :: ListLikeF f => Sized f n a -> Sized f m a -> Sized f (n :+ m) a
- (++) :: ListLikeF f => Sized f n a -> Sized f m a -> Sized f (n :+ m) a
- concat :: forall f f' m n a. (ListLikeF f, ListLikeF f') => Sized f' m (Sized f n a) -> Sized f (m :* n) a
- zip :: forall f a b n m. ListLikeF f => Sized f n a -> Sized f m b -> Sized f (Min n m) (a, b)
- zipSame :: forall f n a b. ListLikeF f => Sized f n a -> Sized f n b -> Sized f n (a, b)
- zipWith :: forall f a b c m n. ListLikeF f => (a -> b -> c) -> Sized f n a -> Sized f m b -> Sized f (Min n m) c
- zipWithSame :: forall f a b c n. ListLikeF f => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
- unzip :: forall f n a b. ListLikeF f => Sized f n (a, b) -> (Sized f n a, Sized f n b)
- map :: Functor f => (a -> b) -> Sized f n a -> Sized f n b
- reverse :: ListLikeF f => Sized f n a -> Sized f n a
- intersperse :: ListLikeF f => a -> Sized f n a -> Sized f ((Two :* n) :-: One) a
- nub :: (ListLikeF f, Eq a) => Sized f n a -> SomeSized f a
- sort :: (ListLikeF f, Ord a) => Sized f n a -> Sized f n a
- sortBy :: ListLikeF f => (a -> a -> Ordering) -> Sized f n a -> Sized f n a
- insert :: (ListLikeF f, Ord a) => a -> Sized f n a -> Sized f (S n) a
- insertBy :: ListLikeF f => (a -> a -> Ordering) -> a -> Sized f n a -> Sized f (S n) a
- toList :: ListLikeF f => Sized f n a -> [a]
- fromList :: forall f n a. ListLikeF f => SNat n -> [a] -> Maybe (Sized f n a)
- fromList' :: (ListLikeF f, SingI (n :: Nat)) => [a] -> Maybe (Sized f n a)
- unsafeFromList :: forall f n a. ListLikeF f => SNat n -> [a] -> Sized f n a
- unsafeFromList' :: (SingI (n :: Nat), ListLikeF f) => [a] -> Sized f n a
- fromListWithDefault :: forall f n a. ListLikeF f => SNat n -> a -> [a] -> Sized f n a
- fromListWithDefault' :: (SingI (n :: Nat), ListLikeF f) => a -> [a] -> Sized f n a
- unsized :: Sized f n a -> f a
- toSized :: ListLikeF f => SNat n -> f a -> Maybe (Sized f n a)
- toSized' :: (ListLikeF f, SingI (n :: Nat)) => f a -> Maybe (Sized f n a)
- unsafeToSized :: SNat n -> f a -> Sized f n a
- unsafeToSized' :: (SingI (n :: Nat), ListLikeF f) => f a -> Sized f n a
- toSizedWithDefault :: ListLikeF f => SNat n -> a -> f a -> Sized f n a
- toSizedWithDefault' :: (SingI (n :: Nat), ListLikeF f) => a -> f a -> Sized f n a
- data Partitioned f n a where
- takeWhile :: ListLikeF f => (a -> Bool) -> Sized f n a -> SomeSized f a
- dropWhile :: ListLikeF f => (a -> Bool) -> Sized f n a -> SomeSized f a
- span :: ListLikeF f => (a -> Bool) -> Sized f n a -> Partitioned f n a
- break :: ListLikeF f => (a -> Bool) -> Sized f n a -> Partitioned f n a
- partition :: ListLikeF f => (a -> Bool) -> Sized f n a -> Partitioned f n a
- elem :: (ListLikeF f, Eq a) => a -> Sized f n a -> Bool
- notElem :: (ListLikeF f, Eq a) => a -> Sized f n a -> Bool
- find :: ListLikeF f => (a -> Bool) -> Sized f n a -> Maybe a
- findIndex :: ListLikeF f => (a -> Bool) -> Sized f n a -> Maybe Int
- sFindIndex :: (SingI n, ListLikeF f) => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n)
- findIndices :: ListLikeF f => (a -> Bool) -> Sized f n a -> [Int]
- sFindIndices :: (SingI n, ListLikeF f) => (a -> Bool) -> Sized f n a -> [Ordinal n]
- elemIndex :: (Eq a, ListLikeF f) => a -> Sized f n a -> Maybe Int
- sElemIndex :: (SingI n, ListLikeF f, Eq a) => a -> Sized f n a -> Maybe (Ordinal n)
- elemIndices :: (ListLikeF f, Eq a) => a -> Sized f n a -> [Int]
- sElemIndices :: (SingI n, ListLikeF f, Eq a) => a -> Sized f n a -> [Ordinal n]
- viewCons :: forall f a n. (SingI n, ListLikeF f) => Sized f n a -> ConsView f n a
- data ConsView f n a where
- viewSnoc :: forall f n a. (SingI n, ListLikeF f) => Sized f n a -> SnocView f n a
- data SnocView f n a where
- (:<)
- NilL
- (:>)
- NilR
Main Data-types
Sized
wraps a sequential type f
and makes length-parametrized version.
GHC's type natural is currently poor, so we adopt Peano numeral here.
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.1.0.0
Typeable ((k -> *) -> Nat -> k -> *) (Sized k) | |
Functor f => Functor (Sized * f n) | |
Foldable f => Foldable (Sized * f n) | |
Traversable f => Traversable (Sized * f n) | |
Eq (f a) => Eq (Sized k f n a) | |
Ord (f a) => Ord (Sized k f n a) | |
Show (f a) => Show (Sized k f n a) | |
ListLikeF f => FoldableLL (Sized * f n a) a | Since 0.1.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
Accessors
Length information
length :: ListLikeF f => 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
Indexing
(%!!) :: ListLikeF f => Sized f n a -> Ordinal n -> a Source
Safe indexing with Ordinal
s.
Since 0.1.0.0
head :: ListLikeF f => Sized f (S n) a -> a 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 :: ListLikeF f => Sized f (S n) a -> a 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 :: ListLikeF f => Sized f (S n) a -> (a, 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 :: ListLikeF f => Sized f (S n) a -> (Sized f n a, a) 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 :: ListLikeF f => Sized f (S n) a -> Sized f n 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 :: ListLikeF f => Sized f (S 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 :: (ListLikeF f, (n :<<= m) ~ True) => SNat n -> 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 :: ListLikeF f => SNat n -> 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 :: (ListLikeF f, (n :<<= m) ~ True) => SNat n -> 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 :: (ListLikeF f, (n :<<= m) ~ True) => SNat n -> 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 :: ListLikeF f => SNat n -> 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
singleton :: forall f a. ListLikeF f => a -> Sized f One a Source
Sequence with one element.
Since 0.1.0.0
toSomeSized :: forall f a. ListLikeF f => f a -> SomeSized f a Source
replicate :: forall f n a. ListLikeF f => SNat n -> a -> Sized f n a Source
Replicates the same value.
Since 0.1.0.0
replicate' :: (SingI (n :: Nat), ListLikeF f) => a -> Sized f n a Source
replicate
with the length inferred.
Since 0.1.0.0
Concatenation
cons :: ListLikeF f => a -> Sized f n a -> Sized f (S n) a Source
Append an element to the head of sequence.
Since 0.1.0.0
(<|) :: ListLikeF f => a -> Sized f n a -> Sized f (S n) a infixr 5 Source
Infix version of cons
.
Since 0.1.0.0
snoc :: ListLikeF f => Sized f n a -> a -> Sized f (S n) a Source
Append an element to the tail of sequence.
Since 0.1.0.0
(|>) :: ListLikeF f => Sized f n a -> a -> Sized f (S n) a infixl 5 Source
Infix version of snoc
.
Since 0.1.0.0
append :: ListLikeF f => Sized f n a -> Sized f m a -> Sized f (n :+ m) a Source
Append two lists.
Since 0.1.0.0
(++) :: ListLikeF f => 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. (ListLikeF f, ListLikeF f') => 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 :: forall f a b n m. ListLikeF f => 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 :: forall f n a b. ListLikeF f => 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 :: forall f a b c m n. ListLikeF f => (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 :: forall f a b c n. ListLikeF f => (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 :: forall f n a b. ListLikeF f => 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
intersperse :: ListLikeF f => a -> Sized f n a -> Sized f ((Two :* n) :-: One) a Source
Intersperces.
Since 0.1.0.0
nub :: (ListLikeF f, Eq a) => Sized f n a -> SomeSized f a Source
Remove all duplicates.
Since 0.1.0.0
sort :: (ListLikeF f, Ord a) => Sized f n a -> Sized f n a Source
Sorting sequence by ascending order.
Since 0.1.0.0
sortBy :: ListLikeF f => (a -> a -> Ordering) -> Sized f n a -> Sized f n a Source
Generalized version of sort
.
Since 0.1.0.0
insert :: (ListLikeF f, Ord a) => a -> Sized f n a -> Sized f (S n) a Source
Insert new element into the presorted sequence.
Since 0.1.0.0
insertBy :: ListLikeF f => (a -> a -> Ordering) -> a -> Sized f n a -> Sized f (S n) a Source
Generalized version of insert
.
Since 0.1.0.0
Conversion
List
fromList :: forall f n a. ListLikeF f => SNat n -> [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' :: (ListLikeF f, SingI (n :: Nat)) => [a] -> Maybe (Sized f n a) Source
fromList
with the result length inferred.
Since 0.1.0.0
unsafeFromList :: forall f n a. ListLikeF f => SNat 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), ListLikeF f) => [a] -> Sized f n a Source
unsafeFromList
with the result length inferred.
Since 0.1.0.0
fromListWithDefault :: forall f n a. ListLikeF f => SNat 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), ListLikeF f) => 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 :: ListLikeF f => SNat n -> 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' :: (ListLikeF f, SingI (n :: Nat)) => f a -> Maybe (Sized f n a) Source
toSized
with the result length inferred.
Since 0.1.0.0
unsafeToSized :: SNat 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), ListLikeF f) => f a -> Sized f n a Source
unsafeToSized
with the result length inferred.
Since 0.1.0.0
toSizedWithDefault :: ListLikeF f => SNat n -> 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), ListLikeF f) => 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
takeWhile :: ListLikeF f => (a -> Bool) -> Sized f n a -> SomeSized f a Source
Take the initial segment as long as elements satisfys the predicate.
Since 0.1.0.0
dropWhile :: ListLikeF f => (a -> Bool) -> Sized f n a -> SomeSized f a Source
Drop the initial segment as long as elements satisfys the predicate.
Since 0.1.0.0
span :: ListLikeF f => (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 :: ListLikeF f => (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 :: ListLikeF f => (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 :: (ListLikeF f, Eq a) => a -> Sized f n a -> Bool Source
Membership test; see also notElem
.
Since 0.1.0.0
find :: ListLikeF f => (a -> Bool) -> Sized f n a -> Maybe a Source
Find the element satisfying the predicate.
Since 0.1.0.0
findIndex :: ListLikeF f => (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
findIndices :: ListLikeF f => (a -> Bool) -> Sized f n a -> [Int] Source
find all elements satisfying findIndices
p xsp
and returns their indices.
Since 0.1.0.0
sFindIndices :: (SingI n, ListLikeF f) => (a -> Bool) -> Sized f n a -> [Ordinal n] Source
Ordinal
version of findIndices
.
Since 0.1.0.0
elemIndex :: (Eq a, ListLikeF f) => 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 :: (SingI n, ListLikeF f, Eq a) => a -> Sized f n a -> Maybe (Ordinal n) Source
Ordinal version of elemIndex
Since 0.1.0.0
elemIndices :: (ListLikeF f, 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 :: (SingI n, ListLikeF f, 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,ListLikeF
f) =>Sized
f n a ->SNat
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, ListLikeF
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,ListLikeF
f) =>Sized
f n a ->SNat
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 :: (ListLikeF
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 :: (ListLikeF
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,ListLikeF
f) =>Sized
f n a ->SNat
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. (SingI n, ListLikeF f) => 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. (SingI n, ListLikeF f) => Sized f n a -> SnocView f n a Source
Case analysis for the snoc-side of sequence.
Since 0.1.0.0
(:<)
NilL
(:>)
NilR